module module high

`IndisputableMonolith.Gravity.GravityParameters`

GravityParameters supplies the RS-derived dynamical-time exponent α_gravity = 2·alphaLock together with upsilon_star and p_steepness. Gravity modelers in Recognition Science cite these constants when constructing radial or morphology corrections. The module consists solely of definitions and direct equalities to phi and alphaLock.

claim$\alpha_{\rm gravity}=2\cdot\alpha_{\rm Lock}=1-\phi^{-1}\approx0.382$, $\upsilon_*=\phi$, $p$ the steepness parameter fixed by the same relation.

background

The module belongs to the Gravity domain and imports only the Constants module, whose single definition is the RS time quantum τ₀ = 1 tick. It introduces the gravity-specific parameters that descend from the phi fixed point. The central object is the dynamical-time exponent expressed directly as α_gravity = 1 - 1/φ.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the constants required by the DerivedFactors module, which derives the morphology factor ξ and radial factor n(r) from SevenBeatViolation and ScaleGate saturation. It therefore closes the parameter interface for all subsequent gravity calculations in the Recognition framework.

scope and limits

Does not contain theorem statements or proofs.
Does not reference the forcing chain or J-uniqueness lemmas.
Does not compute numerical values beyond the phi expression.
Does not address observational constraints or HSB data.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.DerivedFactors module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (35)

def alpha_gravity L49
theorem alpha_gravity_eq_two_alphaLock L51
theorem alpha_gravity_pos L58
def upsilon_star L74
theorem upsilon_star_eq_phi L76
theorem upsilon_star_bounds L78
theorem upsilon_star_bounds_implies_pos L83
def C_xi L96
theorem C_xi_pos L102
def p_steepness L117
theorem p_steepness_eq L119
theorem p_steepness_pos L127
def A_amplitude L142
theorem A_amplitude_eq L144
theorem A_amplitude_bounds L152
def N_tau_galactic L186
def N_r_galactic L192
def galactic_constraint L196
def N_galactic L199
def a0_from_tau_r0 L203
def r0_from_tau_a0 L207
theorem tau_constraint_consistency L209
theorem a0_phi_ladder_formula L238
def F_12 L291
theorem F_12_is_fibonacci_12 L293
theorem F_12_is_perfect_square L295
def N_tau_conjecture L299
theorem N_tau_conjecture_eq_142 L301
def rung_offset L304
theorem rung_offset_is_power_of_2 L306
theorem rung_offset_is_perfect_square L308
theorem rung_offset_is_two_8tick_cycles L310
def N_r_conjecture L314
theorem N_r_conjecture_eq_126 L316
theorem rung_relationship L319