TetVolumeIdentity
plain-language theorem explainer
The declaration records the classical Cayley-Menger volume formula for a tetrahedron as a named hypothesis equating 288 V squared to the determinant value computed from six edge lengths. Researchers discharging ReggeDeficitLinearizationHypothesis or building simplicial geometry bridges in Recognition Science would cite it as the minimal interface for Phase C1. It is introduced as a direct equality definition that avoids embedding the full 19th-century proof.
Claim. For a tetrahedron with edge lengths given by structure $T$ and Cayley-Menger determinant value supplied by structure $cm$, the volume $V$ satisfies $288 V^2 = cm.value$.
background
TetEdges is the structure holding six positive real edge lengths together with their squared versions. TetCMData packages the explicit Cayley-Menger determinant value, which evaluates to $2a^6$ when all edges equal $a>0$ and records the classical polynomial form as a Prop. The module CayleyMenger defines these objects for $n=3$ simplices as Phase C1 of the program to discharge ReggeDeficitLinearizationHypothesis for general simplicial complexes. It deliberately records the volume identity as a named hypothesis rather than reproving the classical result, matching the pattern used for other piecewise-flat geometry facts.
proof idea
The declaration is a direct definition stating the equality $288 V^2 = cm.value$. No lemmas or tactics are applied; it functions as a one-line named hypothesis interface for the classical Cayley-Menger formula.
why it matters
This definition supplies the volume relation required by the simplicial ledger and is referenced by TetEdges constructions. It fills the Phase C1 slot toward discharging ReggeDeficitLinearizationHypothesis, citing the classical Cayley-Menger theorem (Cayley 1841, Menger 1928). The module enables downstream phases for dihedral angles and Schläfli identities while keeping the Euclidean content minimal and zero-sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.