Algebraic moment assembly from Proposition 3.6

This file isolates the exact algebraic content of paper (3.28) used in blueprint node P-mom. The antidiagonal is restricted to positive orders, odd total order vanishes, and even total order m contributes (λ / (√2 π))^(m - 2). Summing the even contributions is then an ordinary geometric series with ratio λ² / (2π²).

The coefficient table furnished by Prop36 may depend on the truncation B. This file deliberately makes no cross-truncation identification: that separate P-mom step requires uniqueness in (3.27) and positivity of the zero-mode four-point coefficient.

def Anderson4D.positiveAntidiagonalSum (𝔛 : ℕ → ℕ → ℝ) (m : ℕ) : ℝ

The positive-order antidiagonal sum occurring literally in (3.28).

Equations

• Anderson4D.positiveAntidiagonalSum 𝔛 m = ∑ p ∈ Finset.HasAntidiagonal.antidiagonal m with 1 ≤ p.1 ∧ 1 ≤ p.2, 𝔛 p.1 p.2

noncomputable def Anderson4D.prop36MomentBase (lam : ℝ) : ℝ

The one-step amplitude in (3.28).

Equations

• Anderson4D.prop36MomentBase lam = lam / (√2 * Real.pi)

noncomputable def Anderson4D.prop36EvenRatio (lam : ℝ) : ℝ

The ratio after restricting (3.28) to even total orders.

Equations

• Anderson4D.prop36EvenRatio lam = lam ^ 2 / (2 * Real.pi ^ 2)

noncomputable def Anderson4D.prop36EvenPartialSum (lam : ℝ) (N : ℕ) : ℝ

The first N even contributions, corresponding to total orders m = 2, 4, ..., 2N.

Equations

• Anderson4D.prop36EvenPartialSum lam N = ∑ n ∈ Finset.range N, Anderson4D.prop36MomentBase lam ^ (2 * n)

structure Anderson4D.Prop36AntidiagonalData (lam : ℝ) (B : ℕ) : Type

The part of the existential data in Prop36 needed for the algebraic assembly of (3.28). It retains the bound clause as well as the literal positive-antidiagonal identity, so downstream code does not need to destruct the much larger eventual moment-factorization clause.

• coeff : ℕ → ℕ → ℝ
• constant : ℝ
• constant_pos : 0 < self.constant
• coeff_bound (m₁ m₂ : ℕ) : 1 ≤ m₁ → 1 ≤ m₂ → |self.coeff m₁ m₂| ≤ self.constant * (self.constant * lam) ^ (m₁ + m₂ - 2)
• sum_identity (m : ℕ) : 2 ≤ m → positiveAntidiagonalSum self.coeff m = if Even m then prop36MomentBase lam ^ (m - 2) else 0

noncomputable def Anderson4D.Prop36.antidiagonalData {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} (hP36 : Prop36 M ρ lam) (B r : ℕ) : Prop36AntidiagonalData lam B

The canonical (3.28) data at truncation B and family size r. Its bound constant is definitionally independent of both parameters.

Equations

• hP36.antidiagonalData B r = { coeff := hP36.coefficientTable B r, constant := hP36.boundConstant, constant_pos := ⋯, coeff_bound := ⋯, sum_identity := ⋯ }

theorem Anderson4D.Prop36.nonempty_antidiagonalData {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} (hP36 : Prop36 M ρ lam) (B r : ℕ) : Nonempty (Prop36AntidiagonalData lam B)

Every chosen truncation and family size in Proposition 3.6 supplies the exact algebraic data of (3.28).

theorem Anderson4D.Prop36AntidiagonalData.odd_sum_eq_zero {lam : ℝ} {B : ℕ} (data : Prop36AntidiagonalData lam B) {m : ℕ} (_hmB : m ≤ B) (hm2 : 2 ≤ m) (hm : Odd m) : positiveAntidiagonalSum data.coeff m = 0

Literal odd-total-order consequence of (3.28).

theorem Anderson4D.Prop36AntidiagonalData.even_sum_eq_pow {lam : ℝ} {B : ℕ} (data : Prop36AntidiagonalData lam B) {m : ℕ} (_hmB : m ≤ B) (hm2 : 2 ≤ m) (hm : Even m) : positiveAntidiagonalSum data.coeff m = prop36MomentBase lam ^ (m - 2)

Literal even-total-order consequence of (3.28).

