C_ilg_prefactor_pos
plain-language theorem explainer
Positivity of the ILG kernel prefactor C = phi^{-3/2} is established. Researchers formalizing the coercive projection law of gravity cite this to guarantee the energy functional is bounded below and the kernel well-defined. The proof is a one-line wrapper that unfolds the definition and applies the standard lemma on positivity of real exponentiation for positive base.
Claim. The ILG kernel prefactor satisfies $0 < C$ where $C = phi^{-3/2}$ and $phi$ is the golden-ratio fixed point.
background
In the Coercive Projection module the ILG kernel prefactor is defined by $C_{ilg} = phi^{-3/2}$. This replaces the earlier galactic-scale constant $phi^{-5}$ and enters the energy functional whose unique minimizer is asserted by the coercive projection law. The module also records the net constant $K_{net} = (9/7)^2$ arising from the eight-tick octave and the pressure equivalence $p = w rho_b$ between the ILG modified Poisson equation and the standard form.
proof idea
The proof is a one-line wrapper. It unfolds the definition of C_ilg_prefactor to the power expression $phi^{-3/2}$ and applies Real.rpow_pos_of_pos using the upstream positivity hypothesis phi_pos.
why it matters
The result supplies the prefactor_positive field inside the certificate theorem coercive_projection_cert. That certificate assembles the coercivity, net-constant, operator-positivity and prefactor-positivity facts needed to certify the unique energy minimizer of the ILG functional. Within the Recognition framework the positivity aligns with the forcing chain step T6 (phi as self-similar fixed point) and ensures the kernel remains positive for the projection law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.