IndisputableMonolith.Geometry.CayleyMenger
This module encodes tetrahedron edge lengths and supplies the Cayley-Menger determinant that recovers squared volume from those lengths. It is the base geometric layer cited by the four downstream modules that discharge the Regge deficit linearization hypothesis. The module consists of data definitions for edges and CM matrices together with volume identities and positivity lemmas for regular cases.
claimEdge-length data for a tetrahedron together with the Cayley-Menger 5-by-5 matrix whose determinant satisfies $288V^2 = (-1)^{5}2^{4-1}CM(l_{ij})$ where $V$ is the Euclidean volume.
background
The module belongs to the geometry layer that supports the Recognition Science program for piecewise-flat simplicial complexes. It introduces the six edge lengths of a tetrahedron and the associated Cayley-Menger matrix used to extract volume. These objects are required before dihedral angles or deficit linearizations can be defined.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
This module supplies the geometric primitives consumed by DihedralAngle (Phase C2), Schlaefli (Phase C3), DeficitLinearization (Phase C4), and SimplicialDeficitDischarge (Phase C5) in the program to prove the paper's Theorem 5.1 (field-curvature identity) as a Lean theorem.
scope and limits
- Does not compute dihedral angles or Regge deficits.
- Does not treat simplices of dimension other than three.
- Does not address non-Euclidean or curved metrics.
- Does not include numerical evaluation or approximation.