IndisputableMonolith.Geometry.CayleyMenger
This module supplies edge-length data structures and Cayley-Menger determinant identities for tetrahedra. It is cited by the four downstream modules that compute dihedral angles, linearize deficits, and discharge the Regge hypothesis. The module contains only definitions for TetEdges, TetCMData, volume identities, and positivity checks.
claimThe module defines edge-length data $ ext{TetEdges} : eal^6$ for a tetrahedron together with the associated Cayley-Menger matrix $ ext{TetCMData}$ whose determinant satisfies $288V^2 = igl| ext{CM}igr|$ for tetrahedron volume $V$.
background
The module introduces TetEdges as the six edge lengths of a tetrahedron and TetCMData as the 5x5 matrix whose entries are 0, 1, and squared distances. These objects support volume computation via the Cayley-Menger determinant and basic positivity checks. The setting is the piecewise-flat simplicial geometry used to formalize Regge deficits in the Recognition Science program. Downstream modules quote this data when constructing dihedral angles and Schläfli identities.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the Cayley-Menger structures required by SimplicialDeficitDischarge (Phase C5 toward the paper's Theorem 5.1 on the field-curvature identity), DeficitLinearization (Phase C4), DihedralAngle (Phase C2), and Schlaefli (Phase C3). These phases together discharge the ReggeDeficitLinearizationHypothesis on general simplicial complexes.
scope and limits
- Does not compute dihedral angles from the edge data.
- Does not perform deficit linearization.
- Does not treat simplices of dimension other than 3.
- Does not reference the phi-ladder or Recognition constants.