Final primitive-pairing ledger

This file contains the last algebraic and finite-sum steps in paper (5.5)--(5.17). In particular, the primitive pairing is kept inside the word sum until the (m_l / 2)! / m_l! gain from (5.10) has been used. Summing a fixed-pairing estimate here would lose precisely the factorial gain which makes the argument close.

The leaf-factorial cancellation after (5.15)

theorem Anderson4D.halfFactorial_div_factorial_mul_sqrtFactorial_le_one (m : ℕ) (hm : Even m) : ↑(m / 2).factorial / ↑m.factorial * sqrtFactorial m ≤ 1

For an even multiplicity, the half-factorial supplied by the pairing count cancels the square-root factorial in Proposition 5.7.

theorem Anderson4D.pairedFactorialLedger_le_one {t : PlaneTree} (mu : t.Multiplicities) (heven : ∀ (l : HeppLeaf t), Even (leafMultiplicity mu l)) : (∏ l : HeppLeaf t, ↑(leafMultiplicity mu l / 2).factorial / ↑(leafMultiplicity mu l).factorial) * ∏ l : HeppLeaf t, sqrtFactorial (leafMultiplicity mu l) ≤ 1

Product form of the preceding cancellation, exactly the leaf ledger remaining after multiplying (5.10) and (5.15).

Primitive pairings survive the support/leaf reindexing

theorem Anderson4D.primitiveCompatibleAcrossPairings_reindexSupportWord {t : PlaneTree} {m : ℕ} {Z : Finset Z4} (e : HeppLeaf t ≃ ↥Z) (A : Finset (Fin m)) (w : SupportWord m Z) : primitiveCompatibleAcrossPairings A (reindexSupportWord e w) = primitiveCompatibleAcrossPairings A w

theorem Anderson4D.sum_profile_primitivePairings_chainWeight_le {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)) (hYreal : ∀ y ∈ Y, PairedDataRealizes d y) (hne : (inducedWordsAtProfile Y Z p).Nonempty) : ∃ (z : HeppLeaf t → Z4), IsAdmissible (pairedMarking d) M z ∧ leafEmbeddingImage z = Z ∧ ∑ w ∈ inducedWordsAtProfile Y Z p, ↑(primitiveCompatibleAcrossPairings A w).card * supportChainWeight w ≤ primitivePairedWordSum (leafMultiplicity (pairedMultiplicities d)) A (heppChainWeight z)

Fixed-profile form of (5.8)--(5.10), with all primitive pairings summed before Proposition 5.7 is applied. This is the pairing-preserving counterpart of the fixed-κ fiber theorem.

Applying Proposition 5.7 without losing (5.10)

noncomputable def Anderson4D.pairedFactorialQuotient {t : PlaneTree} {M m : ℕ} (d : t.PairedValidRealizationData M m) : ℝ

The exact half-factorial quotient supplied by the primitive pairing count for the multiplicities carried by d.

Equations

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

theorem Anderson4D.pairedFactorialQuotient_nonneg {t : PlaneTree} {M m : ℕ} (d : t.PairedValidRealizationData M m) : 0 ≤ pairedFactorialQuotient d

