module module

`IndisputableMonolith.Gravity.GravityParameters`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

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