enhancement_real_above_one
plain-language theorem explainer
The radial enhancement w_real(R, r0, α) = 1 + C_lock ⋅ (R/r0)^α exceeds 1 for every positive R and r0, with no restriction on the real exponent α. Gravity and ILG modelers cite the result to guarantee a strictly positive correction in the real-exponent extension. The proof is a short term-mode chain: positivity of C_lock, positivity of the ratio R/r0, positivity of the real power, and linarith.
Claim. For all real numbers $R, r_0, α$ with $R > 0$ and $r_0 > 0$, $1 < 1 + C_{lock} (R/r_0)^α$, where $C_{lock} = φ^{-3/2} > 0$.
background
The ILG real-exponent module defines the radial weight w_real(R, r0, α) := 1 + C_lock ⋅ (R/r0)^α, extending the asymptotic natural-power results to real exponents via Real.rpow. C_lock is the locked amplitude φ^{-3/2}, introduced to keep proofs independent of the specific power. The module proves four structural facts for this weight when the base is positive: it lies above one, is strictly monotone in R, is unbounded as R → ∞, and produces velocity-squared domination over the Newtonian term.
proof idea
Unfold w_real. Apply C_lock_pos to obtain 0 < C_lock. Use div_pos on the two positivity hypotheses to obtain 0 < R/r0. Invoke Real.rpow_pos_of_pos to obtain 0 < (R/r0)^α. Multiply to obtain 0 < C_lock ⋅ (R/r0)^α. Finish with linarith.
why it matters
The theorem supplies the enhancement_above_one field inside the certificate ILGRealExponentEnhancementCert. It is invoked directly by ilg_real_velocity_sq_dominates_newtonian to obtain V_bar_sq ≤ w_real ⋅ V_bar_sq. In the Recognition framework it closes the structural layer of the real-exponent ILG extension, supporting the gravity sector after the eight-tick octave and D = 3 have been forced in the unified chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.