module module high

`IndisputableMonolith.Gravity.GravityParameters`

GravityParameters supplies the RS-derived constants for gravitational dynamics, centered on the exponent α_gravity = 2 α_Lock = 1 - φ^{-1} ≈ 0.382. Researchers modeling modified Newtonian dynamics or RS cosmology cite these when constructing radial density profiles. The module provides definitions together with elementary bounds and positivity lemmas for the full parameter set.

claim$α_{gravity} = 2 α_{Lock} = 1 - φ^{-1} ≈ 0.382$, together with $υ_* = φ$, $C_ξ$, and $p_{steepness}$ in RS-native units.

background

This module sits in the Gravity domain and imports the base constants from IndisputableMonolith.Constants, where τ₀ denotes the fundamental RS time quantum equal to one tick. It introduces the dynamical-time exponent α_gravity together with auxiliary quantities such as upsilon_star, C_xi, and p_steepness that enter radial and morphological corrections. The definitions rest on the phi-ladder and the Recognition Composition Law.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The parameters defined here are imported by DerivedFactors to construct the ξ morphology factor and n(r) radial profile. That downstream module uses them to address the HSB overprediction problem in the ILG convolution kernel via SevenBeatViolation and ScaleGate saturation logic. It fills the gravity-parameter slot in the T8 forcing chain that sets D=3 and the phi-based mass ladder.

scope and limits

Does not prove the value of alphaLock from the forcing chain.
Does not connect these parameters to observational data.
Does not derive the full gravitational potential.
Does not address quantum corrections or higher-order terms.

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