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)
201theorem regular_not_flat (R : RegularTet) : ¬ IsFlat R.toTetEdges R.cmData := by
proof body
Term-mode proof.
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. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (11)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
IsFlat
in IndisputableMonolith.Geometry.CayleyMenger
decl_use
-
regular_cm_positive
in IndisputableMonolith.Geometry.CayleyMenger
decl_use
-
regular_cm_value_eq
in IndisputableMonolith.Geometry.CayleyMenger
decl_use
-
RegularTet
in IndisputableMonolith.Geometry.CayleyMenger
decl_use
-
Phase
in IndisputableMonolith.Information.ChurchTuringPhysicsStructure
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
Phase
in IndisputableMonolith.RRF.Hypotheses.EightTick
decl_use