Capped cross ledger, part 2: the order-three calibration

After the Parseval collapse the pure-cross entity of a bijection σ is the zero-sum lattice sum

I(σ) = Σ_{k₁+…+k_m=0} ∏ᵢ ‖ρ̂(εkᵢ)‖² ∏_{j<m} ⟨Sⱼ⟩⁻²⟨Tⱼ^σ⟩⁻²,

Sⱼ = k₁+…+kⱼ (identity-order partial sums, one propagator per internal edge of the left Green chain) and Tⱼ^σ the same partial sums taken in σ order (right chain). There are m-1 free momenta and 2(m-1) quadratic propagators: the sum is log-critical, so each free momentum contributes at most one factor L = |log ε|, and only when the propagators covering it are doubled (or critically entangled).

The m = 3 table (proved here, uniformly in σ)

At m = 3, S₁ = k₁, S₂ = -k₃, T₁ = k_{τ1}, T₂ = -k_{τ3} with τ = σ⁻¹, so the propagator multiset of σ is determined by the pair (i,j) = (τ1, τ3):

τ = σ⁻¹	(i,j)	propagators	order
id	(1,3)	⟨k₁⟩⁻⁴⟨k₃⟩⁻⁴	L²
(1 2)	(2,3)	⟨k₁⟩⁻²⟨k₂⟩⁻²⟨k₃⟩⁻⁴	L²
(2 3)	(1,2)	⟨k₁⟩⁻⁴⟨k₂⟩⁻²⟨k₃⟩⁻²	L²
(1 3)	(3,1)	⟨k₁⟩⁻⁴⟨k₃⟩⁻⁴	L²
(1 2 3)	(2,1)	⟨k₁⟩⁻⁴⟨k₂⟩⁻²⟨k₃⟩⁻²	L²
(1 3 2)	(3,2)	⟨k₁⟩⁻²⟨k₂⟩⁻²⟨k₃⟩⁻⁴	L²

r324CC_exists_latticeThree_le_log_sq proves the upper half of the table for all six patterns at once: the arithmetic-geometric split ab ≤ (a²+b²)/2 applied to a = ⟨S₁⟩⁻²⟨S₂⟩⁻², b = ⟨T₁⟩⁻²⟨T₂⟩⁻² reduces every pattern to a pair of doubled propagators at two distinct modes, and each of the three possible pairs (k₁,k₂), (k₁,k₃), (k₂,k₃) iterates into two proved translated windows Σ_k ‖ρ̂(εk)‖²⟨k+γ⟩⁻⁴ ≤ C·L (r324SW_translated_window_le_log) — the shift γ of the inner window being the outer summation variable. The matching lower half is the classical dyadic count Σ_{|s|≤N}⟨s⟩⁻⁴ log(N/⟨s⟩) ≍ (log N)², so every order-three entity is exactly of order L² = L^{m-1}: at m = 3 all six entities have the same grade, and the grading is neither available nor needed — the count 3! = 6 is itself geometric (r324CappedCrossLedgerAt_three_of_entityBoundAt).

The first strict grade drop is at m = 4: τ = (2,4,1,3) gives propagators ⟨k₁⟩⁻²⟨k₁+k₂⟩⁻²⟨k₄⟩⁻²⟨k₂⟩⁻²⟨k₂+k₄⟩⁻²⟨k₃⟩⁻² in three free momenta with no critical proper subspace (every lattice line carries ≥ 3 quadratic propagators), hence order L¹, not L³.

Conditional order-three physical-to-lattice collapse

R324CappedCrossCollapseThree packages the physical-to-lattice comparison. Given this comparison, r324CappedCrossLedgerAt_three_of_collapse proves the order-three ledger.

At higher order the collapse alone is not enough: r324CappedCross_flatGrade_over_budget shows the flat grade m-1 (which is sharp — the identity entity saturates it) overshoots the graded-count clause for every constant, so the general-m route must go through R324CappedCrossGradingBoundAt with a non-constant grade.

Iterated window sums

theorem Anderson4D.r324CC_tsum_prod_le {f : Z4 → ℝ} {g : Z4 → Z4 → ℝ} {A B : ℝ} (hf0 : ∀ (k : Z4), 0 ≤ f k) (hg0 : ∀ (k l : Z4), 0 ≤ g k l) (hfs : Summable f) (hgs : ∀ (k : Z4), Summable (g k)) (hB : 0 ≤ B) (hf : ∑' (k : Z4), f k ≤ A) (hg : ∀ (k : Z4), ∑' (l : Z4), g k l ≤ B) : ∑' (p : Z4 × Z4), f p.1 * g p.1 p.2 ≤ A * B

