The external input: Proposition 3.6 (blueprint node P-3.6)

Paper: P-mom — the external input Prop 3.6 (Gabriel–Rosati)

The frozen statement of Deng–Shen's Proposition 3.6 in coefficient form (PAPER_MAP remark 6): existence of the moment-asymptotics data 𝔛 m₁ m₂ and constants under which the joint moments of the parametrix mode coefficients pmCoeff Wick-factorize ((3.26)) and the pair covariances converge to multiples of the four-point kernel coefficients ((3.27)–(3.28)). The main theorem (Anderson4D.Main.Theorem) is frozen conditionally on this proposition, quantified over all couplings.

def Anderson4D.Prop36WithConstant (M : NoiseModel) (ρ : SmoothCutoff) (lam C : ℝ) : Prop

Proposition 3.6 with one named geometric constant. The paper's generic constant C in the global coefficient bound is uniform in the fixed truncation parameters B and r. Keeping it as an explicit parameter is essential for the corner-tail estimate in Step 3.

Equations

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

structure Anderson4D.Prop36 (M : NoiseModel) (ρ : SmoothCutoff) (lam : ℝ) : Type

Proposition 3.6 of the paper (node P-3.6), coefficient form. There is one positive coefficient-bound constant, uniform over the fixed moment bound B and family size r; after fixing B,r, the coefficient table may still be chosen existentially. The clauses are:

• bound clause (part of (3.27)): |𝔛 m₁ m₂| ≤ C (Cλ)^{m₁+m₂-2};
• sum clause ((3.28)): the sum is over positive orders m₁,m₂ ≥ 1; it equals (λ/(√2·π))^{m-2} for even m and zero for odd m;
• Wick factorization ((3.26)): for every family of r mode/order triples, eventually as ε ↓ 0 the joint moment of the pmCoeffs differs from its full-pairing (Wick) factorization by O(λ_ε^r/|log ε|); the paper's family (m_j, α_j, β_j) is packaged as modes : Fin r → (Z4 × Z4) × ℕ — component .1 the mode pair (α_j, β_j), component .2 the order m_j — so a single quantifier covers it. The same clause records the implicit regularity used when the paper calls these quantities moments: the coefficients are measurable and every displayed finite product is integrable;
• covariance asymptotics ((3.27)): each pair moment is λ_ε² 𝔛 m₁ m₂ · fourPointHCoeff + O(λ_ε²/|log ε|).

Norms ‖·‖ are the complex modulus. The eventuality filter is ε ↓ 0 within (0, ∞).

• boundConstant : ℝ

  The paper's uniform geometric coefficient-bound constant.

• boundConstant_pos : 0 < self.boundConstant
• withBoundConstant : Prop36WithConstant M ρ lam self.boundConstant

noncomputable def Anderson4D.Prop36.coefficientTable {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} (h : Prop36 M ρ lam) (B r : ℕ) : ℕ → ℕ → ℝ

Canonical coefficient table selected after fixing the paper's finite order and family parameters.

Equations

• h.coefficientTable B r = Classical.choose ⋯

