MainTheorem

Private Lemma 7.1a: ‖a + b‖² ≤ 2‖a‖² + 2‖b‖²

Private Lemma 7.1c: Final constant check

Helper lemmas

Auxiliary lemmas for polar decomposition

Parseval identity on circles

Polar decomposition of fockNormSq

Helper: polyEvalCircle = polyEval on the circle

Continuity and integrability helpers

Step 1: Circle-level pointwise bound

Annular decomposition infrastructure

Pre-absorption inequality

Proved via le_of_forall_pos_lt_add with a universal leakage coefficient (etaCoeff_5_universal), avoiding J-dependent leakage bounds.

theorem FockSPR.fock_space_coercivity {D : ℕ} (hD : 1 ≤ D) (a : Fin D → ℂ) : fockNormSq a ≤ 4600 ^ 2 * rhoFockNormSq a

theorem FockSPR.LocalFockSPR (p : Polynomial ℂ) (hp : Polynomial.eval 0 p = 0) : ∫ (z : ℂ), ‖Polynomial.eval z p‖ ^ 2 * Real.exp (-‖z‖ ^ 2) ≤ 4600 ^ 2 * ∫ (z : ℂ), |‖1 + Polynomial.eval z p‖ - 1| ^ 2 * Real.exp (-‖z‖ ^ 2)

Fock-space coercivity for complex polynomials with zero constant term.