enhancement_above_one
plain-language theorem explainer
The radial weight function in Information-Limited Gravity is strictly greater than one for every positive radius and every positive integer exponent. Galaxy rotation-curve analysts cite the result to guarantee that the ILG-modified velocity squared exceeds the Newtonian baryonic prediction at all radii. The proof unfolds the definition of w_radial, establishes positivity of the added term via C_lock_pos and pow_pos, and concludes by linarith.
Claim. For all real numbers $R>0$, $r_0>0$ and natural numbers $n>0$, the radial weight satisfies $1 < 1 + C_0 (R/r_0)^n$, where $C_0 = C_0 > 0$ is the locked amplitude.
background
The module proves structural facts for the ILG radial weight used in the φ-locked SPARC analysis (Phase D9). The weight is defined as w_radial(R, r0, n) := 1 + C_lock * (R/r0)^n, where C_lock is the positive abstract constant sqrt(1/phi^3) chosen to match the three-channel factorization while avoiding real exponents. Its positivity is established separately by C_lock_pos using phi_pos and Real.sqrt_pos. The parameter r0 is a positive real scale (distinct from the integer offset in Masses.Anchor). Together with positivity, strict monotonicity and unboundedness, the above-one property ensures the ILG velocity squared cannot decay Keplerianly.
proof idea
The term-mode proof unfolds w_radial to expose the added term. It applies pow_pos to the positive ratio R/r0 (using div_pos) to obtain a positive power, combines it with C_lock_pos via mul_pos to show the product is positive, and finishes with linarith to conclude that 1 plus a positive quantity exceeds 1.
why it matters
The theorem populates the ILGAsymptoticEnhancementCert structure, which is shown inhabited by ilgAsymptoticEnhancementCert_holds. The certificate is invoked by ilg_velocity_sq_dominates_newtonian to prove V²(R) = w(R)·V_bar²(R) ≥ V_bar²(R). It supplies one of the four structural facts required for the Phase D9 claim that rotation curves remain above the Newtonian envelope and grow without bound, consistent with the eight-tick octave and phi-ladder mass scaling in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.