theorem Anderson4D.Prop36.coefficientTable_spec {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} (h : Prop36 M ρ lam) (B r : ℕ) : (∀ (m₁ m₂ : ℕ), 1 ≤ m₁ → 1 ≤ m₂ → |h.coefficientTable B r m₁ m₂| ≤ h.boundConstant * (h.boundConstant * lam) ^ (m₁ + m₂ - 2)) ∧ (∀ (m : ℕ), 2 ≤ m → ∑ p ∈ Finset.HasAntidiagonal.antidiagonal m with 1 ≤ p.1 ∧ 1 ≤ p.2, h.coefficientTable B r p.1 p.2 = if Even m then (lam / (√2 * Real.pi)) ^ (m - 2) else 0) ∧ ∀ (modes : Fin r → (Z4 × Z4) × ℕ), (∀ (j : Fin r), 1 ≤ (modes j).2 ∧ (modes j).2 ≤ B) → (∀ (ε : ℝ) (j : Fin r), Measurable (pmCoeff M ρ lam ε (modes j).2 (modes j).1.1 (modes j).1.2)) ∧ (∀ (ε : ℝ), MeasureTheory.Integrable (fun (ω : M.Ω) => ∏ j : Fin r, pmCoeff M ρ lam ε (modes j).2 (modes j).1.1 (modes j).1.2 ω) MeasureTheory.volume) ∧ ∃ (C' : ℝ), 0 < C' ∧ ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ‖(∫ (ω : M.Ω), ∏ j : Fin r, pmCoeff M ρ lam ε (modes j).2 (modes j).1.1 (modes j).1.2 ω) - ∑ κ : PartialPairing (Fin r) with κ.IsFull, ∏ i ∈ κ.pairSupport with i < κ i, ∫ (ω : M.Ω), pmCoeff M ρ lam ε (modes i).2 (modes i).1.1 (modes i).1.2 ω * pmCoeff M ρ lam ε (modes (κ i)).2 (modes (κ i)).1.1 (modes (κ i)).1.2 ω‖ ≤ C' * lamEps lam ε ^ r / |Real.log ε| ∧ ∀ (m₁ m₂ : ℕ), 1 ≤ m₁ → m₁ ≤ B → 1 ≤ m₂ → m₂ ≤ B → ∀ (α₁ β₁ α₂ β₂ : Z4), ‖(∫ (ω : M.Ω), pmCoeff M ρ lam ε m₁ α₁ β₁ ω * pmCoeff M ρ lam ε m₂ α₂ β₂ ω) - (lamEps lam ε ^ 2 * h.coefficientTable B r m₁ m₂) • fourPointHCoeff α₁ β₁ α₂ β₂‖ ≤ C' * lamEps lam ε ^ 2 / |Real.log ε|

def Anderson4D.Prop36Family (M : NoiseModel) (ρ : SmoothCutoff) : Prop

Uniform-in-coupling form of the external input. This is the precise hypothesis needed by the conditional main theorem to choose a single small-coupling threshold before lam is quantified.

Equations

• Anderson4D.Prop36Family M ρ = ∃ (C : ℝ), 0 < C ∧ ∀ (lam : ℝ), 0 < lam → Anderson4D.Prop36WithConstant M ρ lam C

noncomputable def Anderson4D.Prop36Family.boundConstant {M : NoiseModel} {ρ : SmoothCutoff} (h : Prop36Family M ρ) : ℝ

The single coefficient-bound constant selected once for the whole positive-coupling family.

Equations

• h.boundConstant = Classical.choose h

theorem Anderson4D.Prop36Family.boundConstant_pos {M : NoiseModel} {ρ : SmoothCutoff} (h : Prop36Family M ρ) : 0 < h.boundConstant

theorem Anderson4D.Prop36Family.withBoundConstant {M : NoiseModel} {ρ : SmoothCutoff} (h : Prop36Family M ρ) (lam : ℝ) : 0 < lam → Prop36WithConstant M ρ lam h.boundConstant

noncomputable def Anderson4D.Prop36Family.prop36 {M : NoiseModel} {ρ : SmoothCutoff} (h : Prop36Family M ρ) {lam : ℝ} (hlam : 0 < lam) : Prop36 M ρ lam

A uniform family specializes to Proposition 3.6 data at every positive coupling, retaining the family's single selected constant.

Equations

• h.prop36 hlam = { boundConstant := h.boundConstant, boundConstant_pos := ⋯, withBoundConstant := ⋯ }

@[simp]

theorem Anderson4D.Prop36Family.prop36_boundConstant {M : NoiseModel} {ρ : SmoothCutoff} (h : Prop36Family M ρ) {lam : ℝ} (hlam : 0 < lam) : (h.prop36 hlam).boundConstant = h.boundConstant

noncomputable def Anderson4D.Prop36Family.couplingThreshold {M : NoiseModel} {ρ : SmoothCutoff} (h : Prop36Family M ρ) : ℝ

A concrete positive coupling threshold depending only on the one family-wide coefficient constant. The extra cutoff at one also gives the paper's subcritical inequality λ² < 2π².

Equations

• h.couplingThreshold = min (1 / (2 * h.boundConstant)) 1

theorem Anderson4D.Prop36Family.couplingThreshold_pos {M : NoiseModel} {ρ : SmoothCutoff} (h : Prop36Family M ρ) : 0 < h.couplingThreshold

theorem Anderson4D.Prop36Family.boundConstant_mul_lt_one {M : NoiseModel} {ρ : SmoothCutoff} (h : Prop36Family M ρ) {lam : ℝ} (hlam : lam ∈ Set.Ioo 0 h.couplingThreshold) : h.boundConstant * lam < 1

Every coupling below the family threshold has geometric ratio strictly smaller than one.

theorem Anderson4D.Prop36Family.sq_lt_two_mul_pi_sq {M : NoiseModel} {ρ : SmoothCutoff} (h : Prop36Family M ρ) {lam : ℝ} (hlam : lam ∈ Set.Ioo 0 h.couplingThreshold) : lam ^ 2 < 2 * Real.pi ^ 2

The same concrete threshold lies safely inside the paper's subcritical range.

noncomputable def Anderson4D.Prop36Family.couplingThresholdWith {M : NoiseModel} {ρ : SmoothCutoff} (h : Prop36Family M ρ) (powerConstant : ℝ) : ℝ

Refine the external Proposition 3.6 threshold by a second positive geometric constant. The latter is the constant produced internally by the deterministic second-moment estimate, so both geometric series can be controlled by one coupling range.

Equations

• h.couplingThresholdWith powerConstant = min h.couplingThreshold (1 / (2 * powerConstant))

theorem Anderson4D.Prop36Family.couplingThresholdWith_pos {M : NoiseModel} {ρ : SmoothCutoff} (h : Prop36Family M ρ) {powerConstant : ℝ} (hpower : 0 < powerConstant) : 0 < h.couplingThresholdWith powerConstant

theorem Anderson4D.Prop36Family.mem_couplingThreshold_of_mem_couplingThresholdWith {M : NoiseModel} {ρ : SmoothCutoff} (h : Prop36Family M ρ) {powerConstant lam : ℝ} (hlam : lam ∈ Set.Ioo 0 (h.couplingThresholdWith powerConstant)) : lam ∈ Set.Ioo 0 h.couplingThreshold

The refined range remains inside the range selected from the external coefficient table.

theorem Anderson4D.Prop36Family.powerConstant_mul_lt_one {M : NoiseModel} {ρ : SmoothCutoff} (h : Prop36Family M ρ) {powerConstant lam : ℝ} (hpower : 0 < powerConstant) (hlam : lam ∈ Set.Ioo 0 (h.couplingThresholdWith powerConstant)) : powerConstant * lam < 1

The internally produced geometric ratio is strictly less than one throughout the refined coupling range.