Hepp-tree cover of the augmented selected cell word

Within one exact support/raw-profile/endpoint signature fibre, the marked block word is dummy-closed. The augmented pairing is full and respects the augmented word, so every occupied label now occurs at least twice. The augmented word is also in the finite lattice box inherited from the actual torus cells.

Thus every actual selected cell word lies in rdec_repeatedTuples after augmentation and hence in at least one valid Hepp-tree slice. The passage from the repeated-tuple carrier to the sum of tree slices is a nonnegative enlargement because the tree cover can overlap; all support/profile/endpoint regrouping before it is exact.

The actual finite box

noncomputable def Anderson4D.selectedCellBoxRadius (ε : ℝ) : ℕ

Natural half-width of the torus grid used by the selected cell partition.

Equations

• Anderson4D.selectedCellBoxRadius ε = (Anderson4D.torusGridRadius ε).natAbs

theorem Anderson4D.torusGridRadius_nonneg {ε : ℝ} (hε : 0 < ε) : 0 ≤ torusGridRadius ε

theorem Anderson4D.selectedCellBoxRadius_cast {ε : ℝ} (hε : 0 < ε) : ↑(selectedCellBoxRadius ε) = torusGridRadius ε

theorem Anderson4D.abs_le_selectedCellBoxRadius_of_mem_torusGrid {ε : ℝ} (hε : 0 < ε) {y : Z4} (hy : y ∈ torusGrid ε) (i : Fin dim) : |y i| ≤ ↑(selectedCellBoxRadius ε)

Every label in the actual torus grid lies in the natural box consumed by the Hepp-tree decomposition.

Augmenting one actual marked-block cell word

