module module

`IndisputableMonolith.Gravity.MasterTheoremNonCircularityAudit`

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

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.MasterTheoremUnconditional module_import

declarations in this module (24)

theorem t0t8_clause_is_complete_forcing_chain L65
theorem t0t8_clause_holds L69
theorem costUniqueness_clause_is_carried L74
theorem costUniqueness_clause_holds L80
theorem bmv_clause_is_carried L85
theorem bmv_clause_holds L90
def placeholderClauseCount L94
theorem lorentzian_clause_is_cert L100
theorem hawking_clause_is_cert L107
theorem cRS_clause_is_cert L114
theorem carried_clauses_hold L120
theorem closed_certs_hold L129
def inhabitedCertClauseCount L144
theorem d2_regge_field_is L151
theorem d2_bianchi_field_is L157
theorem d3_amplitude_field_is L163
theorem d4_page_field_is L171
theorem all_witness_fields_hold L180
def witnessFieldClauseCount L195
theorem d4_page_field_nondegenerate L204
structure ClauseClassification L216
def masterClauseClassification L226
theorem masterClauseClassification_total L233
theorem master_theorem_non_circularity_certificate L252