Fixed-incidence reindexing by realized sets and induced words

This file supplies the finite carrier change used in paper (5.8)--(5.11). For one fixed paired realization datum, a realized lattice tuple is sent to

• its unlabelled support Z, which is an element of realizedSets, and
• the word of its values, now regarded as a word in the finite alphabet Z.

The tuple is recovered by forgetting the subtype proofs in that word. Consequently the map is injective, its finite image gives an exact reindexing of arbitrary real-valued sums, and the result admits a second exact Fubini decomposition by the induced multiplicity profile on Z.

No estimate or target-shaped hypothesis occurs in this construction.

Supports and finite-support words

def Anderson4D.tupleSupport {m : ℕ} (y : Fin m → Z4) : Finset Z4

The unlabelled set of values occurring in a finite lattice tuple.

Equations

• Anderson4D.tupleSupport y = Finset.image y Finset.univ

@[simp]

theorem Anderson4D.mem_tupleSupport {m : ℕ} {y : Fin m → Z4} {x : Z4} : x ∈ tupleSupport y ↔ ∃ (j : Fin m), y j = x

@[reducible, inline]

abbrev Anderson4D.SupportWord (m : ℕ) (Z : Finset Z4) : Type

A word with values in a prescribed finite support.

Equations

• Anderson4D.SupportWord m Z = (Fin m → ↥Z)

def Anderson4D.SupportWord.toTuple {m : ℕ} {Z : Finset Z4} (w : SupportWord m Z) : Fin m → Z4

Forget the support proofs and recover a lattice tuple.

Equations

• w.toTuple j = ↑(w j)

def Anderson4D.tupleWord {m : ℕ} (y : Fin m → Z4) : SupportWord m (tupleSupport y)

Regard a tuple as a word over its own support.

Equations

• Anderson4D.tupleWord y j = ⟨y j, ⋯⟩

@[simp]

theorem Anderson4D.tupleWord_toTuple {m : ℕ} (y : Fin m → Z4) : (tupleWord y).toTuple = y

def Anderson4D.tupleWordAt {m : ℕ} {y : Fin m → Z4} {Z : Finset Z4} (hZ : tupleSupport y = Z) : SupportWord m Z

Transport a tuple word along an equality of its support with Z.

Equations

• Anderson4D.tupleWordAt hZ j = ⟨y j, ⋯⟩

@[simp]

theorem Anderson4D.tupleWordAt_toTuple {m : ℕ} {y : Fin m → Z4} {Z : Finset Z4} (hZ : tupleSupport y = Z) : (tupleWordAt hZ).toTuple = y

theorem Anderson4D.tupleWordAt_injective {m : ℕ} {Z : Finset Z4} {y y' : Fin m → Z4} (hy : tupleSupport y = Z) (hy' : tupleSupport y' = Z) (h : tupleWordAt hy = tupleWordAt hy') : y = y'

A realized tuple has a realized unlabelled support

theorem Anderson4D.tupleSupport_eq_leafEmbeddingImage_of_realizes {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} {M m : ℕ} {y : Fin m → Z4} (hreal : RealizesTuple t Nm mu M y) : ∃ (z : HeppLeaf t → Z4) (w : Fin m → HeppLeaf t), IsAdmissible Nm M z ∧ w ∈ validWords (leafMultiplicity mu) ∧ (∀ (j : Fin m), y j = z (w j)) ∧ tupleSupport y = leafEmbeddingImage z

The support of a realized tuple is exactly the image of its admissible leaf embedding.

def Anderson4D.pairedBranchData {t : PlaneTree} {M m : ℕ} (d : t.PairedValidRealizationData M m) : t.BranchExponentData (4 * M)

Projection of paired realization data to its branch datum.

Equations

• Anderson4D.pairedBranchData d = (↑d).1

def Anderson4D.pairedMarking {t : PlaneTree} {M m : ℕ} (d : t.PairedValidRealizationData M m) : t.HeppMarking

Projection of paired realization data to its canonical marking.

Equations

• Anderson4D.pairedMarking d = (↑d).toHeppMarking ⋯

def Anderson4D.pairedMultiplicities {t : PlaneTree} {M m : ℕ} (d : t.PairedValidRealizationData M m) : t.Multiplicities