theorem Anderson4D.sum_profile_primitivePairings_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))) (hn : 2 ≤ n) (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (hYreal : ∀ y ∈ Y, PairedDataRealizes d y) : ∑ w ∈ inducedWordsAtProfile Y Z p, ↑(primitiveCompatibleAcrossPairings A w).card * supportChainWeight w ≤ pairedFactorialQuotient d * permSumRHS C n t (pairedMarking d) (pairedMultiplicities d)

One fixed multiplicity profile, including all compatible primitive pairings, is bounded by Proposition 5.7 with the exact (5.10) quotient.

theorem Anderson4D.sum_profiles_primitivePairings_chainWeight_le {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))) (hn : 2 ≤ n) (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (hYreal : ∀ y ∈ Y, PairedDataRealizes d y) : ∑ p : PositiveAssignment (↥Z) (2 * n), ∑ w ∈ inducedWordsAtProfile Y Z p, ↑(primitiveCompatibleAcrossPairings A w).card * supportChainWeight w ≤ ↑(2 ^ (2 * n)) * (pairedFactorialQuotient d * permSumRHS C n t (pairedMarking d) (pairedMultiplicities d))

Summing the genuine profile carrier costs at most 2^(2n), while the primitive-pairing factorial quotient remains intact.

Removing the remaining leaf factorials

noncomputable def Anderson4D.primitiveScaleRHS (C : ℝ) (n : ℕ) (t : PlaneTree) (Nm : t.HeppMarking) : ℝ

The scale tail which remains from (5.15) after the leaf factorials, the volume monomial, and the root-diameter factor have been cancelled.

Equations

• Anderson4D.primitiveScaleRHS C n t Nm = C ^ n * ∑ W ∈ (Anderson4D.nonrootBranches t).powerset, ↑(n - W.card).factorial * Anderson4D.permSumScaleTail Nm W

theorem Anderson4D.primitive_permSumScaleTail_nonneg {t : PlaneTree} (Nm : t.HeppMarking) (W : Finset t.VPos) : 0 ≤ permSumScaleTail Nm W

theorem Anderson4D.primitiveScaleRHS_nonneg {C : ℝ} (hC : 0 ≤ C) (n : ℕ) (t : PlaneTree) (Nm : t.HeppMarking) : 0 ≤ primitiveScaleRHS C n t Nm

theorem Anderson4D.pairedFactorialQuotient_mul_permSumRHS_le_primitiveScaleRHS {C : ℝ} (hC : 0 ≤ C) {n M : ℕ} {t : PlaneTree} (d : t.PairedValidRealizationData M (2 * n)) : pairedFactorialQuotient d * permSumRHS C n t (pairedMarking d) (pairedMultiplicities d) ≤ primitiveScaleRHS C n t (pairedMarking d)

The pairing quotient cancels every square-root leaf factorial in Proposition 5.7.

theorem Anderson4D.sum_profiles_primitivePairings_chainWeight_le_primitiveScaleRHS {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))) (hn : 2 ≤ n) (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (hYreal : ∀ y ∈ Y, PairedDataRealizes d y) : ∑ p : PositiveAssignment (↥Z) (2 * n), ∑ w ∈ inducedWordsAtProfile Y Z p, ↑(primitiveCompatibleAcrossPairings A w).card * supportChainWeight w ≤ primitiveScaleRHS (4 * C) n t (pairedMarking d)

The two profile-count powers from (5.8)--(5.9) are absorbed into C ↦ 4C, after which no leaf-factorial term remains.

Exact volume/diameter scale cancellation in (5.16)

noncomputable def Anderson4D.primitiveRatioRHS (C : ℝ) (n : ℕ) (t : PlaneTree) (Nm : t.HeppMarking) : ℝ

The right side of (5.16), before the summation over increasing markings.

Equations

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

theorem Anderson4D.primitiveRatioRHS_nonneg {C : ℝ} (hC : 0 ≤ C) (n : ℕ) (t : PlaneTree) (Nm : t.HeppMarking) : 0 ≤ primitiveRatioRHS C n t Nm

theorem Anderson4D.branchVolume_rootDiameter_mul_primitiveScaleRHS (C : ℝ) (n : ℕ) (t : PlaneTree) (Nm : t.HeppMarking) : branchScaleProduct Nm * ↑(scaleN Nm t.rootV) ^ 2 * primitiveScaleRHS C n t Nm = primitiveRatioRHS C n t Nm

The P-5.6 volume monomial cancels the inverse branch monomial in P-5.7, while the root-scale square paying for the diameter cancels N_r⁻². Only the parent ratios indexed by B \\ (W ∪ {r}) remain.

Summing the genuine increasing markings

noncomputable def Anderson4D.primitiveMarkingRatioSum (C : ℝ) (n M : ℕ) (t : PlaneTree) : ℝ

The actual finite marking sum remaining after (5.16), on the sharp logarithmic exponent carrier.

Equations

• Anderson4D.primitiveMarkingRatioSum C n M t = ∑ N : Anderson4D.ValidBranchExponentData t (Nat.log 2 (4 * M)), Anderson4D.primitiveRatioRHS C n t ((↑N).toHeppMarking ⋯)

def Anderson4D.primitiveGenericDyadicRHS (C : ℝ) (n M : ℕ) (t : PlaneTree) : ℝ

The exact independent-gap majorant obtained from the injective marking code. No endpoint refinement has yet been used in this expression.

Equations

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

theorem Anderson4D.primitiveMarkingRatioSum_le_genericDyadic {C : ℝ} (hC : 0 ≤ C) {n M : ℕ} {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) : primitiveMarkingRatioSum C n M t ≤ primitiveGenericDyadicRHS C n M t

Genuine valid markings inject into the independent root/free/gap coordinates. This is the complete non-endpoint part of (5.17).

theorem Anderson4D.primitiveGenericDyadicRHS_le_factorialLog_of_card_lt {C : ℝ} (hC : 0 ≤ C) {n M K : ℕ} {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (mu : t.Multiplicities) (hn : 2 ≤ n) (htotal : totalMultiplicity mu = 2 * n) (hcard : (nonrootBranches t).card < n - 2) (hnL : n ≤ K * (Nat.log 2 (4 * M) + 1)) : primitiveGenericDyadicRHS C n M t ≤ C ^ n * 2 ^ (nonrootBranches t).card * ((16 * (↑K + 1)) ^ n * ↑(Nat.log 2 (4 * M) + 1) ^ (n - 2))

Away from the unique extremal case |B \\ {r}| = n-2, the generic marking code already gives the refined exponent min(|W|+1,n-2) used after (5.17).

The one constrained coordinate in the endpoint refinement

@[reducible, inline]

abbrev Anderson4D.ConstrainedValidBranchExponentData (t : PlaneTree) (bound : ℕ) (anchor : ↥t.BranchNodes) (allowed : Finset (Fin (bound + 1))) : Type

Valid branch data whose exponent at anchor lies in a prescribed finite set. The endpoint geometry will supply a set of cardinality O(log n) (and hence O(C^n)) in the unique extremal case of (5.17).

Equations

• Anderson4D.ConstrainedValidBranchExponentData t bound anchor allowed = { N : Anderson4D.ValidBranchExponentData t bound // ↑N anchor ∈ allowed }

@[reducible, inline]

abbrev Anderson4D.BranchAwayFrom (t : PlaneTree) (anchor : ↥t.BranchNodes) : Type

Delete the anchored branch coordinate.

Equations

• Anderson4D.BranchAwayFrom t anchor = { v : ↥t.BranchNodes // v ≠ anchor }

def Anderson4D.constrainedBranchExponentCode {t : PlaneTree} {bound : ℕ} {anchor : ↥t.BranchNodes} {allowed : Finset (Fin (bound + 1))} (N : ConstrainedValidBranchExponentData t bound anchor allowed) : ↥allowed × (BranchAwayFrom t anchor → Fin (bound + 1))

An anchored marking is encoded by its allowed anchor exponent and all remaining branch exponents.

Equations

• Anderson4D.constrainedBranchExponentCode N = (⟨↑↑N anchor, ⋯⟩, fun (v : Anderson4D.BranchAwayFrom t anchor) => ↑↑N ↑v)

theorem Anderson4D.constrainedBranchExponentCode_injective {t : PlaneTree} {bound : ℕ} {anchor : ↥t.BranchNodes} {allowed : Finset (Fin (bound + 1))} : Function.Injective constrainedBranchExponentCode

theorem Anderson4D.card_constrainedValidBranchExponentData_le {t : PlaneTree} (bound : ℕ) (anchor : ↥t.BranchNodes) (allowed : Finset (Fin (bound + 1))) : Fintype.card (ConstrainedValidBranchExponentData t bound anchor allowed) ≤ allowed.card * (bound + 1) ^ (t.BranchNodes.card - 1)

Fixing one branch exponent removes one full logarithmic coordinate. This is the finite counting lemma needed in the top W = B \\ {r} case.

Geometry of the fixed endpoint coordinate

noncomputable def Anderson4D.endpointExponentFinset {t : PlaneTree} (bound : ℕ) (x₀ x₁ : Z4) : Finset (Fin (bound + 1))

Exponents compatible with the two-sided admissibility comparison for a fixed pair of endpoint values.

Equations

• Anderson4D.endpointExponentFinset bound x₀ x₁ = {e : Fin (bound + 1) | ↑(2 ^ ↑e) / 2 ≤ Anderson4D.znorm (x₀ - x₁) ∧ Anderson4D.znorm (x₀ - x₁) ≤ 2 * ↑t.leafCount * ↑(2 ^ ↑e)}

theorem Anderson4D.card_endpointExponentFinset_le {t : PlaneTree} (bound : ℕ) (x₀ x₁ : Z4) : (endpointExponentFinset bound x₀ x₁).card ≤ 4 * t.leafCount + 1

The endpoint window contains at most linearly many dyadic exponents. The paper only needs an exponential-in-leafCount bound; this elementary linear estimate is deliberately stronger and avoids any analytic logarithm comparison.

theorem Anderson4D.branchExponent_mem_endpointExponentFinset {t : PlaneTree} (ht : t.isValid = true) {bound M : ℕ} (N : ValidBranchExponentData t bound) (anchor : ↥t.BranchNodes) (f₀ f₁ : HeppLeaf t) (hf : f₀ ≠ f₁) (hanchor : ↑anchor = lcaV ↑f₀ ↑f₁) (z : HeppLeaf t → Z4) (hadm : IsAdmissible ((↑N).toHeppMarking ⋯) M z) : ↑N anchor ∈ endpointExponentFinset bound (z f₀) (z f₁)

A genuine admissible embedding with fixed distinct endpoint leaves forces the LCA exponent into endpointExponentFinset. The lower inequality is Definition 5.4(a); the upper one is the cluster-diameter bound used in the proof of Proposition 5.6.

@[reducible, inline]

abbrev Anderson4D.EndpointValidBranchExponentData (t : PlaneTree) (bound M : ℕ) (f₀ f₁ : HeppLeaf t) (x₀ x₁ : Z4) : Type

Valid logarithmic branch data admitting an embedding with the two chosen leaves fixed at x₀,x₁.

Equations

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

@[implicit_reducible]

noncomputable instance Anderson4D.instFintypeEndpointValidBranchExponentData (t : PlaneTree) (bound M : ℕ) (f₀ f₁ : HeppLeaf t) (x₀ x₁ : Z4) : Fintype (EndpointValidBranchExponentData t bound M f₀ f₁ x₀ x₁)

Equations

• Anderson4D.instFintypeEndpointValidBranchExponentData t bound M f₀ f₁ x₀ x₁ = Fintype.ofFinite (Anderson4D.EndpointValidBranchExponentData t bound M f₀ f₁ x₀ x₁)

def Anderson4D.endpointDataToConstrained {t : PlaneTree} (ht : t.isValid = true) {bound M : ℕ} (anchor : ↥t.BranchNodes) (f₀ f₁ : HeppLeaf t) (hf : f₀ ≠ f₁) (hanchor : ↑anchor = lcaV ↑f₀ ↑f₁) (x₀ x₁ : Z4) (N : EndpointValidBranchExponentData t bound M f₀ f₁ x₀ x₁) : ConstrainedValidBranchExponentData t bound anchor (endpointExponentFinset bound x₀ x₁)

Forget the endpoint witness while retaining the constrained LCA coordinate.

Equations

• Anderson4D.endpointDataToConstrained ht anchor f₀ f₁ hf hanchor x₀ x₁ N = ⟨↑N, ⋯⟩

theorem Anderson4D.endpointDataToConstrained_injective {t : PlaneTree} (ht : t.isValid = true) {bound M : ℕ} (anchor : ↥t.BranchNodes) (f₀ f₁ : HeppLeaf t) (hf : f₀ ≠ f₁) (hanchor : ↑anchor = lcaV ↑f₀ ↑f₁) (x₀ x₁ : Z4) : Function.Injective (endpointDataToConstrained ht anchor f₀ f₁ hf hanchor x₀ x₁)

theorem Anderson4D.card_endpointValidBranchExponentData_le {t : PlaneTree} (ht : t.isValid = true) {bound M : ℕ} (anchor : ↥t.BranchNodes) (f₀ f₁ : HeppLeaf t) (hf : f₀ ≠ f₁) (hanchor : ↑anchor = lcaV ↑f₀ ↑f₁) (x₀ x₁ : Z4) : Fintype.card (EndpointValidBranchExponentData t bound M f₀ f₁ x₀ x₁) ≤ (endpointExponentFinset bound x₀ x₁).card * (bound + 1) ^ (t.BranchNodes.card - 1)

The fixed endpoints remove one logarithmic marking coordinate. The only residual cost is the number of dyadic exponents in the geometric window; the next numerical step absorbs that cardinality exponentially.

theorem Anderson4D.sum_endpointValidBranchExponentData_parentScaleRatio_le {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) {n M : ℕ} (hbranchCard : (nonrootBranches t).card = n - 2) (anchor : ↥t.BranchNodes) (f₀ f₁ : HeppLeaf t) (hf : f₀ ≠ f₁) (hanchor : ↑anchor = lcaV ↑f₀ ↑f₁) (x₀ x₁ : Z4) (W : Finset t.VPos) (hW : W ⊆ nonrootBranches t) : ∑ N : EndpointValidBranchExponentData t (Nat.log 2 (4 * M)) M f₀ f₁ x₀ x₁, ∏ v ∈ nonrootBranches t \ W, parentScaleRatio ((↑↑N).toHeppMarking ⋯) v ≤ ↑(4 * t.leafCount + 1) * (↑(Nat.log 2 (4 * M) + 1) ^ min (W.card + 1) (n - 2) * 2 ^ ((nonrootBranches t).card - W.card))

Fixed endpoints give the paper's refined exponent min(|W|+1,n-2) for every powerset term. The unique top term uses the constrained LCA coordinate; all proper subsets inject into the unrestricted marking carrier.

Endpoint-refined summation of (5.16)--(5.17)

noncomputable def Anderson4D.primitiveEndpointMarkingRatioSum (C : ℝ) (n M : ℕ) (t : PlaneTree) (f₀ f₁ : HeppLeaf t) (x₀ x₁ : Z4) : ℝ

The (5.16) marking sum restricted to markings which genuinely realize the two fixed endpoint values at two fixed distinct leaves.

Equations

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

theorem Anderson4D.primitiveEndpointMarkingRatioSum_le_refinedDyadic {C : ℝ} (hC : 0 ≤ C) {n M : ℕ} {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (hbranchCard : (nonrootBranches t).card = n - 2) (anchor : ↥t.BranchNodes) (f₀ f₁ : HeppLeaf t) (hf : f₀ ≠ f₁) (hanchor : ↑anchor = lcaV ↑f₀ ↑f₁) (x₀ x₁ : Z4) : primitiveEndpointMarkingRatioSum C n M t f₀ f₁ x₀ x₁ ≤ C ^ n * ↑(4 * t.leafCount + 1) * ∑ W ∈ (nonrootBranches t).powerset, ↑(n - W.card).factorial * (↑(Nat.log 2 (4 * M) + 1) ^ min (W.card + 1) (n - 2) * 2 ^ ((nonrootBranches t).card - W.card))

In the extremal tree, the complete endpoint-valid marking sum has the refined exponent min(|W|+1,n-2) term by term.

theorem Anderson4D.primitiveEndpointMarkingRatioSum_le_factorialLog {C : ℝ} (hC : 0 ≤ C) {n M K : ℕ} {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (mu : t.Multiplicities) (hn : 2 ≤ n) (htotal : totalMultiplicity mu = 2 * n) (hnL : n ≤ K * (Nat.log 2 (4 * M) + 1)) (hbranchCard : (nonrootBranches t).card = n - 2) (anchor : ↥t.BranchNodes) (f₀ f₁ : HeppLeaf t) (hf : f₀ ≠ f₁) (hanchor : ↑anchor = lcaV ↑f₀ ↑f₁) (x₀ x₁ : Z4) : primitiveEndpointMarkingRatioSum C n M t f₀ f₁ x₀ x₁ ≤ C ^ n * ↑(4 * t.leafCount + 1) * 2 ^ (nonrootBranches t).card * ((16 * (↑K + 1)) ^ n * ↑(Nat.log 2 (4 * M) + 1) ^ (n - 2))

Pulling the residual geometric-series factors out of the refined powerset sum costs at most 2^|B\{r}|.

theorem Anderson4D.primitiveMarkingRatioSum_le_final_of_card_lt {C : ℝ} (hC : 0 ≤ C) {n M K : ℕ} {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (mu : t.Multiplicities) (hn : 2 ≤ n) (htotal : totalMultiplicity mu = 2 * n) (hcard : (nonrootBranches t).card < n - 2) (hnL : n ≤ K * (Nat.log 2 (4 * M) + 1)) : primitiveMarkingRatioSum C n M t ≤ (32 * C * (↑K + 1)) ^ n * ↑(Nat.log 2 (4 * M) + 1) ^ (n - 2)

Non-extremal form of the complete numerical marking assembly: the unrestricted marking carrier already has at most n-2 logarithmic coordinates, and every residual finite factor is absorbed into the displayed exponential base.

theorem Anderson4D.primitiveEndpointMarkingRatioSum_le_final_of_card_eq {C : ℝ} (hC : 0 ≤ C) {n M K : ℕ} {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (mu : t.Multiplicities) (hn : 2 ≤ n) (htotal : totalMultiplicity mu = 2 * n) (hnL : n ≤ K * (Nat.log 2 (4 * M) + 1)) (hbranchCard : (nonrootBranches t).card = n - 2) (anchor : ↥t.BranchNodes) (f₀ f₁ : HeppLeaf t) (hf : f₀ ≠ f₁) (hanchor : ↑anchor = lcaV ↑f₀ ↑f₁) (x₀ x₁ : Z4) : primitiveEndpointMarkingRatioSum C n M t f₀ f₁ x₀ x₁ ≤ (256 * C * (↑K + 1)) ^ n * ↑(Nat.log 2 (4 * M) + 1) ^ (n - 2)

Extremal endpoint form of the complete numerical marking assembly. The one LCA scale constrained by the fixed endpoint values replaces the otherwise extra logarithm; all polynomial and geometric losses are absorbed into the explicit base 256*C*(K+1).

One-datum P-5.6/P-5.7 lattice assembly

def Anderson4D.primitiveTupleDiameterBracketSq {m : ℕ} (hm : 0 < m) (y : Fin m → Z4) : ℝ

The maximum lattice bracket on a nonempty tuple. Unlike the earlier latticeTupleDiameterBracketSq, this form is indexed by Fin m directly, which is the carrier used by the paired-incidence layer.

Equations

• Anderson4D.primitiveTupleDiameterBracketSq hm y = Finset.univ.sup' ⋯ fun (i : Fin m) => Finset.univ.sup' ⋯ fun (j : Fin m) => Anderson4D.latticeBracketSq (y i) (y j)

theorem Anderson4D.primitiveTupleDiameterBracketSq_nonneg {m : ℕ} (hm : 0 < m) (y : Fin m → Z4) : 0 ≤ primitiveTupleDiameterBracketSq hm y

theorem Anderson4D.primitiveTupleDiameterBracketSq_le_rootScale {t : PlaneTree} (ht : t.isValid = true) {m M : ℕ} (hm : 0 < m) {Nm : t.HeppMarking} {mu : t.Multiplicities} {y : Fin m → Z4} (hreal : RealizesTuple t Nm mu M y) : primitiveTupleDiameterBracketSq hm y ≤ (1 + 2 * ↑t.leafCount) ^ 2 * ↑(scaleN Nm t.rootV) ^ 2

Root-cluster control of the actual maximum bracket on the paired tuple carrier.

theorem Anderson4D.primitive_lattice_estimate {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))) (hn : 2 ≤ n) (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (hYreal : ∀ y ∈ Y, PairedDataRealizes d y) (y : Fin (2 * n) → Z4) (hyreal : PairedDataRealizes d y) (κ : AcrossPairing A) (hκ : RespectsWord A y κ) (x₀ x₁ : Z4) : ↑(realizedSetsContainingPair (↑d).1 ⋯ x₀ x₁).card / ↑(pairedTreeSymDenom t M (2 * n) y) * primitiveTupleDiameterBracketSq ⋯ y * ∑ p : PositiveAssignment (↥Z) (2 * n), ∑ w ∈ inducedWordsAtProfile Y Z p, ↑(primitiveCompatibleAcrossPairings A w).card * supportChainWeight w ≤ volumeEstimateFinalConstant ^ t.leafCount * (1 + 2 * ↑t.leafCount) ^ 2 * latticeBracketInvFourth x₀ x₁ * primitiveRatioRHS (4 * C) n t (pairedMarking d)

Fixed-data lattice assembly for R-4.1pf.

For one paired incidence datum, the actual maximum bracket and the complete primitive pairing/profile chain sum are bounded by P-5.6 and P-5.7. The branch-volume and root-scale monomials cancel exactly, leaving the (5.16) parent-ratio expression.