Primitive-pairing assembly at lattice level

This file joins the exact finite objects which occur between paper (5.5) and (5.17).

The first part is a genuine master bridge. For a fixed cut A, the primitive across-pairing lattice sum is covered by valid Hepp trees and then reindexed by the paired finite incidence denominator from (5.6). No realization or positivity hypothesis is hidden in that statement.

The remaining lemmas expose three independent estimates used after this reindexing:

• Proposition 5.6 cancels the paired incidence denominator against the marked-tree orbit factor;
• Proposition 5.7 controls the primitive compatible word sum;
• the root cluster diameter pays for the maximum in (5.5), and the numerical powerset lemma closes (5.17).

There are exactly two reindexing steps not supplied by the current library:

1. grouping a fixed paired incidence fiber by its unlabelled realized set and the induced multiplicity word (the paper's passage (5.8)--(5.11));
2. reindexing valid increasing branch markings by independent dyadic gaps before applying sum_dyadicAssignmentWeight_le.

They are not replaced here by assumptions equivalent to the desired bound.

Primitive across pairings and the actual lattice statistic

def Anderson4D.primitiveAcrossPairingFinset {m : ℕ} (A : Finset (Fin m)) : Finset (AcrossPairing A)

Primitive pairings crossing the fixed paper cut A | Aᶜ.

Equations

• Anderson4D.primitiveAcrossPairingFinset A = Finset.filter (Anderson4D.IsPrimitiveAcross A) Finset.univ

@[simp]

theorem Anderson4D.mem_primitiveAcrossPairingFinset {m : ℕ} {A : Finset (Fin m)} {κ : AcrossPairing A} : κ ∈ primitiveAcrossPairingFinset A ↔ IsPrimitiveAcross A κ

noncomputable def Anderson4D.pairedReductionStatistic (q : ℕ) (A : Finset (Fin (q + 1))) (κ : AcrossPairing A) (y : Fin (q + 1) → Z4) : ℝ

The (5.5) lattice weight restricted to assignments copied along one across pairing.

Equations

• Anderson4D.pairedReductionStatistic q A κ y = if Anderson4D.RespectsWord A y κ then Anderson4D.reductionWeight q y else 0

theorem Anderson4D.pairedReductionStatistic_nonneg (q : ℕ) (A : Finset (Fin (q + 1))) (κ : AcrossPairing A) (y : Fin (q + 1) → Z4) : 0 ≤ pairedReductionStatistic q A κ y

theorem Anderson4D.respectsPairing_acrossToPartialPairing_iff {m : ℕ} (A : Finset (Fin m)) (κ : AcrossPairing A) (y : Fin m → Z4) : RespectsPairing (acrossToPartialPairing A κ) y ↔ RespectsWord A y κ

The copied-cell predicate produced by Discretization is exactly the across-word predicate used by the pairing and incidence layers. The two definitions write the same equality in opposite orientations.

noncomputable def Anderson4D.primitiveAcrossLatticeSum (M q : ℕ) (A : Finset (Fin (q + 1))) : ℝ

The sum over the primitive pairings crossing a fixed cut. This is the finite lattice expression obtained from (5.5) before choosing a Hepp tree.

Equations

• Anderson4D.primitiveAcrossLatticeSum M q A = ∑ κ ∈ Anderson4D.primitiveAcrossPairingFinset A, Anderson4D.latticeChainSum M (q + 1) (Anderson4D.pairedReductionStatistic q A κ)

def Anderson4D.compatiblePrimitiveAcrossPairings {m : ℕ} (A : Finset (Fin m)) (y : Fin m → Z4) : Finset (AcrossPairing A)

Primitive across pairings compatible with one lattice tuple. Unlike the generic word carrier, this definition does not impose a spurious finiteness assumption on the lattice alphabet Z4.

Equations

• Anderson4D.compatiblePrimitiveAcrossPairings A y = {κ ∈ Anderson4D.primitiveAcrossPairingFinset A | Anderson4D.RespectsWord A y κ}

@[simp]

theorem Anderson4D.mem_compatiblePrimitiveAcrossPairings {m : ℕ} {A : Finset (Fin m)} {y : Fin m → Z4} {κ : AcrossPairing A} : κ ∈ compatiblePrimitiveAcrossPairings A y ↔ IsPrimitiveAcross A κ ∧ RespectsWord A y κ

theorem Anderson4D.primitiveAcrossLatticeSum_eq_pairingCount (M q : ℕ) (A : Finset (Fin (q + 1))) : primitiveAcrossLatticeSum M q A = latticeChainSum M (q + 1) fun (y : Fin (q + 1) → Fin 4 → ℤ) => ↑(compatiblePrimitiveAcrossPairings A y).card * reductionWeight q y

Finite Fubini form of the primitive lattice sum: at each tuple the pairing multiplicity is exactly the number of compatible primitive across pairings.

theorem Anderson4D.mem_repeatedTuples_of_respectsAcross (M q : ℕ) (A : Finset (Fin (q + 1))) (κ : AcrossPairing A) (y : Fin (q + 1) → Z4) (hy : y ∈ rdec_boundedTuples M (q + 1)) (hκ : RespectsWord A y κ) : y ∈ rdec_repeatedTuples M (q + 1)

A copied assignment lies in the repeated-value locus required by the weak tree cover.

A fixed tree slice has paired finite incidence data

noncomputable def Anderson4D.pairedTreeSlice (t : PlaneTree) (M q : ℕ) (A : Finset (Fin (q + 1))) (κ : AcrossPairing A) : Finset (Fin (q + 1) → Z4)

The fixed-tree assignments compatible with one across pairing.

Equations

• Anderson4D.pairedTreeSlice t M q A κ = {y ∈ Anderson4D.rdec_treeRealized t M (q + 1) | Anderson4D.RespectsWord A y κ}

@[simp]

theorem Anderson4D.mem_pairedTreeSlice {t : PlaneTree} {M q : ℕ} {A : Finset (Fin (q + 1))} {κ : AcrossPairing A} {y : Fin (q + 1) → Z4} : y ∈ pairedTreeSlice t M q A κ ↔ y ∈ rdec_treeRealized t M (q + 1) ∧ RespectsWord A y κ

theorem Anderson4D.exists_pairedData_realizes_of_mem_pairedTreeSlice {t : PlaneTree} (ht : t.isValid = true) {M q : ℕ} {A : Finset (Fin (q + 1))} {κ : AcrossPairing A} {y : Fin (q + 1) → Z4} (hy : y ∈ pairedTreeSlice t M q A κ) : ∃ (d : t.PairedValidRealizationData M (q + 1)), PairedDataRealizes d y

A realization of a copied assignment by a fixed valid tree determines an element of that tree's paired finite denominator carrier.

theorem Anderson4D.sum_pairedTreeSlice_eq_paired_incidence {t : PlaneTree} (ht : t.isValid = true) (M q : ℕ) (A : Finset (Fin (q + 1))) (κ : AcrossPairing A) : ∑ y ∈ rdec_treeRealized t M (q + 1), pairedReductionStatistic q A κ y = ∑ d ∈ pairedValidRealizationDataFinset t M (q + 1), ∑ y ∈ pairedTreeSlice t M q A κ with PairedDataRealizes d y, reductionWeight q y / ↑(pairedTreeSymDenom t M (q + 1) y)

Exact fixed-tree form of paper (5.6), now on the actual (5.5) weight and the even-multiplicity denominator.

noncomputable def Anderson4D.primitiveTreeIncidenceSum (M q : ℕ) (A : Finset (Fin (q + 1))) : ℝ

The exact tree-and-incidence expression on the right of the master bridge.

Equations

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

theorem Anderson4D.primitiveAcrossLatticeSum_le_treeIncidence (M q : ℕ) (A : Finset (Fin (q + 1))) : primitiveAcrossLatticeSum M q A ≤ primitiveTreeIncidenceSum M q A

Master lattice/incidence bridge for (5.5)--(5.6).

The proof uses the Hepp-tree cover only after showing from the fixed across pairing that every contributing tuple has repeated values. Each valid tree slice is then reindexed by the exact paired denominator.

Exact pointwise bridge from (5.5) to the Proposition 5.7 weight

def Anderson4D.latticeTupleDiameterBracketSq {m : ℕ} (y : Fin (m + 1) → Z4) : ℝ

The maximum factor in the lattice summand (5.5).

Equations

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

theorem Anderson4D.reductionWeight_eq_diameter_mul_heppChainWeight {t : PlaneTree} {m M : ℕ} {Nm : t.HeppMarking} {mu : t.Multiplicities} {y : Fin (m + 1) → Z4} (hreal : RealizesTuple t Nm mu M y) : ∃ (z : HeppLeaf t → Z4) (w : Fin (m + 1) → HeppLeaf t), IsAdmissible Nm M z ∧ w ∈ validWords (leafMultiplicity mu) ∧ reductionWeight m y = latticeTupleDiameterBracketSq y * heppChainWeight z w

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

The root cluster diameter controls the maximum bracket factor in (5.5). The displayed constant is polynomial in the leaf count and is subsequently absorbed into the paper's exponential base.

P-5.7 and P-5.6 after the exact finite reindexing

theorem Anderson4D.primitivePairedChainSum_le_permSumRHS {C : ℝ} (hC : PermSumEstimate C) (n M : ℕ) (t : PlaneTree) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Z4) (A : Finset (Fin (2 * n))) (hn : 2 ≤ n) (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (htotal : totalMultiplicity mu = 2 * n) (heven : ∀ (l : HeppLeaf t), Even (leafMultiplicity mu l)) (hadm : IsAdmissible Nm M z) : primitivePairedWordSum (leafMultiplicity mu) A (heppChainWeight z) ≤ (∏ l : HeppLeaf t, ↑(leafMultiplicity mu l / 2).factorial / ↑(leafMultiplicity mu l).factorial) * permSumRHS C n t Nm mu

Proposition 5.7 bounds the primitive compatible across-pairing word sum with the exact factorial quotient from (5.10).

theorem Anderson4D.realizedSetsPair_div_pairedDenom_le_volume {t : PlaneTree} (ht : t.isValid = true) {M m : ℕ} (N : t.BranchExponentData (4 * M)) (hN : N.IsValid) (mu : t.Multiplicities) (y : Fin m → Z4) (hreal : RealizesTuple t (N.toHeppMarking hN) mu M y) (A : Finset (Fin m)) (κ : AcrossPairing A) (hκ : RespectsWord A y κ) (x₀ x₁ : Z4) : ↑(realizedSetsContainingPair N hN x₀ x₁).card / ↑(pairedTreeSymDenom t M m y) ≤ volumeEstimateFinalConstant ^ t.leafCount * branchScaleProduct (N.toHeppMarking hN) * latticeBracketInvFourth x₀ x₁

Proposition 5.6 cancels the paired incidence denominator and the marked automorphism factor. This is the precise algebra used between (5.12), (5.14), and (5.16).

The final (5.17) numerical ledger on an actual tree

@[reducible, inline]

abbrev Anderson4D.NonrootBranch (t : PlaneTree) : Type

Actual non-root branch carrier used when independent dyadic gaps are summed after the marking reindexing.

Equations

• Anderson4D.NonrootBranch t = ↥(Anderson4D.nonrootBranches t)

theorem Anderson4D.sum_nonrootBranch_dyadicAssignmentWeight_le (t : PlaneTree) (L : ℕ) (free : Finset (NonrootBranch t)) : ∑ a : NonrootBranch t → Fin L, dyadicAssignmentWeight L free a ≤ ↑L ^ free.card * 2 ^ ((nonrootBranches t).card - free.card)

Tree-carrier specialization of the factorized dyadic summation. Once a valid increasing marking has been injected into independent gap data, every free branch costs L and every other branch costs at most 2.

theorem Anderson4D.card_nonrootBranches_le_order_sub_two {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (mu : t.Multiplicities) (n : ℕ) (htotal : totalMultiplicity mu = 2 * n) : (nonrootBranches t).card ≤ n - 2

A valid tree with total multiplicity 2n has at most n-2 non-root branch nodes.

theorem Anderson4D.tree_sum_factorial_log_balance {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (mu : t.Multiplicities) (n L K : ℕ) (hn : 2 ≤ n) (htotal : totalMultiplicity mu = 2 * n) (hnL : n ≤ K * L) : ∑ W ∈ (nonrootBranches t).powerset, ↑(n - W.card).factorial * ↑L ^ min (W.card + 1) (n - 2) ≤ (16 * (↑K + 1)) ^ n * ↑L ^ (n - 2)

Tree-indexed form of the factorial/logarithm summation after (5.17).