Projection of paired realization data to its canonical multiplicities.

Equations

• Anderson4D.pairedMultiplicities d = (↑d).toMultiplicities ⋯

@[reducible, inline]

abbrev Anderson4D.RealizedSupportWord {t : PlaneTree} {M m : ℕ} (d : t.PairedValidRealizationData M m) : Type

A support/word coordinate whose support is an unlabelled realized set for the branch datum of d.

Equations

• Anderson4D.RealizedSupportWord d = ((Z : ↥(Anderson4D.realizedSets (↑d).1 ⋯)) × Anderson4D.SupportWord m ↑Z)

@[implicit_reducible]

noncomputable instance Anderson4D.instFintypeRealizedSupportWord {t : PlaneTree} {M m : ℕ} (d : t.PairedValidRealizationData M m) : Fintype (RealizedSupportWord d)

Equations

• Anderson4D.instFintypeRealizedSupportWord d = inferInstance

def Anderson4D.RealizedSupportWord.toTuple {t : PlaneTree} {M m : ℕ} {d : t.PairedValidRealizationData M m} (p : RealizedSupportWord d) : Fin m → Z4

Forget a realized support/word coordinate back to its lattice tuple.

Equations

• p.toTuple = p.snd.toTuple

theorem Anderson4D.tupleSupport_mem_realizedSets_of_pairedDataRealizes {t : PlaneTree} {M m : ℕ} (d : t.PairedValidRealizationData M m) {y : Fin m → Z4} (hy : PairedDataRealizes d y) : tupleSupport y ∈ realizedSets (↑d).1 ⋯

A tuple realized by d has an unlabelled support in the public realizedSets carrier.

def Anderson4D.pairedTupleCoordinate {t : PlaneTree} {M m : ℕ} (d : t.PairedValidRealizationData M m) (y : Fin m → Z4) (hy : PairedDataRealizes d y) : RealizedSupportWord d

The canonical support/word coordinate of a tuple realized by d.

Equations

• Anderson4D.pairedTupleCoordinate d y hy = ⟨⟨Anderson4D.tupleSupport y, ⋯⟩, Anderson4D.tupleWord y⟩

@[simp]

theorem Anderson4D.pairedTupleCoordinate_toTuple {t : PlaneTree} {M m : ℕ} (d : t.PairedValidRealizationData M m) (y : Fin m → Z4) (hy : PairedDataRealizes d y) : (pairedTupleCoordinate d y hy).toTuple = y

