IndisputableMonolith.Relativity.GRLimit.Parameters
The module supplies the Recognition Science value for the ILG exponent α = (1 - 1/φ)/2 ≈ 0.191 together with bounds on related coupling parameters such as cLag. Researchers working on the general relativity limit of Recognition Science cite these definitions to fix the perturbative regime. The module is a collection of direct definitions and elementary inequalities derived from the phi-ladder constants.
claimThe ILG exponent is defined by $α = (1 - φ^{-1})/2 ≈ 0.191$, with $c_{Lag}$ and the remaining RS parameters obeying the listed positivity and smallness bounds in phi-based units.
background
This module sits inside the Relativity.GRLimit section and imports the fundamental RS time quantum τ₀ = 1 tick from Constants. It defines the ILG exponent α from the Recognition Science framework as α = (1 - 1/φ)/2. The sibling declarations establish positivity, upper bounds such as α < 1/2, and smallness of the coupling product for the perturbative regime.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module feeds the smoke tests in ParametersTest that verify grLimitParameterFacts_proven. It supplies the concrete numerical bounds required by the GRLimit construction in the Recognition Science derivation of general relativity, closing the parameter interface for the alpha band and phi-ladder constants.
scope and limits
- Does not derive the value of φ from first principles.
- Does not prove the full GRLimit theorem.
- Does not address non-perturbative regimes.
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