weight_rs_positive
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not bound the numerical size of w-1 for any concrete t/τ₀.
- Does not select the dynamical time ratio appropriate to clusters.
- Does not address higher-order lensing terms beyond the first-order weight.
- Does not compare the RS weight against other modified-gravity models.
formal statement (Lean)
82theorem weight_rs_positive (t_ratio : ℝ) (ht : 0 < t_ratio) :
83 1 < weight_rs t_ratio := by
proof body
Tactic-mode proof.
84 unfold weight_rs
85 have h1 : 0 < C_lag_RS * t_ratio ^ alpha_RS := by
86 apply mul_pos
87 · unfold C_lag_RS cLagLock
88 -- φ^(-5) > 0 since φ > 0
89 have h_phi_pos : 0 < Foundation.PhiForcing.φ := Foundation.PhiForcing.phi_pos
90 exact Real.rpow_pos_of_pos h_phi_pos (-5)
91 · exact rpow_pos_of_pos ht alpha_RS
92 linarith
93
94/-- First-order lensing approximation for small weights.
95 When w ≈ 1 + ε with ε small, lensing corrections are O(ε). -/