`regular_not_flat`

proved

show as: view math explainer →

module: IndisputableMonolith.Geometry.CayleyMenger
domain: Geometry
line: 201 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Geometry.CayleyMenger on GitHub at line 201.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 198  cm.value = 0
 199
 200/-- A regular tetrahedron is non-flat. -/
 201theorem regular_not_flat (R : RegularTet) : ¬ IsFlat R.toTetEdges R.cmData := by
 202  unfold IsFlat
 203  rw [regular_cm_value_eq]
 204  have := regular_cm_positive R
 205  rw [regular_cm_value_eq] at this
 206  linarith
 207
 208/-! ## §6. Cayley-Menger Certificate -/
 209
 210/-- Packages the results of Phase C1. -/
 211structure CayleyMengerCert where
 212  regular_value : ∀ R : RegularTet, R.cmData.value = 2 * R.a ^ 6
 213  regular_positive : ∀ R : RegularTet, 0 < R.cmData.value
 214  regular_volume_identity : ∀ R : RegularTet,
 215    R.cmData.value = 144 * ((R.a ^ 3 * Real.sqrt 2) / 12) ^ 2
 216  regular_not_flat : ∀ R : RegularTet, ¬ IsFlat R.toTetEdges R.cmData
 217
 218theorem cayleyMengerCert : CayleyMengerCert where
 219  regular_value := regular_cm_value_eq
 220  regular_positive := regular_cm_positive
 221  regular_volume_identity := regular_cm_volume_identity
 222  regular_not_flat := regular_not_flat
 223
 224end
 225
 226end CayleyMenger
 227end Geometry
 228end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.