IndisputableMonolith.Relativity.GRLimit.Parameters
Defines the Recognition Science parameter pack for the GR limit of ILG gravity: the exponent α = (1 − 1/φ)/2 ≈ 0.191 and the lag coupling c_Lag built from φ. Supplies positivity and smallness lemmas used when recovering Newtonian/GR weak-field behaviour. Anyone citing the proven GR-limit parameter facts or the smoke tests would import this module. Content is definitions plus elementary inequalities on φ.
claimThe module introduces the ILG exponent $\alpha = (1 - 1/\varphi)/2 \approx 0.191$ and the lag constant $c_{\mathrm{Lag}}$ derived from the golden ratio $\varphi$, together with positivity, $\alpha < 1/2$, $c_{\mathrm{Lag}} < 1/10$, and related perturbative smallness statements packaged as GR-limit parameter facts.
background
In Recognition Science the golden ratio $\varphi$ is forced as the self-similar fixed point (T6). The ILG (information-limited gravity) modification of the Newtonian potential is controlled by a single dimensionless exponent $\alpha$ built from $\varphi$, together with a lag/coupling scale $c_{\mathrm{Lag}}$. The present module lives in the Relativity.GRLimit hierarchy and records the concrete RS-native formulae for those parameters.
Upstream it only needs the Constants module (which supplies $\varphi$ and the RS time quantum $\tau_0$). Downstream the values are consumed by the GR-limit analysis that shows the ILG correction becomes perturbatively small in the appropriate regime, recovering ordinary GR/Newtonian behaviour.
Sibling declarations include the raw definitions alpha_from_phi and cLag_from_phi, elementary comparisons such as $\alpha < 1/2$ and $c_{\mathrm{Lag}} < 1/10$, and the bundled structure GRLimitParameterFacts that packages the proven bounds.
proof idea
Primarily a definition module. The core objects are closed-form expressions in $\varphi$. The accompanying lemmas are short inequality proofs: positivity of the RS parameters, $\varphi > 3/2$, $\alpha < 1$ and $\alpha < 1/2$, $c_{\mathrm{Lag}} < 1/10$ and $c_{\mathrm{Lag}} < 1$, and the composite statements that the parameters are perturbative and that the coupling product is small. No deep tactic machinery; each bound follows from the algebraic definition of $\varphi$ and standard real arithmetic.
why it matters in Recognition Science
Supplies the numerical and symbolic parameter pack required by every subsequent GR-limit theorem in the Relativity hierarchy. The bundled facts are imported by the smoke-test module ParametersTest, which checks that the rigorous instance is available and that all stated bounds hold. Without these definitions the claim that ILG reduces to GR in the appropriate limit cannot even be stated in RS-native units. The module therefore sits at the interface between the forcing chain (φ from T6) and the concrete weak-field recovery arguments.
scope and limits
- Does not derive the ILG field equations or the GR-limit theorem itself.
- Does not prove uniqueness of α; only records the RS formula.
- Does not address cosmological or strong-field regimes.
- Does not numerically evaluate α beyond the symbolic expression in φ.
- Does not depend on measured G, c or ħ; works in RS-native units.
used by (1)
depends on (1)
declarations in this module (13)
-
def
alpha_from_phi -
def
cLag_from_phi -
theorem
rs_params_positive -
theorem
alpha_lt_one -
theorem
alpha_lt_half -
theorem
phi_gt_three_halves -
theorem
cLag_lt_one_tenth -
theorem
cLag_lt_one -
theorem
rs_params_perturbative_proven -
theorem
coupling_product_small_proven -
theorem
rs_params_small_proven -
class
GRLimitParameterFacts -
instance
grLimitParameterFacts_proven