GRLimitParameterFacts
plain-language theorem explainer
GRLimitParameterFacts packages three inequalities on the Recognition Science parameters alpha and cLag to establish they are small enough to support perturbative expansions in the ILG-to-GR limit. Researchers deriving effective field equations from the Recognition spine would cite the class to license the small-coupling regime. The declaration is a bare class that collects the statements for later instantiation by explicit lemmas.
Claim. Let $α = (1 - φ^{-1})/2$ and $C_{lag} = φ^{-5}$. Then $α < 1$, $C_{lag} < 1$, $|α C_{lag}| < 0.02$, and $|α C_{lag}| < 0.1$.
background
The module proves that ILG parameters derived from Recognition Science remain small enough for perturbation theory. Upstream definitions give α = (1 - 1/φ)/2 ≈ 0.191 from RS geometry and C_lag = φ^{-5} ≈ 0.090 from the coherence quantum E_coh = φ^{-5} eV. The local setting is the GR limit of the Recognition framework, where these bounds justify treating the coupling as perturbative rather than assuming it outright.
proof idea
The declaration is a class definition with no body. It simply declares the three fields rs_params_small, coupling_product_small, and rs_params_perturbative as propositions. Concrete proofs are supplied downstream by the grLimitParameterFacts_proven instance, which wires in the separate lemmas rs_params_small_proven, coupling_product_small_proven, and rs_params_perturbative_proven.
why it matters
The class supplies the interface that lets the Recognition Science parameters enter the GR limit as a controlled perturbation. It is instantiated by grLimitParameterFacts_proven and is referenced by coneEntropyStub. The module doc states that the product bounds require φ^5 > 10, with the tighter 0.02 bound still needing refinement. This step supports the small-coupling regime used in the eight-tick octave and spatial-dimension derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.