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

regge_calculus_cert

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)

 237theorem regge_calculus_cert : ReggeCalculusCert where
 238  flat_vanishes := regge_action_flat

proof body

Term-mode proof.

 239  cubic_flat := cubic_lattice_flat
 240  deficit_positive := deficit_pos_of_angle_deficit
 241  deficit_negative := deficit_neg_of_angle_excess
 242  kappa_positive := rs_kappa_pos
 243  kappa_derived := rs_kappa_value
 244
 245end
 246
 247end ReggeCalculus
 248end Gravity
 249end IndisputableMonolith

depends on (7)

Lean names referenced from this declaration's body.