enhancement_real_strict_mono
plain-language theorem explainer
The theorem establishes that the real-exponent radial enhancement w(R, r0, α) = 1 + C_lock (R/r0)^α is strictly increasing in the radial coordinate R whenever the inputs are positive and the exponent α is positive. Modelers extending ILG gravity to the locked real exponent would cite this monotonicity when verifying that the enhancement factor grows outward. The tactic proof unfolds the definition, confirms positivity and ordering of the scaled radii, applies the real-power strict-increase lemma, scales by the positive lock constant, and closes
Claim. Let $w(R, r_0, α) := 1 + C_{lock} (R/r_0)^α$ with $C_{lock} = φ^{-3/2} > 0$. Then $0 < R_1 < R_2$, $0 < r_0$, and $0 < α$ together imply $w(R_1, r_0, α) < w(R_2, r_0, α)$.
background
The module supplies structural facts for the real-exponent version of ILG radial enhancement, using the locked exponent α = 1 − 1/φ ∈ (0,1) and the definition w_real(R, r0, α) = 1 + C_lock ⋅ (R/r0)^α. C_lock is the positive locked amplitude √(1/φ³). The anchor r0 supplies φ-exponent offsets per sector derived from wallpaper and cube geometry. Upstream, C_lock_pos records positivity of the amplitude while lt_trans supplies order transitivity used to compare scaled radii.
proof idea
The tactic proof unfolds w_real, obtains 0 < C_lock from C_lock_pos, shows 0 < R1/r0 and 0 < R2/r0 via div_pos, and obtains R1/r0 < R2/r0 by combining lt_trans with mul_lt_mul_of_pos_right and div_eq_mul_inv. It then invokes Real.rpow_lt_rpow to compare the powers, scales the inequality by mul_lt_mul_of_pos_left, and finishes with linarith.
why it matters
The result supplies the strict-monotonicity clause required by the downstream certificate ilgRealExponentEnhancementCert_holds, which assembles positivity, above-one, monotonicity, and unboundedness facts for the real-exponent ILG enhancement. It completes one of the four structural facts listed in the module for the Phase D9 extension of the asymptotic-enhancement work. Monotonicity is consistent with the Recognition framework's eight-tick octave and D = 3 spatial structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.