One genuine integrated primitive-block collapse for R-324

This file specializes the abstract one-block engine to the actual primitive pairing sum supplied by Proposition 4.1. The constants are chosen uniformly before the scale, coupling, order, input family, and outer kernel.

theorem Anderson4D.exists_r324OnePrimitiveCollapse_le_at_truncation (ρ : SmoothCutoff) : ∃ (supportConstant : ℝ) (primitiveConstant : ℝ) (collapseConstant : ℝ), 0 < supportConstant ∧ 0 < primitiveConstant ∧ 0 < collapseConstant ∧ ∀ (lam ε A : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (Gp : T4 → ℝ) (x : T4), 0 < lam → 0 ≤ A → 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → n ≤ truncOrder ε → x ≠ 0 → (∀ (j : Fin (2 * n - 1)), Measurable (G j)) → IsAdmissiblePrimitiveInput n G → (∀ (z : T4), z ≠ 0 → |Gp z| ≤ A * invSqKer z) → MeasureTheory.Integrable (r322CollapseIntegrand Gp (primitiveKernelDiff ρ lam ε n hn G) greenFn x) (paperMeasure.prod paperMeasure) → |r322Collapse Gp (primitiveKernelDiff ρ lam ε n hn G) greenFn x| ≤ A * (primitiveConstant * lam) ^ (2 * n) * collapseConstant * invSqKer x

One concrete primitive block can be removed with the paper's exact perturbative order. Both the E-class fact and the pointwise majorant for the genuine primitive sum are supplied by the proved Proposition 4.1.

theorem Anderson4D.exists_normalized_r324OnePrimitiveCollapse_admissible_at_truncation (ρ : SmoothCutoff) : ∃ (supportConstant : ℝ) (primitiveConstant : ℝ) (collapseConstant : ℝ), 0 < supportConstant ∧ 0 < primitiveConstant ∧ 0 < collapseConstant ∧ ∀ (lam ε A : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (Gp : T4 → ℝ), 0 < lam → 0 < A → 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → n ≤ truncOrder ε → (∀ (j : Fin (2 * n - 1)), Measurable (G j)) → IsAdmissiblePrimitiveInput n G → MemEClassT4 Gp → (∀ (z : T4), z ≠ 0 → |Gp z| ≤ A * invSqKer z) → (∀ (x : T4), MeasureTheory.Integrable (r322CollapseIntegrand Gp (primitiveKernelDiff ρ lam ε n hn G) greenFn x) (paperMeasure.prod paperMeasure)) → ∀ (laterOrder : ℕ), IsAdmissiblePrimitiveInput laterOrder fun (x : Fin (2 * laterOrder - 1)) => normalizedOffDiagonalRepresentative (A * (primitiveConstant * lam) ^ (2 * n) * collapseConstant) (r322Collapse Gp (primitiveKernelDiff ρ lam ε n hn G) greenFn)

After one genuine primitive collapse, division by its proved scale and the harmless diagonal adjustment produce an admissible input family for every later primitive order. This is the concrete induction step used in the successive block collapse.