Proposition 4.1

Paper: P-4.1 — Prop 4.1 — the primitive pairing estimate, proved

This file combines the exact first-order computation with the endpoint-preserving R-51 argument at orders n ≥ 2, and packages the result in the frozen Proposition41 specification.

Monotonicity in the named majorant constant

theorem Anderson4D.primitiveKernelMajorant_mono_constant {C₁ C₂ lam ε supportConstant : ℝ} {n : ℕ} {z : T4} (hC₁ : 0 ≤ C₁) (hC : C₁ ≤ C₂) (hlam : 0 ≤ lam) : primitiveKernelMajorant C₁ lam ε supportConstant n z ≤ primitiveKernelMajorant C₂ lam ε supportConstant n z

theorem Anderson4D.primitiveInsertedMajorant_mono_constant {C₁ C₂ lam ε supportConstant : ℝ} {n : ℕ} {z : T4} (hC₁ : 0 ≤ C₁) (hC : C₁ ≤ C₂) (hlam : 0 ≤ lam) : primitiveInsertedMajorant C₁ lam ε supportConstant n z ≤ primitiveInsertedMajorant C₂ lam ε supportConstant n z

theorem Anderson4D.PrimitiveKernelBounds.mono_constant (ρ : SmoothCutoff) {lam ε : ℝ} {n : ℕ} (hn : 1 ≤ n) {G : Fin (2 * n - 1) → T4 → ℝ} {supportConstant C₁ C₂ : ℝ} (hC₁ : 0 ≤ C₁) (hC : C₁ ≤ C₂) (hlam : 0 ≤ lam) (hbound : PrimitiveKernelBounds ρ lam ε n hn G supportConstant C₁) : PrimitiveKernelBounds ρ lam ε n hn G supportConstant C₂

Final assembly

theorem Anderson4D.proposition41_order_one (ρ : SmoothCutoff) : ∃ (supportConstant : ℝ) (C : ℝ), 0 < supportConstant ∧ 0 < C ∧ ∀ (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ), Prop41BoundPredicate ρ lam ε n hn G 1 supportConstant C

Proposition 4.1 with its order constant exposed as exactly 1.

The generic Proposition41 specification existentially hides that constant, which is appropriate for the standalone paper statement but insufficient when connecting it to the concrete truncation A = ⌊|log ε|⌋. This strengthened public form records the compatibility needed by the R-322/R-324 reductions.

theorem Anderson4D.proposition41_at_truncation (ρ : SmoothCutoff) : ∃ (supportConstant : ℝ) (C : ℝ), 0 < supportConstant ∧ 0 < C ∧ ∀ (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ), 0 < lam → 0 < ε → ε ≤ 1 → n ≤ truncOrder ε → IsAdmissiblePrimitiveInput n G → MemEClassT4 (primitiveKernelDiff ρ lam ε n hn G) ∧ MemEClassT4 (primitiveKernelInsertedDiff ρ lam ε n hn G) ∧ PrimitiveKernelBounds ρ lam ε n hn G supportConstant C

Proposition 4.1 specialized to every order used by the concrete renormalized parametrix.

This theorem is the direct paper-facing bridge: its order hypothesis is literally n ≤ truncOrder ε, with no hidden comparison constant left for a downstream reduction to recover.

theorem Anderson4D.proposition41 (ρ : SmoothCutoff) : Proposition41 ρ

Proposition 4.1. Primitive pairing kernels belong to the hyperoctahedrally invariant class 𝓔 and obey (4.3)--(4.4), uniformly over the perturbative order range.