module module high

`IndisputableMonolith.Gravity.GravityParameters`

GravityParameters supplies the RS-derived dynamical-time exponent α_gravity = 2 α_lock = 1 - φ^{-1} ≈ 0.382 along with upsilon_star, C_xi and p_steepness. Gravity modelers in the Recognition Science program cite these values when building radial and morphology corrections. The module consists of direct definitions, equality lemmas and positivity statements grounded in the phi constants imported from Constants.

claim$\alpha_{\rm gravity} := 2 \cdot \alpha_{\rm lock} = 1 - \phi^{-1} \approx 0.382$, together with $\upsilon_* = \phi$, $C_\xi > 0$ and steepness parameter $p$ satisfying the listed equalities and bounds.

background

The module resides in the Gravity domain and imports the RS time quantum τ₀ = 1 tick from Constants. It defines the dynamical-time exponent α_gravity as twice the lock parameter and equal to one minus the reciprocal of phi, together with the auxiliary constants upsilon_star, C_xi and p_steepness. These objects sit inside the larger Recognition Science construction that begins from J-uniqueness and the phi-ladder.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The parameters feed directly into the DerivedFactors module, which derives the ξ morphology and n(r) radial factors from SevenBeatViolation and ScaleGate saturation. The downstream module states that the ILG kernel overpredicts rotation and uses these gravity parameters to correct the HSB discrepancy.

scope and limits

Does not derive α_gravity from the T0-T8 forcing chain.
Does not connect the parameters to the electromagnetic fine-structure interval.
Does not address the mass-ladder or Berry creation threshold.
Does not incorporate the eight-tick octave or D = 3 forcing.

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