C_ilg_prefactor_pos
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the exponent -3/2 from the recognition composition law.
- Does not supply a numerical evaluation of the prefactor.
- Does not address stability under small perturbations of phi.
- Does not extend the claim to bases that are not strictly positive.
formal statement (Lean)
134theorem C_ilg_prefactor_pos : 0 < C_ilg_prefactor := by
proof body
Term-mode proof.
135 unfold C_ilg_prefactor
136 exact Real.rpow_pos_of_pos phi_pos _
137
138/-- The ILG alpha exponent: alpha = (1 - 1/phi) / 2 = alphaLock. -/