Triangle
plain-language theorem explainer
Triangle supplies the 2-simplex data structure for Regge calculus on the RS lattice, recording three positive real edge lengths. Discrete gravity researchers cite it when constructing simplicial complexes to compute areas via Heron's formula and feed into deficit-angle derivations. The definition is a direct record of the three reals with their positivity witnesses; the accompanying area function is the standard square-root expression.
Claim. A triangle is a triple of positive real numbers $a,b,c>0$ that serve as the edge lengths of a 2-simplex.
background
The module formalizes exact Regge calculus for the RS discrete gravity programme on the lattice $Z^3×Z$. Curvature is concentrated on codimension-2 hinges and the Regge action is the sum of (area × deficit angle). Edge lengths are determined by the J-cost defect field. The Triangle structure is the basic 2-simplex primitive; sibling structures include Simplex4D (4-simplex) and HingeData (area plus deficit). Upstream results supply positivity of constants such as $c$ (Constants.c_pos) and structural facts on nuclear densities and ledger factorization that calibrate the underlying J-cost.
proof idea
The structure is introduced by declaring three real fields a, b, c together with the three positivity hypotheses. The area definition is the direct transcription of Heron's formula: $s=(a+b+c)/2$ followed by the square root of the product $s(s-a)(s-b)(s-c)$. The non-negativity theorem is the one-line application of Real.sqrt_nonneg to that expression.
why it matters
Triangle provides the geometric atom required by the full (non-linear) Regge machinery that replaces the linearized deficit-angle ansatz. It is used by defectDist_nonneg in CostAlgebra, by Jcost_zero_iff_one and Jmetric_exp_sinh in Cost, and by RecognitionDistance in RecogGeom. These feed the Regge action non-negativity and Gauss-Bonnet results listed in the module. The definition therefore sits at the interface between the J-cost ladder and the discrete curvature programme whose landmarks include the eight-tick octave and the three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.