module module

`IndisputableMonolith.Gravity.DiscriminatorMatrix`

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 (2)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.MasterTheorem module_import
IndisputableMonolith.Verification.Track6FalsifierSensitivity module_import

depends on (5)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Gravity.BlackHoleEchoesFromBounce module_import
IndisputableMonolith.Gravity.BlackHoleEntropyFromLedger module_import
IndisputableMonolith.Gravity.BlackHoleEntropySI module_import
IndisputableMonolith.Gravity.DiscriminatorCert module_import

declarations in this module (23)

inductive Rival L82
inductive Sector L92
def rivalPrediction L103
def rsPredictionLower L120
def rsPredictionUpper L126
theorem cell_LQG_LeadingLog L142
theorem cell_LQG_EchoDamping L147
theorem cell_LQG_RungPhase L152
theorem cell_String_LeadingLog L157
theorem cell_String_EchoDamping L163
theorem cell_String_RungPhase_positive L169
theorem cell_CDT_LeadingLog_distinct L175
theorem cell_CDT_EchoDamping_positive L180
theorem cell_CDT_RungPhase_positive L184
theorem cell_Bohmian_LeadingLog_distinct L190
theorem cell_Bohmian_EchoDamping_positive L195
theorem cell_Bohmian_RungPhase_positive L200
structure DiscriminatorMatrixCert L212
def discriminatorMatrixFull L236
theorem discriminatorMatrixFull_inhabited L253
structure PerRivalDistinguishability L262
def perRivalDistinguishability_holds L272
theorem discriminator_matrix_one_statement L294