theorem
proved
rs_kappa_pos
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Gravity.ReggeCalculus on GitHub at line 219.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
216 with kappa = 8*phi^5. -/
217noncomputable def rs_kappa : ℝ := 8 * phi ^ 5
218
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