areaWeight
plain-language theorem explainer
Defines the concrete geometric area/face-weight matrix on an eight-vertex Freudenthal-local Regge star: diagonal entries vanish, off-diagonal entries equal the star's regular hinge area. Anyone comparing weak-field Regge second variation to a Dirichlet form cites this weight. The body is a one-line piecewise definition from the star's hinge-area scale.
Claim. Given a concrete local Regge star $S$ (background edge length and nonnegative hinge area) and vertices $i,j$ in the eight-vertex local chart, the area weight is $A_S(i,j) = 0$ if $i=j$, and $A_S(i,j) = A_0(S)$ (the regular hinge area of $S$) otherwise.
background
This module builds a fully concrete finite flat-sector Regge model that the weak-field bridge can consume without new geometric axioms. The Cayley–Menger stack supplies regular tetrahedron data and dihedral angles, but not yet full differentiable CM determinants or arbitrary-triangulation dihedral derivatives. The workaround is a regular Freudenthal-local star whose second-variation data is ordinary graph-Laplacian Regge data.
A ConcreteReggeStar packages a positive background edge length and a nonnegative hinge area $A_0$. Vertices run over an eight-point local chart (cubic cell / Freudenthal chart). The area weight matrix is the geometric face-weight input to the Dirichlet energy: diagonal terms drop out of the quadratic form; off-diagonal terms carry the regular hinge area.
proof idea
Pure definition, not a proof. On equal vertices return $0$; otherwise return the star's stored regular hinge area $A_0$. No lemmas are applied. Downstream nonnegativity and symmetry proofs simply unfold this case split and use $A_0 \ge 0$ from the star structure.
why it matters
This weight is the geometric input that closes the concrete component comparison. Downstream, off-diagonal coefficients satisfy $M_{ij} = -A_{ij}$, every row of $M$ sums to zero, and the second-order Regge action equals $\tfrac12$ times the Dirichlet form built from these weights. Those facts assemble into the concrete ReggeComponentComparison object and the equality of second variation with the geometric Dirichlet form, which the weak-field bridge consumes.
It is deliberately not a general Cayley–Menger / dihedral-derivative construction. It is the first fully concrete finite model and the exact interface a future full derivative computation must match. In the broader RS geometry stack it supplies the finite-chart area data that lets the flat-sector Regge package talk to the conformal weak-field bridge without extra axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.