The general-order entity lattice pattern and its AM–GM grade

R324CollapsePi collapses one half chain at every order. A pure-cross entity has two half chains sharing the same m cross momenta: the left chain reads them in identity order, the right chain in the order of the bijection. So the collapsed entity of the bijection σ is the zero-sum lattice sum whose summand is

W_τ(q) = ∏ᵢ ‖ρ̂(εqᵢ)‖² · P(q) · P(q∘τ), τ = σ⁻¹,

where P(q) = ∏ⱼ ⟨qⱼ+…+q_{m-1}⟩⁻² is exactly the propagator product harvested by r324Col_piChain_integral (suffix sums; on the zero-sum sector these are the paper's prefix sums up to sign). This file defines that pattern for arbitrary m and arbitrary σ, and proves what the arithmetic-geometric argument gives.

The grade the AM–GM argument gives is flat

ab ≤ (a²+b²)/2 applied to a = P(q), b = P(q∘τ) splits every entity into two doubled patterns (r324ColLatWeight_le_doubled_avg), and the relabelling q ↦ q∘τ is a measure-preserving bijection of the lattice configuration space under which the symbol weight is invariant (r324Col_tsum_doubled_perm). Hence at every order and for every bijection the AM–GM bound is the identity entity's own bound (r324Col_tsum_latWeight_le): the argument is uniform in σ and therefore produces exactly the flat grade m-1.

That is sharp for the identity entity, and by r324CappedCross_flatGrade_over_budget it is over budget for large m. So this file also delimits precisely what is missing for the graded clause: a mechanism that is not invariant under relabelling the cross momenta, i.e. one that sees the interaction between the two suffix-sum families rather than each separately. At m = 3 the flat grade is enough (3! ≤ 2³), which is why order three closes on the calibration alone.

The lattice configuration of an entity

def Anderson4D.r324ColExtend {m : ℕ} (q : Fin m → Z4) : ℕ → Z4

Extend a finite momentum assignment to the sequence consumed by the chain collapse.

Equations

• Anderson4D.r324ColExtend q j = if h : j < m then q ⟨j, h⟩ else 0

noncomputable def Anderson4D.r324ColLatSym (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (q : Fin m → Z4) : ℝ

The symbol weight ∏ᵢ ‖ρ̂(εqᵢ)‖² of the m cross legs.

Equations

• Anderson4D.r324ColLatSym ρ ε q = ∏ i : Fin m, ‖ρ.symbol ε (q i)‖ ^ 2

noncomputable def Anderson4D.r324ColLatProp {m : ℕ} (q : Fin m → Z4) : ℝ

The propagator product of one half chain, read in the order q: the suffix-sum brackets delivered by r324Col_piChain_integral.

Equations

• Anderson4D.r324ColLatProp q = Anderson4D.r324ColPiProp m (Anderson4D.r324ColExtend q)

noncomputable def Anderson4D.r324ColLatWeight (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (τ : Equiv.Perm (Fin m)) (q : Fin m → Z4) : ℝ

The lattice summand of the pure-cross entity σ at order m: symbol weights times the two half-chain propagator products, the left one in identity order and the right one in the order τ = σ⁻¹.

Equations

• Anderson4D.r324ColLatWeight ρ ε τ q = Anderson4D.r324ColLatSym ρ ε q * (Anderson4D.r324ColLatProp q * Anderson4D.r324ColLatProp (q ∘ ⇑τ))

noncomputable def Anderson4D.r324ColLatDoubled (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (q : Fin m → Z4) : ℝ

The doubled pattern: the same symbol weight against a squared propagator product. This is the resonant shape the arithmetic-geometric split produces.

Equations

• Anderson4D.r324ColLatDoubled ρ ε q = Anderson4D.r324ColLatSym ρ ε q * Anderson4D.r324ColLatProp q ^ 2

theorem Anderson4D.r324ColLatSym_nonneg (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (q : Fin m → Z4) : 0 ≤ r324ColLatSym ρ ε q

theorem Anderson4D.r324ColPiProp_nonneg (n : ℕ) (q : ℕ → Z4) : 0 ≤ r324ColPiProp n q

theorem Anderson4D.r324ColLatProp_nonneg {m : ℕ} (q : Fin m → Z4) : 0 ≤ r324ColLatProp q

theorem Anderson4D.r324ColLatWeight_nonneg (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (τ : Equiv.Perm (Fin m)) (q : Fin m → Z4) : 0 ≤ r324ColLatWeight ρ ε τ q

theorem Anderson4D.r324ColLatDoubled_nonneg (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (q : Fin m → Z4) : 0 ≤ r324ColLatDoubled ρ ε q

The arithmetic-geometric split, uniformly in the order

theorem Anderson4D.r324ColLatWeight_le_doubled_avg (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (τ : Equiv.Perm (Fin m)) (q : Fin m → Z4) : r324ColLatWeight ρ ε τ q ≤ (r324ColLatDoubled ρ ε q + r324ColLatSym ρ ε q * r324ColLatProp (q ∘ ⇑τ) ^ 2) / 2

The AM–GM split at every order and every bijection. The mixed propagator pattern of σ is dominated by the average of the two doubled patterns: the identity one and the σ-relabelled one.

Relabelling invariance

def Anderson4D.R324ColZeroSum (m : ℕ) : Type

The zero-sum sector. The two external Green legs of each half chain integrate to unit mass and turn the last surviving character into the Kronecker delta q₀+…+q_{m-1} = 0 (r324Col_piChain_closed), so the collapsed entity is a sum over this sector only. It carries m-1 free momenta, which is why the flat grade is m-1 and not m.

Equations

• Anderson4D.R324ColZeroSum m = { q : Fin m → Anderson4D.Z4 // ∑ i : Fin m, q i = 0 }

@[implicit_reducible]

instance Anderson4D.instCoeFunR324ColZeroSumForallFinZ4 (m : ℕ) : CoeFun (R324ColZeroSum m) fun (x : R324ColZeroSum m) => Fin m → Z4

Equations

• Anderson4D.instCoeFunR324ColZeroSumForallFinZ4 m = { coe := Subtype.val }

def Anderson4D.r324ColReindex {m : ℕ} (τ : Equiv.Perm (Fin m)) : (Fin m → Z4) ≃ (Fin m → Z4)

Reordering the cross momenta is a bijection of the lattice configuration space.

Equations

• Anderson4D.r324ColReindex τ = (Equiv.symm τ).arrowCongr (Equiv.refl Anderson4D.Z4)

@[simp]

theorem Anderson4D.r324ColReindex_apply {m : ℕ} (τ : Equiv.Perm (Fin m)) (q : Fin m → Z4) : (r324ColReindex τ) q = q ∘ ⇑τ

def Anderson4D.r324ColReindexZero {m : ℕ} (τ : Equiv.Perm (Fin m)) : R324ColZeroSum m ≃ R324ColZeroSum m

Reordering preserves momentum conservation, so it restricts to the zero-sum sector.

Equations

• Anderson4D.r324ColReindexZero τ = (Anderson4D.r324ColReindex τ).subtypeEquiv ⋯

@[simp]

theorem Anderson4D.r324ColReindexZero_val {m : ℕ} (τ : Equiv.Perm (Fin m)) (q : R324ColZeroSum m) : ↑((r324ColReindexZero τ) q) = ↑q ∘ ⇑τ

theorem Anderson4D.r324ColLatSym_comp (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (τ : Equiv.Perm (Fin m)) (q : Fin m → Z4) : r324ColLatSym ρ ε (q ∘ ⇑τ) = r324ColLatSym ρ ε q

The symbol weight is symmetric in the cross momenta.

theorem Anderson4D.r324Col_tsum_doubled_perm (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (τ : Equiv.Perm (Fin m)) : ∑' (q : R324ColZeroSum m), r324ColLatSym ρ ε ↑q * r324ColLatProp (↑q ∘ ⇑τ) ^ 2 = ∑' (q : R324ColZeroSum m), r324ColLatDoubled ρ ε ↑q

The relabelled doubled sum is the identity doubled sum. This is the exact reason the arithmetic-geometric argument cannot see the grading: it is invariant under permuting the cross momenta.

theorem Anderson4D.r324Col_summable_doubled_perm (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (τ : Equiv.Perm (Fin m)) (h : Summable fun (q : R324ColZeroSum m) => r324ColLatDoubled ρ ε ↑q) : Summable fun (q : R324ColZeroSum m) => r324ColLatSym ρ ε ↑q * r324ColLatProp (↑q ∘ ⇑τ) ^ 2

The grade the argument delivers

theorem Anderson4D.r324Col_tsum_latWeight_le (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (τ : Equiv.Perm (Fin m)) (h : Summable fun (q : R324ColZeroSum m) => r324ColLatDoubled ρ ε ↑q) : (Summable fun (q : R324ColZeroSum m) => r324ColLatWeight ρ ε τ ↑q) ∧ ∑' (q : R324ColZeroSum m), r324ColLatWeight ρ ε τ ↑q ≤ ∑' (q : R324ColZeroSum m), r324ColLatDoubled ρ ε ↑q

Every entity is bounded by the identity entity's doubled sum, at every order. This is the exact output of the arithmetic-geometric argument at general m and general σ: the flat grade. It is sharp for σ = id and, by r324CappedCross_flatGrade_over_budget, cannot by itself fund the graded-count clause at large m.

General-order analytic inputs

def Anderson4D.R324ColPhysicalCollapseAt (ρ : SmoothCutoff) (C : ℝ) (m : ℕ) : Prop

The general-order physical→lattice collapse, as a named Prop: the physical entity integral is dominated by the zero-sum lattice sum of its own suffix-bracket pattern. This is what r324Col_piChain_integral and r324Col_piChain_closed evaluate half by half; assembling the two halves needs the covariance Fourier expansion and one Tonelli interchange between the mode sum and the 2m+4 physical integrations.

Equations

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

def Anderson4D.R324ColDoubledBudgetAt (ρ : SmoothCutoff) (D : ℝ) (m : ℕ) : Prop

The doubled window budget: the identity-pattern lattice sum, m-1 free momenta each covered by one critical quartic window, is D^m·L^{m-1}. This is the general-order form of the proved translated-window iteration r324SW_translated_window_le_log.

Equations

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

theorem Anderson4D.r324Col_entityBoundAt_of_collapse {ρ : SmoothCutoff} {C D : ℝ} {m : ℕ} (hC : 0 ≤ C) (hcol : R324ColPhysicalCollapseAt ρ C m) (hbud : R324ColDoubledBudgetAt ρ D m) : R324CappedCrossEntityBoundAt ρ (C * D) m

The general-order per-entity ledger. The collapse plus the doubled window budget give the ungraded per-entity bound at every order, with the flat grade m-1 that the arithmetic-geometric argument delivers uniformly in the bijection.

theorem Anderson4D.r324Col_cappedCrossLedgerAt_three {ρ : SmoothCutoff} {C D : ℝ} (hC : 0 ≤ C) (hD : 0 ≤ D) (hcol : R324ColPhysicalCollapseAt ρ C 3) (hbud : R324ColDoubledBudgetAt ρ D 3) : ∃ (K : ℝ), 0 ≤ K ∧ R324CappedCrossLedgerAt ρ K 3

Order three closes on the general machine. At m = 3 the entity count 3! = 6 is itself geometric, so the flat grade suffices and the capped cross ledger at order three follows from the two general-order inputs alone.