Showcase

This file packages the local Fock-space argument in a paper-friendly form.

The key reduction is the centered decomposition

p = (p - C (p.eval 0)) + C (p.eval 0),

which kills the constant term and lets the core theorem LocalFockSPR_of_small_norm apply to the centered polynomial. The phase-aligned conclusion is then obtained by the wrapper in LocalHelpers.lean.

noncomputable def FockSPR.centeredPolynomial (p : Polynomial ℂ) : Polynomial ℂ

The centered polynomial obtained by removing the constant term.

Equations

• FockSPR.centeredPolynomial p = p - Polynomial.C (Polynomial.eval 0 p)

theorem FockSPR.centeredPolynomial_eval_zero (p : Polynomial ℂ) : Polynomial.eval 0 (centeredPolynomial p) = 0

The centered polynomial has zero constant term.

theorem FockSPR.orthogonalReduction (p : Polynomial ℂ) : p = centeredPolynomial p + Polynomial.C (Polynomial.eval 0 p)

The paper-friendly orthogonal reduction step: split off the constant term.

theorem FockSPR.orthogonalReduction_core (p : Polynomial ℂ) (hp_real : (Polynomial.eval 0 p).im = 0) (hsmall : 1 / Real.pi * ∫ (z : ℂ), ‖Polynomial.eval z p‖ ^ 2 * Real.exp (-‖z‖ ^ 2) ≤ (1 / 4601) ^ 2) : ∫ (z : ℂ), ‖Polynomial.eval z p‖ ^ 2 * Real.exp (-‖z‖ ^ 2) ≤ 23003 ^ 2 * ∫ (z : ℂ), |‖1 + Polynomial.eval z p‖ - 1| ^ 2 * Real.exp (-‖z‖ ^ 2)

The centered core estimate, stated as a reusable theorem for the paper.

theorem FockSPR.orthogonalReduction_exists_phase (p : Polynomial ℂ) (hsmall : 1 / Real.pi * ∫ (z : ℂ), ‖Polynomial.eval z p‖ ^ 2 * Real.exp (-‖z‖ ^ 2) ≤ (1 / 4601) ^ 2) : ∃ (w : ℂ), ‖w‖ = 1 ∧ ∫ (z : ℂ), ‖w * (1 + Polynomial.eval z p) - 1‖ ^ 2 * Real.exp (-‖z‖ ^ 2) ≤ 23003 ^ 2 * ∫ (z : ℂ), |‖1 + Polynomial.eval z p‖ - 1| ^ 2 * Real.exp (-‖z‖ ^ 2)

The phase-aligned version used in the final statement.