noncomputable def Anderson4D.r324SelectedMarkedAugmentedCellWord {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (y : Fin (2 * m) → Z4) : Fin (2 * residualBlockOrder (r324MarkedResidualBlock κp κm π selected) + 2) → Z4

Dummy-closed marked-block word attached to one ambient cell index.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.tupleSupport_openEdgeAugmentedWord {α : Type u_1} [DecidableEq α] {q : ℕ} (w : Fin q → α) (a b : Fin q) : Finset.image (openEdgeAugmentedWord w a b) Finset.univ = Finset.image w Finset.univ

Adding copies of two already occupied endpoint labels does not change the finite support.

theorem Anderson4D.tupleSupport_r324SelectedMarkedAugmentedCellWord {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (y : Fin (2 * m) → Z4) : tupleSupport (r324SelectedMarkedAugmentedCellWord κp κm π selected y) = tupleSupport (r324SelectedMarkedCellWord κp κm π selected y)

theorem Anderson4D.mem_torusGrid_of_mem_r324SelectedPhysicalCells {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (ε : ℝ) (hε : 0 < ε) {y : Fin (2 * m) → Z4} (hy : y ∈ (SmoothCutoff.r324SelectedPhysicalOpenEdgeCells κp κm π selected ε hε).indices) (i : Fin (2 * m)) : y i ∈ torusGrid ε

Every coordinate of an actual ambient cell index lies in the torus grid.

theorem Anderson4D.r324SelectedMarkedCellWord_mem_torusGrid {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (ε : ℝ) (hε : 0 < ε) {y : Fin (2 * m) → Z4} (hy : y ∈ (SmoothCutoff.r324SelectedPhysicalOpenEdgeCells κp κm π selected ε hε).indices) (i : Fin (2 * residualBlockOrder (r324MarkedResidualBlock κp κm π selected))) : r324SelectedMarkedCellWord κp κm π selected y i ∈ torusGrid ε

Every label of the local marked-block word remains in the actual torus grid.

theorem Anderson4D.r324SelectedMarkedAugmentedCellWord_mem_torusGrid {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (ε : ℝ) (hε : 0 < ε) {y : Fin (2 * m) → Z4} (hy : y ∈ (SmoothCutoff.r324SelectedPhysicalOpenEdgeCells κp κm π selected ε hε).indices) (i : Fin (2 * residualBlockOrder (r324MarkedResidualBlock κp κm π selected) + 2)) : r324SelectedMarkedAugmentedCellWord κp κm π selected y i ∈ torusGrid ε

Dummy copies preserve membership in the actual torus grid.

theorem Anderson4D.r324SelectedMarkedAugmentedCellWord_mem_boundedTuples {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (ε : ℝ) (hε : 0 < ε) {y : Fin (2 * m) → Z4} (hy : y ∈ (SmoothCutoff.r324SelectedPhysicalOpenEdgeCells κp κm π selected ε hε).indices) : r324SelectedMarkedAugmentedCellWord κp κm π selected y ∈ rdec_boundedTuples (selectedCellBoxRadius ε) (2 * residualBlockOrder (r324MarkedResidualBlock κp κm π selected) + 2)

The augmented actual marked-block word belongs to the finite bounded tuple carrier.

theorem Anderson4D.r324SelectedMarkedAugmentedCellWord_mem_repeatedTuples {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (ε : ℝ) (hε : 0 < ε) {y : Fin (2 * m) → Z4} (hy : y ∈ (SmoothCutoff.r324SelectedPhysicalOpenEdgeCells κp κm π selected ε hε).indices) : r324SelectedMarkedAugmentedCellWord κp κm π selected y ∈ rdec_repeatedTuples (selectedCellBoxRadius ε) (2 * residualBlockOrder (r324MarkedResidualBlock κp κm π selected) + 2)

The dummy-closed word has no singleton occupied value and hence lies in the repeated-tuple carrier used by the Hepp-tree cover.

The first nonnegative enlargement: overlapping tree slices

theorem Anderson4D.exists_treeRealized_r324SelectedMarkedAugmentedCellWord {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (ε : ℝ) (hε : 0 < ε) {y : Fin (2 * m) → Z4} (hy : y ∈ (SmoothCutoff.r324SelectedPhysicalOpenEdgeCells κp κm π selected ε hε).indices) : ∃ t ∈ rdec_treeEnum (2 * residualBlockOrder (r324MarkedResidualBlock κp κm π selected) + 2), r324SelectedMarkedAugmentedCellWord κp κm π selected y ∈ rdec_treeRealized t (selectedCellBoxRadius ε) (2 * residualBlockOrder (r324MarkedResidualBlock κp κm π selected) + 2)

Every actual augmented marked-block cell word occurs in at least one valid Hepp-tree realization slice.

theorem Anderson4D.r324ValidTree_root_branch_or_eq_leaf {t : PlaneTree} (ht : t.isValid = true) : t.rootV ∈ t.BranchNodes ∨ t = PlaneTree.leaf

A valid tree is either genuinely branched at the root or is the one-leaf tree. The latter is the constant-label base case and must not be silently passed to Proposition 5.7, whose public statement assumes a branched root.

theorem Anderson4D.exists_admissible_realization_r324SelectedMarkedCellWord {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (ε : ℝ) (hε : 0 < ε) {y : Fin (2 * m) → Z4} (hy : y ∈ (SmoothCutoff.r324SelectedPhysicalOpenEdgeCells κp κm π selected ε hε).indices) : ∃ t ∈ rdec_treeEnum (2 * residualBlockOrder (r324MarkedResidualBlock κp κm π selected) + 2), ∃ (Nm : t.HeppMarking) (z : HeppLeaf t → Z4), t.isValid = true ∧ IsAdmissible Nm (selectedCellBoxRadius ε) z ∧ leafEmbeddingImage z = tupleSupport (r324SelectedMarkedCellWord κp κm π selected y) ∧ (t.rootV ∈ t.BranchNodes ∨ t = PlaneTree.leaf)

The tree-cover witness can be refined to an admissible injective leaf embedding whose image is exactly the occupied support of the old open word. This is the realization datum consumed by the occupied-label Proposition 5.7 specialization.

The disjunction is intentional: a branched tree enters Proposition 5.7, whereas the one-leaf constant-label tree remains an explicit base case.

theorem Anderson4D.exists_tree_realization_and_rawFiberBound_of_selectedCell {C : ℝ} (hperm : PermSumEstimate C) {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (ε : ℝ) (hε : 0 < ε) {y : Fin (2 * m) → Z4} (hy : y ∈ (SmoothCutoff.r324SelectedPhysicalOpenEdgeCells κp κm π selected ε hε).indices) : ∃ t ∈ rdec_treeEnum (2 * residualBlockOrder (r324MarkedResidualBlock κp κm π selected) + 2), ∃ (Nm : t.HeppMarking) (z : HeppLeaf t → Z4), t.isValid = true ∧ IsAdmissible Nm (selectedCellBoxRadius ε) z ∧ leafEmbeddingImage z = tupleSupport (r324SelectedMarkedCellWord κp κm π selected y) ∧ (t = PlaneTree.leaf ∨ t.rootV ∈ t.BranchNodes ∧ ∃ (e : HeppLeaf t ≃ ↥(tupleSupport (r324SelectedMarkedCellWord κp κm π selected y))), (∀ (l : HeppLeaf t), ↑(e l) = z l) ∧ let κB := residualPrimitiveBlockPairing (momentCombinedPairing κp κm π) (r324MarkedResidualBlock κp κm π selected) ⋯; let a := r324MarkedResidualLowerPosition κp κm π selected; let b := r324MarkedResidualUpperPosition κp κm π selected; let reference := r324MarkedResidualOccupiedLeafWord κp κm π selected y e; ∃ (n : ℕ), 2 ≤ n ∧ ∑ w ∈ openEdgeRawCountFixedEndpointFiber κB a b reference, heppChainWeight (fun (l : HeppLeaf t) => ↑(e l)) w ≤ (1 + (2 * ↑(selectedCellBoxRadius ε)) ^ 2) ^ 2 * permSumRHS C n t Nm (openEdgeArbitraryMultiplicities κB a b ⋯ ⋯ ⋯ reference ⋯ ⋯))

A genuine selected physical cell word either belongs to the explicit constant-label leaf-tree base case, or its occupied-label realization feeds directly into the raw-count fixed-endpoint Proposition 5.7 bound.

This theorem is still purely the word-sum consumer. It neither asserts the analytic cell majorant nor suppresses the later cell-volume and automorphism ledgers.