FreudenthalReggeComponentCert
plain-language theorem explainer
Certificate structure packaging five identities that close the weak-field Regge component comparison on the concrete Freudenthal-local flat sector (eight vertices). Anyone citing the equality of second-order Regge action with the geometric Dirichlet form on regular hinge areas uses this bundle. It is a pure interface definition; the single inhabitant is assembled by plugging in the already-proved derivative and matrix lemmas.
Claim. A certificate asserting: (1) the regular triangular hinge area $A(a)=(\sqrt{3}/4)a^{2}$ satisfies $\mathrm{d}A/\mathrm{d}a=(\sqrt{3}/2)a$; (2) the regular tetrahedral dihedral angle is invariant under uniform edge scaling (derivative zero); (3) for every concrete local Regge star $S$ and distinct local vertices $i,j$, the second-variation matrix obeys $M_{ij}=-A_{ij}$ with $A$ the geometric area-weight matrix; (4) every row of $M$ sums to zero; (5) the second-order Regge action on the induced weak-field data equals $\tfrac12$ times the Dirichlet form of those area weights on any eight-vertex log-potential.
background
The module supplies a fully concrete finite model for the weak-field Regge bridge, restricted to a regular flat-sector / Freudenthal-local chart. The local vertex type is eight points (Fin 8), matching a cubic cell. A concrete Regge star carries only two background scales: a positive edge length and a nonnegative hinge area.
Area weights are the constant off-diagonal matrix with value equal to that hinge area (diagonal zero). The weak-field Regge data are the graph-Laplacian package built from those weights, and the coefficient matrix $M$ is the associated bilinear form. Log-potentials are maps from the eight vertices to reals, the same objects used by the continuum Laplacian action.
Honest scope from the module: the Cayley-Menger stack already knows regular tetrahedron data, but does not yet expose full differentiable CM determinants or arbitrary dihedral derivatives. This certificate therefore targets only the regular hinge-area / Laplacian model the bridge can consume without new geometric axioms.
proof idea
No proof body: this is a structure whose five fields are propositions. An inhabitant is obtained by assigning already-proved lemmas to each field (area derivative of the regular triangle formula, vanishing derivative of the scale-invariant regular dihedral angle, off-diagonal identification $M=-A$, row-sum vanishing, and the second-variation/Dirichlet equality). The last field is the one-line wrapper that rewrites via the concrete component-comparison hypothesis into the geometric Dirichlet form.
why it matters
This is the exact interface the weak-field bridge needs for a finite flat-sector coefficient package. Downstream, freudenthalReggeComponentCert is the unique theorem that fills every field, thereby discharging the concrete closure stated in the module: second-order Regge action equals half the geometric Dirichlet form on regular area weights.
In the Recognition geometry stack it is the first fully concrete finite model a future full Cayley-Menger / dihedral-derivative computation must match. It does not itself invoke the forcing chain (T0–T8) or the Recognition Composition Law; it sits on the gravity/geometry side that feeds continuum and weak-field comparisons once those foundations are in place. The open question it frames is the upgrade from regular Freudenthal-local data to arbitrary Regge triangulations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.