regularTriangleArea_pos
plain-language theorem explainer
For any positive edge length, the regular triangular hinge area (√3/4)a² is strictly positive. Cited by anyone wiring concrete Freudenthal/Regge area weights so hinges stay nondegenerate. Proof unfolds the closed form and multiplies elementary positivity of √3/4 and a².
Claim. If $a > 0$, then the regular triangular hinge area $\frac{\sqrt{3}}{4} a^{2}$ is strictly positive.
background
The module builds a concrete finite flat-sector Regge component that the weak-field bridge can consume without new geometric axioms. Hinge areas enter the coefficient matrix as geometric weights: off diagonal one wants $M_{ij} = -A_{ij}$, rows summing to zero, so the second-order action is a Dirichlet form with those weights.
The regular triangular hinge area is the elementary formula $(\sqrt{3}/4) a^{2}$ for an equilateral face of edge $a$. It is the area weight used by the regular local star and the concrete Regge-star comparison in this file. The Cayley-Menger stack already supplies regular tetrahedron data and dihedral angles; this module stays inside that regular model rather than arbitrary edge-length derivatives.
Positivity of the area for $a > 0$ is the strict companion of the nonnegativity fact for the same formula. Both keep the geometric weights on the correct side of zero when the edge length is a genuine positive scale.
proof idea
Term-mode after unfold regularTriangleArea. The goal is positivity of $(\sqrt{3}/4)\cdot a^{2}$. Apply real multiplication-positivity to the product of two factors: first $\sqrt{3}/4 > 0$, obtained from $\sqrt{3} > 0$ (via $\sqrt{\cdot}$ strict on $3 > 0$) and division by $4 > 0$; second $a^{2} > 0$, from squaring a positive real. No geometric lemmas beyond the definition.
why it matters
Closes a tiny but necessary positivity gate in the concrete Freudenthal-local Regge package. The module's honest scope is the regular flat-sector model whose area weights are exactly this formula and whose second variation is the graph-Laplacian Regge data already used by the weak-field bridge. Downstream siblings (areaWeight, regularLocalStar, derivative facts for uniform scale) need the area to be a positive scale factor so the Dirichlet form is nondegenerate on genuine edges.
No parent theorem currently lists this declaration in used_by; it is infrastructure for the component comparison itself. It does not touch the forcing chain (T0-T8), RCL, or the phi ladder; it is pure Euclidean hinge geometry feeding the Regge side of the gravity bridge. The open geometric gap remains full Cayley-Menger determinants and dihedral derivatives for arbitrary triangulations; this positivity fact is already settled inside the regular model that future derivative work must match.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.