CoerciveProjectionCert
plain-language theorem explainer
CoerciveProjectionCert packages four positivity conditions that certify the ILG energy functional possesses a unique minimizer under the coercive projection law. Researchers modeling gravity through information-limited dynamics cite this structure when confirming coercivity exceeds zero, the net factor exceeds one, the weight operator stays nonnegative, and the prefactor is positive. The declaration is a direct record structure with no computation or reduction steps.
Claim. A certificate for the coercive projection law consists of four conditions: the coercivity constant satisfies $0 < c$ where $c = 49/162$, the net constant satisfies $1 < K$ where $K = (9/7)^2$, the weight operator satisfies $w f^2 ≥ 0$ for all real $w,f$ with $w ≥ 1$, and the prefactor satisfies $0 < C$ where $C = ϕ^{-3/2}$.
background
The module formalizes the Coercive Projection Law of Gravity from the CPM and pressure-gravity papers. It treats the ILG energy functional as having a unique minimizer once coercivity, net factor, operator positivity, and prefactor positivity hold. The coercivity constant $c = 49/162$ is taken from the eight-tick projection bound; the net constant $K_{net} = (9/7)^2$ arises from $ε = 1/8$ with the return tick supplying the extra factor of 9/7. The prefactor $C = ϕ^{-3/2}$ replaces the earlier galactic kernel scale. The operator condition states that weights $w ≥ 1$ keep the quadratic form nonnegative, ensuring the energy is bounded below.
proof idea
The declaration is a structure definition that directly records the four field assertions. It packages the inequality $0 < c_{coercive}$, the inequality $1 < K_{net}$, the universal quantification $∀ w f, 1 ≤ w → 0 ≤ w f^2$, and the inequality $0 < C_{ilg_prefactor}$. No tactics, reductions, or lemmas are applied; the structure simply serves as a typed container for these four facts.
why it matters
The structure supplies the certificate type instantiated by the downstream theorem coercive_projection_cert, which populates the fields with explicit positivity lemmas. It closes the verification that the ILG energy functional has a unique minimizer, tying the eight-tick octave (T7) and the phi-based prefactor directly to the energy-minimization principle. The certificate supports the claimed equivalence between the ILG modified Poisson equation and standard Poisson with effective pressure source $p = w ρ_b$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.