module module

`IndisputableMonolith.Gravity.QGChannelRungDerivation`

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

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cosmology.PhiRungLadder module_import

declarations in this module (33)

def strongFieldRung L60
theorem strongFieldRung_eq_abs_eta_B_rung L63
theorem strongFieldRung_in_ladder L69
def ptaCorrectionValue L76
def ehtCorrectionValue L83
def sStarCorrectionValue L87
def cassiniCorrectionValue L93
def ringdownCorrectionValue L100
theorem ptaCorrectionValue_pos L104
theorem ehtCorrectionValue_pos L107
theorem sStarCorrectionValue_pos L110
theorem cassiniCorrectionValue_pos L113
theorem ringdownCorrectionValue_pos L116
theorem golden_ratio_partition L126
theorem golden_ratio_complement L138
theorem channel_rung_pair L147
theorem pta_sstar_same_base L151
theorem eht_eq_two_times_pta L155
theorem cassini_eq_three_times_pta L159
theorem ringdown_is_one_rung L164
structure DerivedChannelPrediction L173
def ptaDerived L183
def ehtDerived L194
def sStarDerived L205
def cassiniDerived L216
def ringdownDerived L227
def derivedChannels L239
theorem derivedChannels_length L242
theorem all_derived_channels_pos L245
theorem four_channels_share_rung_44 L250
theorem ringdown_rung_eq_1 L257
structure QGChannelRungDerivationCert L261
def qgChannelRungDerivationCert L269