module module

`IndisputableMonolith.Gravity.Track1BCStructural`

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.MasterTheoremStructural module_import
IndisputableMonolith.Gravity.Track1BCPhysicalResidual module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Geometry.DiscreteBianchi module_import
IndisputableMonolith.Gravity.MasterTheorem module_import

declarations in this module (14)

structure with L70
theorem requires L72
def abstract_regge_action L88
def abstract_eh_action L92
def regge_eh_continuum_structural_prop L100
theorem regge_eh_continuum_canonical_witness L103
def discrete_bianchi_structural_prop L114
theorem discrete_bianchi_canonical_witness L118
theorem reg_eh_continuum_and_bianchi_structural_holds L128
def regEHContinuumAndBianchiWitness L140
structure Track1BCStructuralCert L149
def track1BCStructuralCert L157
theorem track1BCStructuralCert_inhabited L163
theorem track1BC_one_statement L176