coupling_product_small_proven
plain-language theorem explainer
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,
Claim. Let $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
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}.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.