Occupied-label realization of the marked R-324 block

This file specializes the generic occupied-label reindexing to the unique marked residual primitive block. A genuine ambient selected cell word is first restricted to that block and then reindexed by an equivalence between its finite occupied support and the leaves of a Hepp tree.

The resulting reference leaf word is surjective, respects every unmarked local pairing edge, and is therefore a direct input to the correct raw-count fixed-endpoint Proposition 5.7 fibre bound.

This remains a word-sum theorem. It does not assert a cell-integral majorant or discharge the cell-volume and automorphism ledgers.

noncomputable def Anderson4D.r324MarkedResidualOccupiedLeafWord {t : PlaneTree} {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (y : Fin (2 * m) → Z4) (e : HeppLeaf t ≃ ↥(tupleSupport (r324MarkedResidualBlockWord κp κm π selected y))) : Fin (2 * residualBlockOrder (r324MarkedResidualBlock κp κm π selected)) → HeppLeaf t

Reindex the marked-block restriction of an ambient selected cell word by a Hepp-leaf/occupied-support equivalence.

Equations

• Anderson4D.r324MarkedResidualOccupiedLeafWord κp κm π selected y e = Anderson4D.reindexSupportWord e (Anderson4D.tupleWord (Anderson4D.r324MarkedResidualBlockWord κp κm π selected y))

theorem Anderson4D.r324MarkedResidualOccupiedLeafWord_surjective {t : PlaneTree} {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (y : Fin (2 * m) → Z4) (e : HeppLeaf t ≃ ↥(tupleSupport (r324MarkedResidualBlockWord κp κm π selected y))) : Function.Surjective (r324MarkedResidualOccupiedLeafWord κp κm π selected y e)

The marked-block leaf word is surjective onto the leaves of its occupied-support Hepp realization.

theorem Anderson4D.r324MarkedResidualOccupiedLeafWord_respectsExcept {t : PlaneTree} {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (y : Fin (2 * m) → Z4) (hy : RespectsPairingExcept (momentCombinedPairing κp κm π) (r324ResidualMarkedLowerEndpoint selected) (r324ResidualMarkedUpperEndpoint π selected) y) (e : HeppLeaf t ≃ ↥(tupleSupport (r324MarkedResidualBlockWord κp κm π selected y))) (i : Fin (2 * residualBlockOrder (r324MarkedResidualBlock κp κm π selected))) : i ≠ r324MarkedResidualLowerPosition κp κm π selected → i ≠ r324MarkedResidualUpperPosition κp κm π selected → r324MarkedResidualOccupiedLeafWord κp κm π selected y e i = r324MarkedResidualOccupiedLeafWord κp κm π selected y e ((residualPrimitiveBlockPairing (momentCombinedPairing κp κm π) (r324MarkedResidualBlock κp κm π selected) ⋯) i)

The occupied-label leaf word retains equality on every unmarked edge of the canonical marked primitive pairing.

theorem Anderson4D.r324MarkedResidualRawCountFiber_le_permSumRHS {C : ℝ} (hperm : PermSumEstimate C) {t : PlaneTree} {m M : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (y : Fin (2 * m) → Z4) (hy : RespectsPairingExcept (momentCombinedPairing κp κm π) (r324ResidualMarkedLowerEndpoint selected) (r324ResidualMarkedUpperEndpoint π selected) y) (e : HeppLeaf t ≃ ↥(tupleSupport (r324MarkedResidualBlockWord κp κm π selected y))) (Nm : t.HeppMarking) (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (hadm : IsAdmissible Nm M fun (l : HeppLeaf t) => ↑(e 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 * ↑M) ^ 2) ^ 2 * permSumRHS C n t Nm (openEdgeArbitraryMultiplicities κB a b ⋯ ⋯ ⋯ reference ⋯ ⋯)

Direct Proposition 5.7 bound for the raw-count fibre generated by an actual marked-block selected cell word. Surjectivity is obtained from the occupied finite support, never from Z4.