C_ilg_prefactor
This definition supplies the ILG kernel prefactor as phi raised to the power of negative three-halves. Researchers assembling the coercive projection energy functional or the modified Poisson equation in galactic-scale models cite this constant when replacing the earlier phi^{-5} scaling. The assignment is a direct extraction from the phi-ladder scaling in the upstream forcing chain.
claimThe ILG prefactor is given by $C = phi^{-3/2}$.
background
The module formalizes the Coercive Projection Law of Gravity, establishing a unique energy minimizer for the ILG functional together with pressure equivalence to standard Poisson. Core constants include the coercivity value 49/162 and the net factor K_net = (9/7)^2 that arises from eight-tick epsilon = 1/8. Phi is the self-similar fixed point forced in the T0-T8 chain.
proof idea
One-line definition that directly assigns the real value phi to the power of negative 3/2.
why it matters in Recognition Science
The constant enters the positivity theorem C_ilg_prefactor_pos and the CoerciveProjectionCert structure that bundles coercivity positivity, K_net > 1, operator positivity, and prefactor positivity. It implements the replacement of phi^{-5} by phi^{-3/2} in the galactic kernel, consistent with the eight-tick octave and D = 3 from the unified forcing chain.
scope and limits
- Does not prove positivity of the prefactor.
- Does not derive the exponent -3/2 from the Recognition Composition Law.
- Does not specify the full ILG energy functional.
- Does not connect the prefactor to specific observational galaxy data.
formal statement (Lean)
132noncomputable def C_ilg_prefactor : ℝ := phi ^ (-(3/2 : ℝ))
proof body
Definition body.
133