theorem
proved
rs_kappa_value
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Gravity.ReggeCalculus on GitHub at line 222.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
219theorem rs_kappa_pos : 0 < rs_kappa := by
220 unfold rs_kappa; exact mul_pos (by norm_num) (pow_pos phi_pos 5)
221
222theorem rs_kappa_value : rs_kappa = 8 * phi ^ 5 := rfl
223
224/-! ## Regge Calculus Certificate -/
225
226structure ReggeCalculusCert where
227 flat_vanishes : ∀ hinges,
228 (∀ h ∈ hinges, deficit_angle h = 0) → regge_action hinges = 0
229 cubic_flat : 2 * Real.pi - 4 * (Real.pi / 2) = 0
230 deficit_positive : ∀ h : HingeData,
231 h.dihedral_angles.sum < 2 * Real.pi → 0 < deficit_angle h
232 deficit_negative : ∀ h : HingeData,
233 2 * Real.pi < h.dihedral_angles.sum → deficit_angle h < 0
234 kappa_positive : 0 < rs_kappa
235 kappa_derived : rs_kappa = 8 * phi ^ 5
236
237theorem regge_calculus_cert : ReggeCalculusCert where
238 flat_vanishes := regge_action_flat
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