Iterated summation for a two-variable nonnegative lattice family. If the outer family sums to ≤ A and every inner slice sums to ≤ B, the product family over Z4 × Z4 sums to ≤ A·B.

theorem Anderson4D.r324CC_tsum_prod_snd_le {f : Z4 → ℝ} {g : Z4 → Z4 → ℝ} {A B : ℝ} (hf0 : ∀ (k : Z4), 0 ≤ f k) (hg0 : ∀ (k l : Z4), 0 ≤ g k l) (hfs : Summable f) (hgs : ∀ (k : Z4), Summable (g k)) (hB : 0 ≤ B) (hf : ∑' (k : Z4), f k ≤ A) (hg : ∀ (k : Z4), ∑' (l : Z4), g k l ≤ B) : ∑' (p : Z4 × Z4), f p.2 * g p.2 p.1 ≤ A * B

Mirrored iterated summation (outer variable in the second slot).

theorem Anderson4D.r324CC_summable_prod {f : Z4 → ℝ} {g : Z4 → Z4 → ℝ} {B : ℝ} (hf0 : ∀ (k : Z4), 0 ≤ f k) (hg0 : ∀ (k l : Z4), 0 ≤ g k l) (hfs : Summable f) (hgs : ∀ (k : Z4), Summable (g k)) (_hB : 0 ≤ B) (hg : ∀ (k : Z4), ∑' (l : Z4), g k l ≤ B) : Summable fun (p : Z4 × Z4) => f p.1 * g p.1 p.2

theorem Anderson4D.r324CC_summable_prod_snd {f : Z4 → ℝ} {g : Z4 → Z4 → ℝ} {B : ℝ} (hf0 : ∀ (k : Z4), 0 ≤ f k) (hg0 : ∀ (k l : Z4), 0 ≤ g k l) (hfs : Summable f) (hgs : ∀ (k : Z4), Summable (g k)) (hB : 0 ≤ B) (hg : ∀ (k : Z4), ∑' (l : Z4), g k l ≤ B) : Summable fun (p : Z4 × Z4) => f p.2 * g p.2 p.1

The collapsed order-three lattice sums

noncomputable def Anderson4D.r324CCbrk (k : Z4) : ℝ

The Japanese bracket ⟨k⟩⁻² of the paper's Green propagator.

Equations

• Anderson4D.r324CCbrk k = (1 + Anderson4D.paperModeNormSq k)⁻¹

noncomputable def Anderson4D.r324CCsym (ρ : SmoothCutoff) (ε : ℝ) (k : Z4) : ℝ

The symbol weight ‖ρ̂(εk)‖² of one cross leg.

Equations

• Anderson4D.r324CCsym ρ ε k = ‖ρ.symbol ε k‖ ^ 2

noncomputable def Anderson4D.r324CCwin (ρ : SmoothCutoff) (ε : ℝ) (γ k : Z4) : ℝ

The ε-window family with shift γ: the exact summand of the proved translated-window estimate.

Equations

• Anderson4D.r324CCwin ρ ε γ k = Anderson4D.r324CCsym ρ ε k * Anderson4D.r324CCbrk (k + γ) ^ 2

def Anderson4D.r324CCmode (i : Fin 3) (p : Z4 × Z4) : Z4

The three cross momenta of an order-three all-cross entity, as functions of the two free lattice variables; k₃ = -(k₁+k₂) is the zero-sum constraint left by the two external Green legs.

Equations

• Anderson4D.r324CCmode i p = if i = 0 then p.1 else if i = 1 then p.2 else -(p.1 + p.2)

@[simp]

theorem Anderson4D.r324CCmode_zero (p : Z4 × Z4) : r324CCmode 0 p = p.1

@[simp]

theorem Anderson4D.r324CCmode_one (p : Z4 × Z4) : r324CCmode 1 p = p.2

@[simp]

theorem Anderson4D.r324CCmode_two (p : Z4 × Z4) : r324CCmode 2 p = -(p.1 + p.2)

noncomputable def Anderson4D.r324CCsymWeight (ρ : SmoothCutoff) (ε : ℝ) (p : Z4 × Z4) : ℝ

The symbol weight of all three cross legs.

Equations

• Anderson4D.r324CCsymWeight ρ ε p = Anderson4D.r324CCsym ρ ε p.1 * Anderson4D.r324CCsym ρ ε p.2 * Anderson4D.r324CCsym ρ ε (-(p.1 + p.2))

noncomputable def Anderson4D.r324CCPair (ρ : SmoothCutoff) (ε : ℝ) (u w : Fin 3) (p : Z4 × Z4) : ℝ

The pair family carrying two doubled propagators at the modes u ≠ w: the resonant shape reached after the arithmetic-geometric split.

Equations

• Anderson4D.r324CCPair ρ ε u w p = Anderson4D.r324CCsymWeight ρ ε p * (Anderson4D.r324CCbrk (Anderson4D.r324CCmode u p) ^ 2 * Anderson4D.r324CCbrk (Anderson4D.r324CCmode w p) ^ 2)

noncomputable def Anderson4D.r324CCLatticeThree (ρ : SmoothCutoff) (ε : ℝ) (i j : Fin 3) : ℝ

The collapsed order-three entity value. After the Parseval collapse the entity of the bijection σ is the zero-sum lattice sum of the three symbol weights against the two identity-order propagators ⟨k₁⟩⁻²⟨k₃⟩⁻² and the two σ-order propagators ⟨k_{σ⁻¹1}⟩⁻²⟨k_{σ⁻¹3}⟩⁻²; (i,j) = (σ⁻¹1, σ⁻¹3).

Equations

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

theorem Anderson4D.r324CCbrk_nonneg (k : Z4) : 0 ≤ r324CCbrk k

theorem Anderson4D.r324CCbrk_le_one (k : Z4) : r324CCbrk k ≤ 1

theorem Anderson4D.r324CCsym_nonneg (ρ : SmoothCutoff) (ε : ℝ) (k : Z4) : 0 ≤ r324CCsym ρ ε k

theorem Anderson4D.r324CCsym_le_one (ρ : SmoothCutoff) (ε : ℝ) (k : Z4) : r324CCsym ρ ε k ≤ 1

theorem Anderson4D.r324CCwin_nonneg (ρ : SmoothCutoff) (ε : ℝ) (γ k : Z4) : 0 ≤ r324CCwin ρ ε γ k

theorem Anderson4D.r324CC_summable_win (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (γ : Z4) : Summable (r324CCwin ρ ε γ)

theorem Anderson4D.r324CCbrk_neg (k : Z4) : r324CCbrk (-k) = r324CCbrk k

theorem Anderson4D.r324CCPair_nonneg (ρ : SmoothCutoff) (ε : ℝ) (u w : Fin 3) (p : Z4 × Z4) : 0 ≤ r324CCPair ρ ε u w p

theorem Anderson4D.r324CCPair_comm (ρ : SmoothCutoff) (ε : ℝ) (u w : Fin 3) (p : Z4 × Z4) : r324CCPair ρ ε u w p = r324CCPair ρ ε w u p

The three resonant shapes

theorem Anderson4D.r324CC_prodWin_bound (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {W : ℝ} (hW0 : 0 ≤ W) (hwin : ∀ (γ : Z4), ∑' (k : Z4), r324CCwin ρ ε γ k ≤ W) (T : Z4 → Z4) : (Summable fun (p : Z4 × Z4) => r324CCwin ρ ε 0 p.1 * r324CCwin ρ ε (T p.1) p.2) ∧ ∑' (p : Z4 × Z4), r324CCwin ρ ε 0 p.1 * r324CCwin ρ ε (T p.1) p.2 ≤ W * W

Product-form majorants of the paired lattice families, and the value of the two window sums they iterate.

theorem Anderson4D.r324CC_prodWin_snd_bound (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {W : ℝ} (hW0 : 0 ≤ W) (hwin : ∀ (γ : Z4), ∑' (k : Z4), r324CCwin ρ ε γ k ≤ W) (T : Z4 → Z4) : (Summable fun (p : Z4 × Z4) => r324CCwin ρ ε 0 p.2 * r324CCwin ρ ε (T p.2) p.1) ∧ ∑' (p : Z4 × Z4), r324CCwin ρ ε 0 p.2 * r324CCwin ρ ε (T p.2) p.1 ≤ W * W

theorem Anderson4D.r324CC_le_of_majorant {F M : Z4 × Z4 → ℝ} {C : ℝ} (hF0 : ∀ (p : Z4 × Z4), 0 ≤ F p) (hFM : ∀ (p : Z4 × Z4), F p ≤ M p) (hM : Summable M) (hMb : ∑' (p : Z4 × Z4), M p ≤ C) : Summable F ∧ ∑' (p : Z4 × Z4), F p ≤ C

theorem Anderson4D.r324CC_pair_bound (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {W : ℝ} (hW0 : 0 ≤ W) (hwin : ∀ (γ : Z4), ∑' (k : Z4), r324CCwin ρ ε γ k ≤ W) {u w : Fin 3} (huw : u ≠ w) : Summable (r324CCPair ρ ε u w) ∧ ∑' (p : Z4 × Z4), r324CCPair ρ ε u w p ≤ W * W

The paired lattice sums are logarithmic squared. Two doubled propagators at distinct modes iterate into two translated windows, in one of the three resonant shapes (k₁,k₂), (k₁,k₁+k₂), (k₂,k₁+k₂).

theorem Anderson4D.r324CC_latticeThree_le (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {W : ℝ} (hW0 : 0 ≤ W) (hwin : ∀ (γ : Z4), ∑' (k : Z4), r324CCwin ρ ε γ k ≤ W) {i j : Fin 3} (hij : i ≠ j) : r324CCLatticeThree ρ ε i j ≤ W * W

The order-three calibration. Every one of the six order-three entities collapses to a lattice sum of size ≤ (C·L)²: the four propagators ⟨k₁⟩⁻²⟨k₃⟩⁻²⟨k_{σ⁻¹1}⟩⁻²⟨k_{σ⁻¹3}⟩⁻² always split, by the arithmetic-geometric inequality, into two doubled propagators at two distinct modes, and each doubled propagator is one critical translated window.

theorem Anderson4D.r324CC_exists_latticeThree_le_log_sq (ρ : SmoothCutoff) : ∃ (CL : ℝ), 0 < CL ∧ ∀ {ε : ℝ}, 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → ∀ (i j : Fin 3), i ≠ j → r324CCLatticeThree ρ ε i j ≤ CL * |Real.log ε| ^ 2

The m = 3 entity table, in closed form. Uniformly in the bijection, the collapsed order-three entity is O(|log ε|²) — exactly L^{m-1} at m = 3. All six entities carry the same order, so no grading is available (or needed) at order three.

From the order-three collapse to the capped ledger at m = 3

def Anderson4D.R324CappedCrossCollapseThree (ρ : SmoothCutoff) (C : ℝ) : Prop

The order-three Parseval-collapse interface. It says that the physical entity integral is dominated by the collapsed zero-sum lattice sum of its own propagator pattern, with a pattern (i,j) = (σ⁻¹1, σ⁻¹3) of two distinct modes.

Equations

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

theorem Anderson4D.r324CappedCross_entityBoundAt_three_of_collapse {ρ : SmoothCutoff} {C : ℝ} (hC : 0 ≤ C) (h : R324CappedCrossCollapseThree ρ C) : ∃ (K : ℝ), 2 ≤ K ∧ R324CappedCrossEntityBoundAt ρ K 3

The collapse plus the proved calibration gives the ungraded per-entity bound at order three.

theorem Anderson4D.r324CappedCrossLedgerAt_three_of_collapse {ρ : SmoothCutoff} {C : ℝ} (hC : 0 ≤ C) (h : R324CappedCrossCollapseThree ρ C) : ∃ (K : ℝ), 0 ≤ K ∧ R324CappedCrossLedgerAt ρ K 3

The capped cross ledger at order three, conditional only on the order-three Parseval collapse: the six-entity count is geometric, so the proved uniform L² calibration closes the whole fibre.

Why the grading cannot be dropped beyond low orders

theorem Anderson4D.r324CappedCross_flatGrade_over_budget (C : ℝ) (N : ℕ) : ∃ (m : ℕ), N ≤ m ∧ C ^ m < ↑(r324LedgerThreePermEntities m).card

The flat grade is over budget at high capped orders. The entity count is exactly m!, so the flat grade m-1 — i.e. the ungraded per-entity ceiling, which is sharp at the identity entity — fails the graded-count clause ∑_e L^{grade e} ≤ C^m·L^{m-1} for every constant C at large m. Hence any proof of the capped cross ledger beyond the lowest orders must produce a genuinely non-constant grade.