Lattice-level assembly after Proposition 5.7

This file records the elementary scale-summation and factorial/logarithm ledger used at the end of paper §5.2, equations (5.16)--(5.17). The geometric tree summation and the continuum discretization are kept as separate interfaces; the lemma below closes the final numerical step without hiding its uniform exponential constant.

Independent dyadic-scale summation

noncomputable def Anderson4D.dyadicAssignmentWeight {ι : Type u_1} [Fintype ι] [DecidableEq ι] (L : ℕ) (free : Finset ι) (a : ι → Fin L) : ℝ

Product weight obtained after summing a Hepp marking from the leaves toward the root. Coordinates in free carry the logarithmic loss; every other coordinate carries a summable dyadic gap. This is the factorized majorant behind paper (5.17).

Equations

• Anderson4D.dyadicAssignmentWeight L free a = ∏ i : ι, if i ∈ free then 1 else (1 / 2) ^ ↑(a i)

theorem Anderson4D.sum_dyadicAssignmentWeight_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (L : ℕ) (free : Finset ι) : ∑ a : ι → Fin L, dyadicAssignmentWeight L free a ≤ ↑L ^ free.card * 2 ^ (Fintype.card ι - free.card)

Factorized geometric summation in (5.17). Each unrestricted scale costs L, whereas a scale carrying a parent-ratio factor costs at most the geometric constant 2. The actual increasing-marking domain injects into this independent gap domain, so this is the reusable numerical estimate consumed by the tree-specific assembly.

The factorial--logarithm balance

theorem Anderson4D.cube_le_eight_pow (k : ℕ) : k ^ 3 ≤ 8 ^ k

A deliberately coarse exponential envelope for the cubic residue in the factorial/logarithm balance.

theorem Anderson4D.factorial_log_balance_nat (n s L K : ℕ) (hn : 2 ≤ n) (hs : s ≤ n - 2) (hnL : n ≤ K * L) : (n - s).factorial * L ^ min (s + 1) (n - 2) ≤ (8 * (K + 1)) ^ n * L ^ (n - 2)

The elementary inequality after (5.17), natural-scale form.

If the perturbative order satisfies n ≤ K L, then, uniformly for 0 ≤ s ≤ n-2,

(n-s)! L^min(s+1,n-2) ≤ (8 (K+1))^n L^(n-2).

Here L is the number of available dyadic scales (later comparable to |log ε|). The proof separates the endpoint cases n-s ≤ 3; away from them, exactly n-s-3 powers of L pay for the factorial, while the cubic residue is absorbed by 8^n.

theorem Anderson4D.factorial_log_balance (n s L K : ℕ) (hn : 2 ≤ n) (hs : s ≤ n - 2) (hnL : n ≤ K * L) : ↑(n - s).factorial * ↑L ^ min (s + 1) (n - 2) ≤ (8 * (↑K + 1)) ^ n * ↑L ^ (n - 2)

Real-valued form used by the analytic assembly. It is an exact cast of factorial_log_balance_nat, so no Archimedean or asymptotic argument is left implicit.

theorem Anderson4D.sum_factorial_log_balance {α : Type u_1} [DecidableEq α] (B : Finset α) (n L K : ℕ) (hn : 2 ≤ n) (hB : B.card ≤ n - 2) (hnL : n ≤ K * L) : ∑ W ∈ B.powerset, ↑(n - W.card).factorial * ↑L ^ min (W.card + 1) (n - 2) ≤ (16 * (↑K + 1)) ^ n * ↑L ^ (n - 2)

Powerset-summed form of the final estimate after (5.17). The hypothesis B.card ≤ n-2 is the paper's |B|-1 ≤ r-2 ≤ n-2 after removing the root. The number of choices of W costs at most 2ⁿ, absorbed into the displayed base 16(K+1).