grLimitParameterFacts_proven
plain-language theorem explainer
The declaration supplies a concrete instance of the GRLimitParameterFacts class by wiring the three component theorems that bound the Recognition Science parameters alpha and cLag. A physicist deriving perturbative general-relativity limits from the Recognition spine would cite this instance to certify that the coupling remains small. The construction is a direct one-line wrapper that assembles the three proven bounds into the required structure.
Claim. Let $alpha = (1 - phi^{-1})/2$ and $C_{lag} = phi^{-5}$. Then $alpha < 1$, $C_{lag} < 1$, $|alpha · C_{lag}| < 0.02$, and $|alpha · C_{lag}| < 0.1$.
background
The module on parameter limits defines the class GRLimitParameterFacts to encode that the Recognition Science parameters remain small enough for perturbative treatment in general relativity. It derives alpha from the golden ratio geometry as (1 - 1/phi)/2 and cLag as phi to the minus five from the coherence energy scale. Upstream results supply the component bounds: rs_params_small_proven establishes both parameters less than one, rs_params_perturbative_proven shows their product less than 0.1 via alpha less than one half and cLag less than one tenth, and coupling_product_small_proven addresses the stricter product bound.
proof idea
The declaration is a one-line wrapper that directly assigns the three proven theorems to the fields of the GRLimitParameterFacts class: rs_params_small receives rs_params_small_proven, coupling_product_small receives coupling_product_small_proven, and rs_params_perturbative receives rs_params_perturbative_proven.
why it matters
This instance closes the parameter-bounds section and feeds downstream into coneEntropyStub for entropy calculations in the GR limit. It realizes the module claim that the ILG parameters are proven small and perturbative. The construction supports the perturbative regime needed to connect the Recognition spine to general relativity, while the coupling_product_small_proven documentation flags the open question of tightening the product bound to 0.02.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.