IsFlat
plain-language theorem explainer
IsFlat defines flatness for a tetrahedron by the vanishing of its Cayley-Menger determinant value. Researchers in discrete geometry and Regge calculus cite this predicate when identifying degenerate simplices. The definition consists of a direct equality to zero on the supplied determinant scalar.
Claim. For edge-length data $T$ and Cayley-Menger data $cm$, the tetrahedron is flat when $cm.value = 0$.
background
TetEdges is the structure holding six positive real numbers as edge lengths of a tetrahedron, with squared lengths defined positively. TetCMData is the structure carrying the scalar value of the Cayley-Menger determinant for those edges, including a regularity condition that the value equals twice the sixth power of the side length when all edges are equal. The module sets up the determinant for tetrahedra as part of Phase C1 in discharging the ReggeDeficitLinearizationHypothesis. It adopts a minimal approach by defining the determinant directly as a scalar from edge lengths and recording volume identities as named hypotheses rather than proving full classical results. This local setting enables later phases for dihedral angles and Schläfli identities while keeping the module free of sorry and new axioms.
proof idea
The definition is a one-line wrapper that equates the flatness proposition to the condition that the Cayley-Menger value equals zero.
why it matters
IsFlat supplies the degeneracy predicate used in CayleyMengerCert to package Phase C1 results and in the theorem showing regular tetrahedra are non-flat. It completes the degenerate case handling in the Cayley-Menger setup, aligning with the framework's T8 for three spatial dimensions and the overall bridge to Regge calculus. It touches the open question of full classical Euclidean geometry proofs being left as hypotheses for downstream modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.