module module

`IndisputableMonolith.Gravity.QGObservableSignalModels`

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.MasterTheoremUnconditional module_import

depends on (5)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cosmology.PhiRungLadder module_import
IndisputableMonolith.Gravity.MasterTheorem module_import
IndisputableMonolith.Gravity.PTAStructural module_import
IndisputableMonolith.Gravity.StrongFieldStructural module_import

declarations in this module (15)

structure ObservationChannelSignalModel L37
def ptaChannel L50
def ehtChannel L66
def sStarChannel L84
def cassiniChannel L100
def ringdownChannel L119
def qgChannels L136
theorem qgChannels_length L139
theorem all_channels_separated L143
def ptaSignalModelWitness L152
def strongFieldSignalModelWitness L161
structure QGObservableSignalModelsCert L176
def qgObservableSignalModelsCert L182
theorem qgObservableSignalModelsCert_inhabited L188
theorem qg_observable_signal_models_one_statement L196