coupling_product_small_proven
Researchers modeling perturbative general relativity limits cite the result that the absolute value of the product of the ILG exponent alpha equals (1 minus phi inverse) over two and the lag constant C_lag equals phi to the minus five is strictly less than 0.02. The bound confirms the coupling remains small enough for the GR approximation. The proof extracts positivity from rs_params_positive, establishes alpha below one fifth by verifying phi below five thirds through explicit square root comparisons, invokes the prior cLag_lt_one_tenth bound,
claimLet $phi = (1 + sqrt(5))/2$. Then $|((1 - phi^{-1})/2) * phi^{-5}| < 0.02$.
background
The module proves that ILG parameters alpha and C_lag extracted from Recognition Science remain small and perturbative. alpha_from_phi is defined as (1 - 1/phi)/2 and cLag_from_phi as phi^{-5}. The upstream theorem cLag_lt_one_tenth establishes phi^{-5} < 1/10 while rs_params_positive confirms both quantities are positive. Module documentation states the parameters arise from RS geometry with alpha approximately 0.191 and C_lag approximately 0.090, and records the explicit goal of proving their product below 0.02.
proof idea
The tactic proof first obtains positivity of both factors from rs_params_positive and rewrites the absolute value via abs_of_nonneg. It then proves alpha_from_phi < 1/5 by unfolding the definition, showing Constants.phi < 5/3 via Real.sqrt_lt applied to 5 < (7/3)^2, followed by linarith and calc chains that reach the target inequality. It applies cLag_lt_one_tenth to bound the second factor and finishes with mul_lt_mul'' to obtain the product bound below 1/50.
why it matters in Recognition Science
This theorem supplies the coupling_product_small field inside the grLimitParameterFacts_proven instance that realizes the GRLimitParameterFacts structure. It closes the explicit status note in the module documentation that required either alpha below 1/5 or a tighter C_lag bound to reach product below 0.02. In the Recognition Science framework the result confirms the perturbative character of parameters on the phi-ladder, consistent with the native constants c = 1 and hbar = phi^{-5}.
scope and limits
- Does not compute the exact numerical value of the product.
- Does not establish the bound under small perturbations to phi.
- Does not address products formed with other RS-derived parameters.
- Does not extend the argument to higher-order terms in the GR expansion.
formal statement (Lean)
157theorem coupling_product_small_proven : |alpha_from_phi * cLag_from_phi| < 0.02 := by
proof body
Tactic-mode proof.
158 have hα_pos := rs_params_positive.1
159 have hC_pos := rs_params_positive.2
160 rw [abs_of_nonneg (mul_nonneg (le_of_lt hα_pos) (le_of_lt hC_pos))]
161
162 -- Strategy: Prove α < 1/5
163 -- Need: (1 - 1/φ)/2 < 1/5
164 -- ⟺ 1 - 1/φ < 2/5
165 -- ⟺ 1 - 2/5 < 1/φ
166 -- ⟺ 3/5 < 1/φ
167 -- ⟺ φ < 5/3
168
169 have hα_lt_one_fifth : alpha_from_phi < 1 / 5 := by
170 unfold alpha_from_phi
171 have hφ_pos : 0 < Constants.phi := Constants.phi_pos
172
173 -- Need to prove φ < 5/3
174 have hφ_lt_5_3 : Constants.phi < 5 / 3 := by
175 unfold Constants.phi
176 -- (1+√5)/2 < 5/3
177 -- ⟺ 3(1+√5) < 10
178 -- ⟺ 3 + 3√5 < 10
179 -- ⟺ 3√5 < 7
180 -- ⟺ √5 < 7/3
181 -- ⟺ 5 < 49/9
182 -- 5 = 45/9 < 49/9 ✓
183 have h_sqrt5_lt : Real.sqrt 5 < 7 / 3 := by
184 -- use sqrt_lt equivalence: √x < y ↔ x < y^2
185 have hx : 0 ≤ (5 : ℝ) := by norm_num
186 have hy : 0 ≤ (7 / 3 : ℝ) := by norm_num
187 have hxy : (5 : ℝ) < (7 / 3 : ℝ) ^ 2 := by norm_num
188 exact (Real.sqrt_lt hx hy).2 hxy
189 have : 1 + Real.sqrt 5 < 1 + 7 / 3 := by linarith
190 have : (1 + Real.sqrt 5) / 2 < (1 + 7 / 3) / 2 := by
191 exact div_lt_div_of_pos_right this (by norm_num)
192 calc (1 + Real.sqrt 5) / 2
193 < (1 + 7 / 3) / 2 := this
194 _ = 10 / 6 := by norm_num
195 _ = 5 / 3 := by norm_num
196
197 -- Now: φ < 5/3 ⟹ 1/φ > 3/5 ⟹ 1 - 1/φ < 2/5 ⟹ α < 1/5
198 have : 1 / Constants.phi > 3 / 5 := by
199 -- From φ < 5/3 and φ > 0, we get 1/(5/3) < 1/φ i.e., 3/5 < 1/φ
200 have hpos : 0 < Constants.phi := hφ_pos
201 have : 1 / (5 / 3 : ℝ) < 1 / Constants.phi :=
202 one_div_lt_one_div_of_lt hpos hφ_lt_5_3
203 simpa using this
204 have : 1 - 1 / Constants.phi < 2 / 5 := by linarith
205 have : (1 - 1 / Constants.phi) / 2 < (2 / 5) / 2 := by
206 exact div_lt_div_of_pos_right this (by norm_num)
207 calc (1 - 1 / Constants.phi) / 2
208 < (2 / 5) / 2 := this
209 _ = 1 / 5 := by norm_num
210
211 have hC_lt : cLag_from_phi < 1 / 10 := cLag_lt_one_tenth
212
213 calc alpha_from_phi * cLag_from_phi
214 < (1 / 5) * (1 / 10) := by
215 apply mul_lt_mul'' hα_lt_one_fifth hC_lt (le_of_lt hα_pos) (le_of_lt hC_pos)
216 _ = 1 / 50 := by norm_num
217 _ = 0.02 := by norm_num
218
219/-- PROVEN: Both parameters < 1. -/