CayleyMengerCert
plain-language theorem explainer
The CayleyMengerCert structure packages four properties of the Cayley-Menger scalar on regular tetrahedra: explicit value 2a^6, strict positivity, identity with the squared volume formula, and non-degeneracy. Researchers working on simplicial Regge calculus cite it to invoke the full set of Phase C1 facts in one record. The definition is a direct structure that assembles the four sibling lemmas without additional reasoning.
Claim. A structure asserting that for every regular tetrahedron with edge length $a>0$, the Cayley-Menger scalar equals $2a^6$, is strictly positive, satisfies the identity $144((a^3 sqrt(2)/12)^2)$, and the configuration is non-flat.
background
The module develops the Cayley-Menger determinant for tetrahedra as Phase C1 toward discharging the Regge deficit linearization hypothesis for simplicial complexes. A RegularTet consists of a positive real edge length a together with the TetEdges obtained by setting all six lengths equal to a. IsFlat is the predicate that the CM scalar vanishes, marking degeneracy to a point.
proof idea
This is a structure definition. The downstream theorem cayleyMengerCert constructs the instance by supplying the four lemmas regular_cm_value_eq, regular_cm_positive, regular_cm_volume_identity, and regular_not_flat directly into the respective fields.
why it matters
The structure packages the Phase C1 results for the Cayley-Menger determinant on regular tetrahedra, enabling the chain through dihedral angles, Schläfli identities, and simplicial deficit discharge in later phases. It supplies the concrete certificate consumed by cayleyMengerCert. In the Recognition Science setting it supplies the explicit non-flat volume identity required for the geometry bridge in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.