C_lock
plain-language theorem explainer
C_lock defines the locked ILG amplitude as the positive square root of phi cubed in the denominator. Analysts of SPARC rotation curves under phi-locked ILG would cite this constant when proving positivity and growth of the radial weight. The declaration is a direct abbreviation chosen to keep all downstream arguments free of Real.rpow.
Claim. The locked ILG amplitude is defined by $C = (1/phi^3)^{1/2}$, equivalently $phi^{-3/2}$.
background
The ILG radial weight is given by $w(R) = 1 + C (R/r_0)^alpha$ with dynamical exponent $alpha = 1 - 1/phi$ and amplitude $C = phi^{-3/2}$ obtained from three-channel factorization. This module proves the four structural facts (positivity, strict increase above one, monotonicity, and unbounded growth) that together imply the ILG-modified velocity squared exceeds the Newtonian baryonic term at every radius and diverges as radius tends to infinity. All proofs stay inside rational exponents to avoid the rpow surface while preserving the same qualitative envelope.
proof idea
Direct definition that sets C_lock to the square root of the reciprocal of phi to the third power.
why it matters
C_lock supplies the amplitude used by every enhancement theorem in the module (enhancement_pos, enhancement_above_one, enhancement_strict_mono, enhancement_unbounded) and by alphaLock_lt_one and J_bit in Constants. It realizes the three-channel factorization required for the structural prediction against Keplerian decay in Phase D9 of the RS_PhiLocked_SPARC_Prereg analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.