pith. machine review for the scientific record. sign in
theorem proved term proof

simplicialFieldCurvatureCert

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

formal statement (Lean)

 184theorem simplicialFieldCurvatureCert : SimplicialFieldCurvatureCert where
 185  discharge := fun D a ha hinges G hCal =>

proof body

Term-mode proof.

 186    simplicial_linearization_discharge D a ha hinges G hCal
 187  identity := fun D a ha hinges G hCal ε =>
 188    field_curvature_identity_simplicial_einstein D a ha hinges G hCal ε
 189  cubic_calibrated := fun a ha G => cubic_calibrated_against_graph a ha G
 190  schlaefli_kills_linear := fun W η => linear_regge_vanishes W η
 191  kappa_value := Constants.kappa_einstein_eq
 192
 193end
 194
 195end SimplicialDeficitDischarge
 196end SimplicialLedger
 197end Foundation
 198end IndisputableMonolith

depends on (17)

Lean names referenced from this declaration's body.