Tetrahedron
plain-language theorem explainer
A structure records a tetrahedron as six positive real edge lengths between vertices labeled 0-3. Discrete gravity workers cite it when instantiating the simplicial complex for exact Regge calculus on the RS lattice. The definition is a plain record type that bundles the six lengths with their positivity constraints.
Claim. A tetrahedron is a 3-simplex specified by six positive real numbers $l_{01},l_{02},l_{03},l_{12},l_{13},l_{23}$ that give the lengths of the edges connecting four vertices labeled 0,1,2,3.
background
The module supplies the exact nonlinear Regge calculus layer for the Recognition Science discrete gravity programme. It replaces the linearized deficit-angle ansatz with the full Regge action $S=∑_h A_h δ_h$, where curvature is concentrated on codimension-2 hinges of a piecewise-flat simplicial complex. Edge lengths on the underlying $ℤ^3×ℤ$ lattice are taken from the J-cost defect field.
proof idea
The declaration is a direct structure definition. It introduces six real fields for the edge lengths together with six positivity hypotheses; no lemmas or tactics are invoked.
why it matters
The structure supplies the elementary 3-simplex needed to construct the simplicial complex on which the Regge action and deficit-angle calculations rest. It supports the module's replacement of Assumption A2 by the full Regge machinery and appears in the chain leading to regge_action_nonneg_flat and regge_action_gauss_bonnet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.