IndisputableMonolith.Relativity.GRLimit.Parameters
The Parameters module defines the ILG exponent α = (1 - 1/φ)/2 ≈ 0.191 from Recognition Science together with bounds on related RS parameters for the GR limit. Researchers setting up perturbative relativity models from the RS framework would cite these facts. The module assembles definitions such as alpha_from_phi and lemmas establishing positivity and perturbative validity.
claim$α = (1 - φ^{-1})/2 ≈ 0.191$ with rs parameters satisfying positivity, α < 1/2, and perturbative smallness.
background
The module resides in the Relativity.GRLimit subdomain and imports the base constant τ₀ = 1 tick from IndisputableMonolith.Constants. It introduces the exponent α derived from the self-similar fixed point φ, along with cLag and the full set of rs parameters on the phi-ladder. The local theoretical setting prepares these quantities for the GR limit while ensuring they obey the inequalities required by the Recognition Composition Law.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies grLimitParameterFacts_proven, which the downstream ParametersTest module verifies as available with all bounds holding. It provides the RS-derived α for the GR limit analysis and connects the parameter facts to the broader Recognition Science chain.
scope and limits
- Does not derive the full GR limit equations.
- Does not address non-perturbative regimes.
- Does not perform numerical simulations of the parameters.
- Does not interface with experimental observations.
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