From kernel comparison to Fourier-coefficient agreement

The bounded-operator parametrix uses the graded word expansion, while the probabilistic moment estimate uses the paper's partial-pairing expansion. This file records the exact downstream bridge: almost-everywhere equality of their kernels implies equality of every paper Fourier coefficient.

theorem Anderson4D.PartialPairing.parametrixGradedCoefficientAgreement_of_ae_kernel_eq (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) (ω : M.Ω) (hkernel : ∀ n ≤ A, ∀ᵐ (x : T4) (y : T4) ∂paperMeasure, parametrixP M ρ lam ε n x y ω = gradedParametrix M ρ lam ε n x y ω) : ParametrixGradedCoefficientAgreement M ρ lam ε A ω

Almost-everywhere equality of the pairing and graded kernels through a finite order gives the coefficient agreement consumed by the physical operator bridge.

theorem Anderson4D.PartialPairing.parametrixGradedCoefficientAgreement_of_integrability (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) (ω : M.Ω) (hint : ParametrixIdentityIntegrability M ρ lam ε ω) : ParametrixGradedCoefficientAgreement M ρ lam ε A ω

The existing pointwise Proposition 3.4 ledger therefore implies the integrated coefficient agreement. The endpoint diagonal is discarded using its zero paper-Haar measure.