theorem Anderson4D.pairedTupleCoordinate_injective {t : PlaneTree} {M m : ℕ} (d : t.PairedValidRealizationData M m) {y y' : Fin m → Z4} (hy : PairedDataRealizes d y) (hy' : PairedDataRealizes d y') (h : pairedTupleCoordinate d y hy = pairedTupleCoordinate d y' hy') : y = y'

The support/word coordinate loses no information about the tuple.

Exact finite image of an arbitrary fixed incidence fiber

def Anderson4D.pairedFiberCoordinates {t : PlaneTree} {M m : ℕ} (d : t.PairedValidRealizationData M m) (Y : Finset (Fin m → Z4)) (hY : ∀ y ∈ Y, PairedDataRealizes d y) : Finset (RealizedSupportWord d)

Image of a finite tuple family in unlabelled-support/word coordinates. The hypothesis is local: every tuple in Y is incident to the one fixed datum d.

Equations

• Anderson4D.pairedFiberCoordinates d Y hY = Finset.image (fun (y : ↥Y) => Anderson4D.pairedTupleCoordinate d ↑y ⋯) Y.attach

theorem Anderson4D.pairedFiberCoordinateMap_injective {t : PlaneTree} {M m : ℕ} (d : t.PairedValidRealizationData M m) (Y : Finset (Fin m → Z4)) (hY : ∀ y ∈ Y, PairedDataRealizes d y) : Function.Injective fun (y : ↥Y) => pairedTupleCoordinate d ↑y ⋯

theorem Anderson4D.sum_pairedFiberCoordinates {t : PlaneTree} {M m : ℕ} (d : t.PairedValidRealizationData M m) (Y : Finset (Fin m → Z4)) (hY : ∀ y ∈ Y, PairedDataRealizes d y) (F : (Fin m → Z4) → ℝ) : ∑ p ∈ pairedFiberCoordinates d Y hY, F p.toTuple = ∑ y ∈ Y, F y

Exact fixed-fiber reindexing. Any statistic on tuples can be summed over the finite image of the support/word coordinate with no multiplicity loss.

Fixed-support words and a second exact Fubini decomposition

def Anderson4D.tuplesAtSupport {m : ℕ} (Y : Finset (Fin m → Z4)) (Z : Finset Z4) : Finset (Fin m → Z4)

Tuples in Y whose unlabelled support is exactly Z.

Equations

• Anderson4D.tuplesAtSupport Y Z = {y ∈ Y | Anderson4D.tupleSupport y = Z}

@[simp]

theorem Anderson4D.mem_tuplesAtSupport {m : ℕ} {Y : Finset (Fin m → Z4)} {Z : Finset Z4} {y : Fin m → Z4} : y ∈ tuplesAtSupport Y Z ↔ y ∈ Y ∧ tupleSupport y = Z

def Anderson4D.inducedWordsAtSupport {m : ℕ} (Y : Finset (Fin m → Z4)) (Z : Finset Z4) : Finset (SupportWord m Z)

Words over Z induced by the tuples in the corresponding support fiber.

Equations

• Anderson4D.inducedWordsAtSupport Y Z = Finset.image (fun (y : ↥(Anderson4D.tuplesAtSupport Y Z)) => Anderson4D.tupleWordAt ⋯) (Anderson4D.tuplesAtSupport Y Z).attach

theorem Anderson4D.inducedWordMap_injective {m : ℕ} (Y : Finset (Fin m → Z4)) (Z : Finset Z4) : Function.Injective fun (y : ↥(tuplesAtSupport Y Z)) => tupleWordAt ⋯

theorem Anderson4D.sum_inducedWordsAtSupport {m : ℕ} (Y : Finset (Fin m → Z4)) (Z : Finset Z4) (F : (Fin m → Z4) → ℝ) : ∑ w ∈ inducedWordsAtSupport Y Z, F w.toTuple = ∑ y ∈ tuplesAtSupport Y Z, F y

Reindex one fixed-support fiber by its actual finite word image.

The induced multiplicity profile on one support

def Anderson4D.supportWordMultiplicity {m : ℕ} {Z : Finset Z4} (w : SupportWord m Z) (x : ↥Z) : ℕ

Multiplicity of one support value in a support word.

Equations

• Anderson4D.supportWordMultiplicity w x = {j : Fin m | w j = x}.card

theorem Anderson4D.tupleSupport_toTuple_eq_of_mem_inducedWordsAtSupport {m : ℕ} {Y : Finset (Fin m → Z4)} {Z : Finset Z4} {w : SupportWord m Z} (hw : w ∈ inducedWordsAtSupport Y Z) : tupleSupport w.toTuple = Z

Words induced from the exact support fiber hit every element of Z.

def Anderson4D.supportWordProfile {m : ℕ} {Z : Finset Z4} (w : SupportWord m Z) (hrange : tupleSupport w.toTuple = Z) : PositiveAssignment (↥Z) m

The positive assignment induced by a support word which hits all of its support.

Equations

• Anderson4D.supportWordProfile w hrange = ⟨fun (x : ↥Z) => ⟨Anderson4D.supportWordMultiplicity w x, ⋯⟩, ⋯⟩

def Anderson4D.SupportWord.HasProfile {m : ℕ} {Z : Finset Z4} (w : SupportWord m Z) (p : PositiveAssignment (↥Z) m) : Prop

Profile predicate independent of the proof that a word hits Z.

Equations

• w.HasProfile p = ∀ (x : ↥Z), Anderson4D.supportWordMultiplicity w x = ↑(↑p x)

@[implicit_reducible]

noncomputable instance Anderson4D.instDecidableSupportWordHasProfile {m : ℕ} {Z : Finset Z4} (w : SupportWord m Z) (p : PositiveAssignment (↥Z) m) : Decidable (w.HasProfile p)

Equations

• Anderson4D.instDecidableSupportWordHasProfile w p = Classical.propDecidable (w.HasProfile p)

theorem Anderson4D.supportWordProfile_hasProfile {m : ℕ} {Z : Finset Z4} (w : SupportWord m Z) (hrange : tupleSupport w.toTuple = Z) : w.HasProfile (supportWordProfile w hrange)

noncomputable def Anderson4D.inducedWordsAtProfile {m : ℕ} (Y : Finset (Fin m → Z4)) (Z : Finset Z4) (p : PositiveAssignment (↥Z) m) : Finset (SupportWord m Z)

Words in one realized-support fiber having the prescribed induced multiplicity assignment p.

Equations

• Anderson4D.inducedWordsAtProfile Y Z p = {w ∈ Anderson4D.inducedWordsAtSupport Y Z | w.HasProfile p}

theorem Anderson4D.sum_inducedWords_eq_sum_profiles {m : ℕ} (Y : Finset (Fin m → Z4)) (Z : Finset Z4) (F : SupportWord m Z → ℝ) : ∑ w ∈ inducedWordsAtSupport Y Z, F w = ∑ p : PositiveAssignment (↥Z) m, ∑ w ∈ inducedWordsAtProfile Y Z p, F w

Exact second Fubini decomposition by the induced multiplicity assignment χ from paper (5.8)--(5.9).

theorem Anderson4D.card_positiveAssignments_support_le_two_pow (m : ℕ) (Z : Finset Z4) : Fintype.card (PositiveAssignment (↥Z) m) ≤ 2 ^ m

There are at most 2^m possible induced profiles, uniformly in the size and labelling of the support.

Every induced word carries a genuine leaf realization

def Anderson4D.SupportWord.IsInducedBy {t : PlaneTree} {M m : ℕ} (d : t.PairedValidRealizationData M m) {Z : Finset Z4} (w : SupportWord m Z) : Prop

A support word is induced by the fixed paired datum d when it is the value word of one admissible leaf embedding with the prescribed leaf multiplicities.

Equations

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

theorem Anderson4D.SupportWord.isInducedBy_of_mem_inducedWordsAtSupport {t : PlaneTree} {M m : ℕ} (d : t.PairedValidRealizationData M m) (Y : Finset (Fin m → Z4)) (hY : ∀ y ∈ Y, PairedDataRealizes d y) {Z : Finset Z4} {w : SupportWord m Z} (hw : w ∈ inducedWordsAtSupport Y Z) : IsInducedBy d w

Every word in the exact fixed-incidence image has a genuine admissible leaf realization; this is the local witness needed to invoke Proposition 5.7 after grouping by profile.

noncomputable def Anderson4D.leafEquivSupport {t : PlaneTree} {Z : Finset Z4} (z : HeppLeaf t → Z4) (hz : Function.Injective z) (himage : leafEmbeddingImage z = Z) : HeppLeaf t ≃ ↥Z

An injective leaf embedding whose image is Z gives an equivalence from the labelled leaves to the unlabelled support.

Equations

• Anderson4D.leafEquivSupport z hz himage = Equiv.ofBijective (fun (l : Anderson4D.HeppLeaf t) => ⟨z l, ⋯⟩) ⋯

@[simp]

theorem Anderson4D.leafEquivSupport_apply_val {t : PlaneTree} {Z : Finset Z4} (z : HeppLeaf t → Z4) (hz : Function.Injective z) (himage : leafEmbeddingImage z = Z) (l : HeppLeaf t) : ↑((leafEquivSupport z hz himage) l) = z l

theorem Anderson4D.supportWordMultiplicity_eq_leafMultiplicity {t : PlaneTree} {M m : ℕ} (d : t.PairedValidRealizationData M m) {Z : Finset Z4} (w : SupportWord m Z) {z : HeppLeaf t → Z4} {u : Fin m → HeppLeaf t} (hadm : IsAdmissible (pairedMarking d) M z) (hu : u ∈ validWords (leafMultiplicity (pairedMultiplicities d))) (himage : leafEmbeddingImage z = Z) (hwu : ∀ (j : Fin m), ↑(w j) = z (u j)) (x : ↥Z) : supportWordMultiplicity w x = leafMultiplicity (pairedMultiplicities d) ((leafEquivSupport z ⋯ himage).symm x)

Under a genuine leaf realization, the support multiplicity profile is the leaf multiplicity function transported along the leaf/support equivalence.

def Anderson4D.reindexSupportWord {t : PlaneTree} {m : ℕ} {Z : Finset Z4} (e : HeppLeaf t ≃ ↥Z) (w : SupportWord m Z) : Fin m → HeppLeaf t

Reindex a support word by a leaf/support equivalence.

Equations

• Anderson4D.reindexSupportWord e w j = e.symm (w j)

theorem Anderson4D.reindexSupportWord_injective {t : PlaneTree} {m : ℕ} {Z : Finset Z4} (e : HeppLeaf t ≃ ↥Z) : Function.Injective (reindexSupportWord e)

theorem Anderson4D.reindexSupportWord_fiber_card {t : PlaneTree} {m : ℕ} {Z : Finset Z4} (e : HeppLeaf t ≃ ↥Z) (w : SupportWord m Z) (l : HeppLeaf t) : {j : Fin m | reindexSupportWord e w j = l}.card = supportWordMultiplicity w (e l)

Fiber cardinality after reindexing a support word to the leaf alphabet.

theorem Anderson4D.reindexSupportWord_mem_validWords_of_sameProfile {t : PlaneTree} {M m : ℕ} (d : t.PairedValidRealizationData M m) {Z : Finset Z4} (p : PositiveAssignment (↥Z) m) (w₀ w : SupportWord m Z) (hw₀profile : w₀.HasProfile p) (hwprofile : w.HasProfile p) {z : HeppLeaf t → Z4} {u₀ : Fin m → HeppLeaf t} (hadm : IsAdmissible (pairedMarking d) M z) (hu₀ : u₀ ∈ validWords (leafMultiplicity (pairedMultiplicities d))) (himage : leafEmbeddingImage z = Z) (hw₀u : ∀ (j : Fin m), ↑(w₀ j) = z (u₀ j)) : reindexSupportWord (leafEquivSupport z ⋯ himage) w ∈ validWords (leafMultiplicity (pairedMultiplicities d))

Fixing one realized word in a profile identifies that profile with the fixed datum's labelled leaf multiplicities. Every other word with the same profile therefore reindexes to a validWords word on the leaves.

Pairing primitivity and the chain weight survive the reindexing

noncomputable def Anderson4D.supportChainWeight {m : ℕ} {Z : Finset Z4} (w : SupportWord m Z) : ℝ

The adjacent-chain product read directly on a support word.

Equations

• Anderson4D.supportChainWeight w = ∏ j : Anderson4D.AdjacentIndex m, Anderson4D.latticeEdgeWeight ↑(w ↑j) ↑(w (Anderson4D.adjacentSucc j))

theorem Anderson4D.supportChainWeight_nonneg {m : ℕ} {Z : Finset Z4} (w : SupportWord m Z) : 0 ≤ supportChainWeight w

theorem Anderson4D.supportWord_respectsWord_iff_toTuple {m : ℕ} {Z : Finset Z4} (A : Finset (Fin m)) (κ : AcrossPairing A) (w : SupportWord m Z) : RespectsWord A w κ ↔ RespectsWord A w.toTuple κ

Reading pairing compatibility before or after forgetting support proofs is equivalent.

theorem Anderson4D.SupportWord.respectsWord_of_mem_inducedWordsAtSupport {m : ℕ} {Y : Finset (Fin m → Z4)} {Z : Finset Z4} {w : SupportWord m Z} (A : Finset (Fin m)) (κ : AcrossPairing A) (hY : ∀ y ∈ Y, RespectsWord A y κ) (hw : w ∈ inducedWordsAtSupport Y Z) : RespectsWord A w κ

If the original tuple family respects one across pairing, every induced support word respects it as well.

theorem Anderson4D.supportChainWeight_eq_heppChainWeight {t : PlaneTree} {m : ℕ} {Z : Finset Z4} (w : SupportWord m Z) (z : HeppLeaf t → Z4) (u : Fin m → HeppLeaf t) (hwu : ∀ (j : Fin m), ↑(w j) = z (u j)) : supportChainWeight w = heppChainWeight z u

A leaf realization reads the same adjacent-chain product as its support word.

theorem Anderson4D.reindexSupportWord_respectsWord {t : PlaneTree} {m : ℕ} {Z : Finset Z4} (e : HeppLeaf t ≃ ↥Z) (A : Finset (Fin m)) (κ : AcrossPairing A) (w : SupportWord m Z) (hw : RespectsWord A w κ) : RespectsWord A (reindexSupportWord e w) κ

Renaming the support alphabet along an equivalence preserves compatibility with a fixed across pairing.

theorem Anderson4D.supportChainWeight_eq_heppChainWeight_reindex {t : PlaneTree} {m : ℕ} {Z : Finset Z4} (e : HeppLeaf t ≃ ↥Z) (w : SupportWord m Z) (z : HeppLeaf t → Z4) (he : ∀ (l : HeppLeaf t), ↑(e l) = z l) : supportChainWeight w = heppChainWeight z (reindexSupportWord e w)

If an alphabet equivalence is induced by an embedding z, reindexing does not change the adjacent-chain product.

theorem Anderson4D.SupportWord.exists_primitiveLeafRealization {t : PlaneTree} {M m : ℕ} (d : t.PairedValidRealizationData M m) {Z : Finset Z4} (w : SupportWord m Z) (A : Finset (Fin m)) (κ : AcrossPairing A) (hinduced : IsInducedBy d w) (hrespects : RespectsWord A w κ) (hprimitive : IsPrimitiveAcross A κ) : ∃ (z : HeppLeaf t → Z4) (u : Fin m → HeppLeaf t), IsAdmissible (pairedMarking d) M z ∧ u ∈ validWords (leafMultiplicity (pairedMultiplicities d)) ∧ leafEmbeddingImage z = Z ∧ (∀ (j : Fin m), ↑(w j) = z (u j)) ∧ NoProperLeafBlock u ∧ supportChainWeight w = heppChainWeight z u

A primitive across pairing on the support word transports through an injective admissible embedding to the paper's primitive leaf-word condition (5.11)(c).

theorem Anderson4D.wordSumFiltered_le_paperSumFiltered_of_nonneg {α : Type u_1} [Fintype α] [DecidableEq α] {m : ℕ} (mult : α → ℕ) (P : (Fin m → α) → Prop) [DecidablePred P] (F : (Fin m → α) → ℝ) (hF : ∀ (w : Fin m → α), 0 ≤ F w) : wordSumFiltered mult P F ≤ paperSumFiltered mult P F

A raw restricted word sum is no larger than its factorial-ledger counterpart when the summand is nonnegative.

theorem Anderson4D.permSumRHS_nonneg {C : ℝ} (hC : 0 ≤ C) (n : ℕ) (t : PlaneTree) (Nm : t.HeppMarking) (mu : t.Multiplicities) : 0 ≤ permSumRHS C n t Nm mu

The explicit right-hand side of Proposition 5.7 is nonnegative for a nonnegative constant.

theorem Anderson4D.two_pow_two_mul_permSumRHS (C : ℝ) (n : ℕ) (t : PlaneTree) (Nm : t.HeppMarking) (mu : t.Multiplicities) : ↑(2 ^ (2 * n)) * permSumRHS C n t Nm mu = permSumRHS (4 * C) n t Nm mu

The exponential profile count is absorbed by multiplying the absolute constant in Proposition 5.7 by four.

theorem Anderson4D.sum_inducedWordsAtProfile_chainWeight_le_wordSumFiltered {t : PlaneTree} {M m : ℕ} (d : t.PairedValidRealizationData M m) (Y : Finset (Fin m → Z4)) {Z : Finset Z4} (p : PositiveAssignment (↥Z) m) (A : Finset (Fin m)) (κ : AcrossPairing A) (hYreal : ∀ y ∈ Y, PairedDataRealizes d y) (hYrespect : ∀ y ∈ Y, RespectsWord A y κ) (hprimitive : IsPrimitiveAcross A κ) (hne : (inducedWordsAtProfile Y Z p).Nonempty) : ∃ (z : HeppLeaf t → Z4), IsAdmissible (pairedMarking d) M z ∧ leafEmbeddingImage z = Z ∧ ∑ w ∈ inducedWordsAtProfile Y Z p, supportChainWeight w ≤ wordSumFiltered (leafMultiplicity (pairedMultiplicities d)) NoProperLeafBlock (heppChainWeight z)

Fixed-profile bridge to the primitive word sum.

Choose any realized word in a nonempty profile fiber. Its admissible leaf embedding identifies the unlabelled support with the labelled leaves. Every other word in the profile then reindexes injectively into the paper's validWords carrier, and primitivity supplies condition (5.11)(c). Hence the whole fixed-profile chain sum is bounded by the restricted word sum appearing immediately before Proposition 5.7.

theorem Anderson4D.sum_inducedWordsAtProfile_chainWeight_le_permSumRHS {C : ℝ} (hC : PermSumEstimate C) {n M : ℕ} {t : PlaneTree} (d : t.PairedValidRealizationData M (2 * n)) (Y : Finset (Fin (2 * n) → Z4)) {Z : Finset Z4} (p : PositiveAssignment (↥Z) (2 * n)) (A : Finset (Fin (2 * n))) (κ : AcrossPairing A) (hn : 2 ≤ n) (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (hYreal : ∀ y ∈ Y, PairedDataRealizes d y) (hYrespect : ∀ y ∈ Y, RespectsWord A y κ) (hprimitive : IsPrimitiveAcross A κ) (hne : (inducedWordsAtProfile Y Z p).Nonempty) : ∃ (z : HeppLeaf t → Z4), IsAdmissible (pairedMarking d) M z ∧ leafEmbeddingImage z = Z ∧ ∑ w ∈ inducedWordsAtProfile Y Z p, supportChainWeight w ≤ permSumRHS C n t (pairedMarking d) (pairedMultiplicities d)

Paper (5.8)--(5.11), fixed-profile analytic bound.

For total length 2n, the preceding exact reindexing feeds directly into Proposition 5.7. Validity and parity are read from the paired realization datum itself, so the only remaining assumptions are precisely P-5.7's tree hypotheses and the nonempty primitive profile fiber.

theorem Anderson4D.sum_inducedWordsAtProfile_chainWeight_le_permSumRHS_unconditional {C : ℝ} (hC : PermSumEstimate C) {n M : ℕ} {t : PlaneTree} (d : t.PairedValidRealizationData M (2 * n)) (Y : Finset (Fin (2 * n) → Z4)) {Z : Finset Z4} (p : PositiveAssignment (↥Z) (2 * n)) (A : Finset (Fin (2 * n))) (κ : AcrossPairing A) (hn : 2 ≤ n) (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (hYreal : ∀ y ∈ Y, PairedDataRealizes d y) (hYrespect : ∀ y ∈ Y, RespectsWord A y κ) (hprimitive : IsPrimitiveAcross A κ) : ∑ w ∈ inducedWordsAtProfile Y Z p, supportChainWeight w ≤ permSumRHS C n t (pairedMarking d) (pairedMultiplicities d)

Empty profile fibers satisfy the same bound trivially; nonempty fibers use the genuine embedding extracted above.

theorem Anderson4D.sum_profiles_chainWeight_le_two_pow_mul_permSumRHS {C : ℝ} (hC : PermSumEstimate C) {n M : ℕ} {t : PlaneTree} (d : t.PairedValidRealizationData M (2 * n)) (Y : Finset (Fin (2 * n) → Z4)) (Z : Finset Z4) (A : Finset (Fin (2 * n))) (κ : AcrossPairing A) (hn : 2 ≤ n) (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (hYreal : ∀ y ∈ Y, PairedDataRealizes d y) (hYrespect : ∀ y ∈ Y, RespectsWord A y κ) (hprimitive : IsPrimitiveAcross A κ) : ∑ p : PositiveAssignment (↥Z) (2 * n), ∑ w ∈ inducedWordsAtProfile Y Z p, supportChainWeight w ≤ ↑(2 ^ (2 * n)) * permSumRHS C n t (pairedMarking d) (pairedMultiplicities d)

Summing over all induced profiles costs at most 2^(2n), the exact profile-count loss from (5.9).

theorem Anderson4D.sum_inducedWordsAtSupport_chainWeight_le_two_pow_mul_permSumRHS {C : ℝ} (hC : PermSumEstimate C) {n M : ℕ} {t : PlaneTree} (d : t.PairedValidRealizationData M (2 * n)) (Y : Finset (Fin (2 * n) → Z4)) (Z : Finset Z4) (A : Finset (Fin (2 * n))) (κ : AcrossPairing A) (hn : 2 ≤ n) (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (hYreal : ∀ y ∈ Y, PairedDataRealizes d y) (hYrespect : ∀ y ∈ Y, RespectsWord A y κ) (hprimitive : IsPrimitiveAcross A κ) : ∑ w ∈ inducedWordsAtSupport Y Z, supportChainWeight w ≤ ↑(2 ^ (2 * n)) * permSumRHS C n t (pairedMarking d) (pairedMultiplicities d)

The complete fixed-support word fiber, after summing away the profile coordinate, is controlled by the same 2^(2n) loss.

theorem Anderson4D.sum_inducedWordsAtSupport_chainWeight_le_permSumRHS_four_mul {C : ℝ} (hC : PermSumEstimate C) {n M : ℕ} {t : PlaneTree} (d : t.PairedValidRealizationData M (2 * n)) (Y : Finset (Fin (2 * n) → Z4)) (Z : Finset Z4) (A : Finset (Fin (2 * n))) (κ : AcrossPairing A) (hn : 2 ≤ n) (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (hYreal : ∀ y ∈ Y, PairedDataRealizes d y) (hYrespect : ∀ y ∈ Y, RespectsWord A y κ) (hprimitive : IsPrimitiveAcross A κ) : ∑ w ∈ inducedWordsAtSupport Y Z, supportChainWeight w ≤ permSumRHS (4 * C) n t (pairedMarking d) (pairedMultiplicities d)

Constant-absorbed form of the complete fixed-support estimate. This is the statement consumed by the outer realized-set summation: all profile bookkeeping has disappeared into the replacement C ↦ 4C.

theorem Anderson4D.sum_eq_sum_tuplesAtSupport {m : ℕ} (Y : Finset (Fin m → Z4)) (S : Finset (Finset Z4)) (hS : ∀ y ∈ Y, tupleSupport y ∈ S) (F : (Fin m → Z4) → ℝ) : ∑ y ∈ Y, F y = ∑ Z ∈ S, ∑ y ∈ tuplesAtSupport Y Z, F y

Exact grouping of a finite tuple family by unlabelled support, provided every occurring support belongs to the chosen finite support carrier.

theorem Anderson4D.sum_pairedFiber_eq_realizedSets_words {t : PlaneTree} {M m : ℕ} (d : t.PairedValidRealizationData M m) (Y : Finset (Fin m → Z4)) (hY : ∀ y ∈ Y, PairedDataRealizes d y) (F : (Fin m → Z4) → ℝ) : ∑ y ∈ Y, F y = ∑ Z ∈ realizedSets (↑d).1 ⋯, ∑ w ∈ inducedWordsAtSupport Y Z, F w.toTuple

Paper (5.8)--(5.11), carrier-level finite Fubini.

A fixed paired incidence fiber is first grouped by its unlabelled realized set and then reindexed by the actual words occurring over that set. The equality is exact for every statistic F; neither automorphism factors nor factorial bounds have entered yet.

theorem Anderson4D.sum_pairedFiber_eq_realizedSets_profiles_words {t : PlaneTree} {M m : ℕ} (d : t.PairedValidRealizationData M m) (Y : Finset (Fin m → Z4)) (hY : ∀ y ∈ Y, PairedDataRealizes d y) (F : (Fin m → Z4) → ℝ) : ∑ y ∈ Y, F y = ∑ Z ∈ realizedSets (↑d).1 ⋯, ∑ p : PositiveAssignment (↥Z) m, ∑ w ∈ inducedWordsAtProfile Y Z p, F w.toTuple

Full carrier decomposition through the paper's χ parameter.

This is the exact three-level finite sum over an unlabelled realized set, a positive multiplicity assignment on that set, and the words with that assignment. The preceding exponential cardinality theorem bounds the middle carrier by 2^m.