weight_rs_positive
plain-language theorem explainer
The theorem shows that the RS weight function w(t) = 1 + C_lag (t/τ₀)^α strictly exceeds 1 whenever the time ratio t/τ₀ is positive. Cluster-lensing calculations cite it to guarantee that ILG corrections remain enhancements rather than reductions. The proof unfolds the definition, establishes positivity of the product term via the locked C_lag = φ^{-5} and real-power positivity, then closes with linear arithmetic.
Claim. Let $w(t) = 1 + C_0 (t/τ_0)^α$ where $C_0 = φ^{-5} > 0$ and $α = (1 - 1/φ)/2 ≈ 0.191$. Then for every real $t > 0$, $w(t) > 1$.
background
The module formalizes Induced Light Gravity lensing at cluster scales under Recognition Science parameter locks. The weight function is defined as weight_rs(t_ratio) = 1 + C_lag_RS * t_ratio ^ alpha_RS, with C_lag_RS := cLagLock = φ^{-5} and alpha_RS := alphaLock = (1 - 1/φ)/2. These locks come from the forcing chain (T5 J-uniqueness and T6 phi fixed point) and are imported via Constants.cLagLock and GravityBridge.C_lag_RS. The local setting states that RS predicts κ/κ_GR ≈ 1 + O(C_lag α) ≈ 1 + O(0.02) at cluster scales.
proof idea
The tactic proof unfolds weight_rs, then applies mul_pos to the product C_lag_RS * t_ratio^alpha_RS. Positivity of C_lag_RS follows from phi_pos and Real.rpow_pos_of_pos at exponent -5; positivity of the power follows from rpow_pos_of_pos at the positive t_ratio. The final linarith step converts the strict positivity of the added term into the desired 1 < w inequality.
why it matters
The result anchors the claim that ILG deviations remain positive enhancements under RS locks, feeding the module's key statement that cluster lensing corrections stay within 1–2 % of GR. It directly supports the downstream lensing_correction_first_order and rs_lensing_correction_bounded siblings. The open numerical question left in the doc-comment (correct t/τ₀ for clusters) remains untouched; the theorem only guarantees the sign, not the size, of the correction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.