rs_params_small_proven
plain-language theorem explainer
The theorem establishes that the Recognition Science-derived parameters alpha and cLag are both strictly less than one. Physicists working on perturbative limits in general relativity would cite this result to justify the smallness of coupling constants in the ILG framework. The proof is a direct conjunction of two prior inequalities for alpha and for cLag.
Claim. Let $alpha = (1 - phi^{-1})/2$ and $C_{lag} = phi^{-5}$. Then $alpha < 1$ and $C_{lag} < 1$.
background
The GRLimit.Parameters module connects Recognition Science to general relativity limits by defining two parameters from the golden ratio phi. Alpha equals (1 minus 1 over phi) divided by 2, drawn from RS geometry, while cLag equals phi to the power of negative five, taken from the coherence quantum scale. The module proves these ILG parameters are small enough to support perturbation theory rather than assuming the bounds.
proof idea
The proof is a term-mode one-line wrapper that constructs the conjunction by pairing the upstream theorems alpha_lt_one and cLag_lt_one.
why it matters
This supplies the rs_params_small field inside the grLimitParameterFacts_proven instance that instantiates GRLimitParameterFacts with actual proofs. It fills the small-parameter requirement stated in the module documentation from Source.txt line 26, confirming the perturbative regime for the Recognition Science connection to relativity limits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.