theorem Anderson4D.Prop36AntidiagonalData.sum_two_mul_add_two {lam : ℝ} {B : ℕ} (data : Prop36AntidiagonalData lam B) (n : ℕ) (hnB : 2 * n + 2 ≤ B) : positiveAntidiagonalSum data.coeff (2 * n + 2) = prop36MomentBase lam ^ (2 * n)

At total order 2n+2, the antidiagonal contribution has exponent exactly 2n.

theorem Anderson4D.Prop36AntidiagonalData.sum_even_antidiagonals_eq_partialSum {lam : ℝ} {B : ℕ} (data : Prop36AntidiagonalData lam B) (N : ℕ) (hNB : 2 * N ≤ B) : ∑ n ∈ Finset.range N, positiveAntidiagonalSum data.coeff (2 * n + 2) = prop36EvenPartialSum lam N

Summing the (3.28) identities at total orders 2, 4, ..., 2N gives the exact finite even partial sum.

Exact geometric-series evaluation

theorem Anderson4D.prop36MomentBase_sq (lam : ℝ) : prop36MomentBase lam ^ 2 = prop36EvenRatio lam

Squaring the amplitude in (3.28) gives the geometric ratio λ²/(2π²) with no hidden normalization factor.

theorem Anderson4D.prop36MomentBase_even_pow (lam : ℝ) (n : ℕ) : prop36MomentBase lam ^ (2 * n) = prop36EvenRatio lam ^ n

Every even contribution is the corresponding power of the one-variable geometric ratio.

theorem Anderson4D.prop36EvenPartialSum_eq_geometric (lam : ℝ) (N : ℕ) : prop36EvenPartialSum lam N = ∑ n ∈ Finset.range N, prop36EvenRatio lam ^ n

Exact conversion of the finite even contribution sum to a geometric partial sum.

theorem Anderson4D.prop36EvenPartialSum_eq_closed (lam : ℝ) (N : ℕ) (hr : prop36EvenRatio lam ≠ 1) : prop36EvenPartialSum lam N = (prop36EvenRatio lam ^ N - 1) / (prop36EvenRatio lam - 1)

Closed form for every finite even partial sum.

theorem Anderson4D.prop36EvenRatio_lt_one {lam : ℝ} (hlam : lam ^ 2 < 2 * Real.pi ^ 2) : prop36EvenRatio lam < 1

The subcritical hypothesis is exactly the statement that the even geometric ratio is strictly below one.

theorem Anderson4D.prop36EvenRatio_nonneg (lam : ℝ) : 0 ≤ prop36EvenRatio lam

theorem Anderson4D.one_sub_prop36EvenRatio_inv_eq_limitPrefactor {lam : ℝ} (hlam : lam ^ 2 < 2 * Real.pi ^ 2) : (1 - prop36EvenRatio lam)⁻¹ = limitPrefactor lam

Algebraic identification of the geometric-series value with the prefactor used by the limit Gaussian law.

theorem Anderson4D.hasSum_prop36EvenTerms {lam : ℝ} (hlam : lam ^ 2 < 2 * Real.pi ^ 2) : HasSum (fun (n : ℕ) => prop36MomentBase lam ^ (2 * n)) (limitPrefactor lam)

The even (3.28) contributions have sum exactly limitPrefactor λ in the subcritical regime.

theorem Anderson4D.tsum_prop36EvenTerms_eq_limitPrefactor {lam : ℝ} (hlam : lam ^ 2 < 2 * Real.pi ^ 2) : ∑' (n : ℕ), prop36MomentBase lam ^ (2 * n) = limitPrefactor lam

tsum form of the exact even contribution sum.

theorem Anderson4D.tendsto_prop36EvenPartialSum {lam : ℝ} (hlam : lam ^ 2 < 2 * Real.pi ^ 2) : Filter.Tendsto (prop36EvenPartialSum lam) Filter.atTop (nhds (limitPrefactor lam))

The finite even partial sums converge to the exact prefactor in the limit law.

theorem Anderson4D.Prop36.exists_evenAntidiagonalPartialSum {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} (hP36 : Prop36 M ρ lam) (N r : ℕ) : ∃ (data : Prop36AntidiagonalData lam (2 * N)), ∑ n ∈ Finset.range N, positiveAntidiagonalSum data.coeff (2 * n + 2) = prop36EvenPartialSum lam N

Direct API from Proposition 3.6: at every even truncation 2N, one may choose a single coefficient table whose summed positive antidiagonals through that truncation equal the geometric partial sum.