regularTriangleArea_nonneg
plain-language theorem explainer
For every real edge length a, the regular triangular hinge area (√3/4) a² is nonnegative. Anyone assembling a ConcreteReggeStar or checking area weights in the Freudenthal-local Regge model cites this. The proof unfolds the area formula and multiplies two elementary nonnegativity facts: √3/4 ≥ 0 and a² ≥ 0.
Claim. For every real number $a$, the regular triangular hinge area satisfies $0 \le (\sqrt{3}/4)\, a^2$.
background
The module builds a concrete finite flat-sector Regge component that the weak-field bridge can consume without new geometric axioms. It works with a regular Freudenthal-local model: hinge areas come from the regular triangle formula, and second-variation data is the graph-Laplacian Regge package already used downstream.
The hinge-area weight is defined by regularTriangleArea a := (√3 / 4) a², the classical area of an equilateral triangle of side a. Nonnegativity of that weight is part of the ConcreteReggeStar interface (hinge areas must be ≥ 0), so this lemma is the first arithmetic check before the local star can be assembled.
The broader Cayley–Menger stack already supplies regular tetrahedron CM values and dihedral data, but not yet full differentiable CM determinants for arbitrary edge lengths. This module therefore targets only the regular flat-sector case.
proof idea
Term-mode proof after unfolding the definition. The expression is a product of √3/4 and a². Apply mul_nonneg: the first factor is nonnegative because √3 ≥ 0 and the constant 4 is positive (div_nonneg + Real.sqrt_nonneg + norm_num); the second factor is nonnegative by sq_nonneg a. No geometry beyond the algebraic formula is used.
why it matters
Feeds directly into regularLocalStar, which packages the concrete local star at scale a: edge length a > 0 and hinge area equal to the regular triangle area, with nonnegativity discharged by this theorem. That star is the geometric input for the component comparison (off-diagonal M_ij = −A_ij, row sums zero, Dirichlet form with concrete weights) that the weak-field conformal Regge bridge consumes.
In the Recognition geometry stack this is scaffolding closure for the first fully concrete finite model, not a claim about arbitrary Regge triangulations. It sits under the honest-scope note that full Cayley–Menger derivative formulas remain future work; the interface this lemma helps fill is exactly what those derivatives must match.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.