regularTriangleArea
plain-language theorem explainer
The classical equilateral-triangle area $A(a)=(\sqrt{3}/4)a^2$ is packaged as the hinge-area weight for the concrete Freudenthal-local Regge star. Anyone wiring the weak-field second-variation comparison to geometric Dirichlet weights cites this formula. It is a one-line definition of the elementary area expression, not a derived identity.
Claim. For real edge length $a$, the regular triangular hinge area is $A(a)=\frac{\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. Full Cayley-Menger determinants and arbitrary dihedral derivatives are not yet exposed as differentiable maps of all edge lengths, so the comparison is proved only for a regular flat-sector / Freudenthal-local model.
In that model, hinge areas enter as the geometric weights of the second-order Regge action. Off diagonal the coefficient matrix is minus those areas, rows sum to zero, and the action reduces to a Dirichlet form. The present definition supplies the regular equilateral hinge area that feeds those weights.
Sibling positivity lemmas and a derivative lemma treat this same formula; the local star constructor installs it as the background hinge area at scale $a>0$.
proof idea
Pure definition: the function is declared equal to $(\sqrt{3}/4),a^2$. No lemmas are applied. Downstream proofs unfold this abbreviation and then use elementary real arithmetic (nonnegativity of squares and square roots, product rule for the derivative).
why it matters
This is the geometric input that makes the concrete Regge star honest: regularLocalStar sets the background hinge area to this value, and the certificate structure records that the area map is derivative-ready with slope $(\sqrt{3}/2)a$. The parent comparison theorem then identifies the second-order Regge action with one-half the Dirichlet form built from the induced area weights.
Within Recognition Science geometry, the declaration is scaffolding for the weak-field conformal Regge bridge rather than a forcing-chain step (T0-T8). It closes the first fully concrete finite model the bridge can target; a future full Cayley-Menger derivative stack must reproduce the same interface for non-regular triangulations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.