regularLocalStar
plain-language theorem explainer
Packages a positive edge scale a into a concrete local Regge star whose hinge weight is the regular triangular area (√3/4)a². Cited by anyone building the flat-sector Freudenthal model or the weak-field Regge bridge coefficient matrix. The body is a structure instance: edge length a, positivity from the hypothesis, hinge area and its nonnegativity from the regular-triangle lemmas.
Claim. For every real $a>0$, there is a concrete local Regge star with background edge length $a$ and hinge-area weight equal to the regular triangular area $(\sqrt{3}/4)a^{2}$.
background
The module builds a fully 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, so the comparison is proved only for a regular Freudenthal-local model: off-diagonal coefficients $M_{ij}=-A_{ij}$, rows sum to zero, and the second-order action is the Dirichlet form with those geometric weights.
A concrete local Regge star records the flat background scales needed for that bookkeeping: a positive edge length and a nonnegative hinge area. The regular triangular hinge area is $(\sqrt{3}/4)a^{2}$; its nonnegativity is already proved for every real $a$. This constructor simply installs those two scales into the star structure at a chosen positive edge length.
proof idea
Definitional structure instance, not a tactic proof. Set the background edge length to $a$ and discharge positivity by the given hypothesis $a>0$. Set the hinge area to regularTriangleArea a (i.e. $(\sqrt{3}/4)a^{2}$) and discharge nonnegativity by applying regularTriangleArea_nonneg.
why it matters
Supplies the canonical regular local star that the concrete flat-sector / Freudenthal Regge component comparison is written against. Downstream area-weight and second-variation identities in this module are meant to run on stars of this shape: hinge weights from the regular triangle formula, edge scale positive and fixed. It is the exact finite geometric interface a future full Cayley–Menger derivative computation must match if the bridge is to leave the regular model. No used-by edges are recorded yet; the declaration is infrastructure for the component package rather than a cited theorem in the forcing chain (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.