TetEdges
plain-language theorem explainer
TetEdges records six positive real numbers as the edge lengths of a tetrahedron. Workers on piecewise-flat geometry and Regge calculus cite this record when supplying input to Cayley-Menger volume formulas. The definition is a direct structure with an embedded positivity axiom and a derived squared-length accessor proved positive by the power rule.
Claim. A tetrahedron edge-length datum is a map $e : {0,1,2,3,4,5} → ℝ$ such that $e(i) > 0$ for all $i$, together with the derived squared lengths $e(i)^2$.
background
The module defines Cayley-Menger data for 3-simplices as the first step toward discharging ReggeDeficitLinearizationHypothesis. TetEdges supplies the six edge lengths with a strict positivity condition; downstream objects such as TetCMData and TetVolumeIdentity consume this record to state the classical determinant identity 288 V² = CM(T). The module avoids full matrix lifts and records volume relations as named hypotheses rather than reproving classical geometry.
proof idea
The structure is introduced by direct record declaration. The accessor sq is the pointwise square of len. Positivity of sq follows by applying pow_pos to the supplied len_pos hypothesis.
why it matters
TetEdges is the base input type for TetCMData, RegularTet.toTetEdges, TetCMPositivity, and the volume identity theorems. It anchors Phase C1 of the simplicial geometry chain that feeds DihedralAngle and SimplicialDeficitDischarge. The construction respects the three-dimensional setting (T8) and supplies the edge data required for the Recognition Composition Law applications in later modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.