genuine_component_dirichlet_reduction_from_final
plain-language theorem explainer
On any finite 3D Regge triangulation, a concrete component comparison (weak-field data whose bilinear coefficients match independent dual weights off-diagonal and obey the Schläfli row sum) makes the second-order Regge action of a vertex log-potential equal half the Dirichlet form of the edge-area weights. Discrete-gravity and continuum-bridge authors cite it once the geometric package is already built. The proof is a one-line packaging into the existing genuine-component Dirichlet reduction.
Claim. Let $K$ be a finite 3D Regge triangulation and $C$ a concrete component comparison on $K$: weak-field Regge data $W$, independent dual weights, off-diagonal match of bilinear coefficients to those dual weights, and the Schläfli row-sum identity. Then for every vertex log-potential $\varepsilon$, the second-order Regge action of $W$ at $\varepsilon$ equals $\tfrac12$ times the Dirichlet form of the edge-area weights of $W$ at $\varepsilon$.
background
Weak-field Regge calculus expands the discrete gravitational action to quadratic order in a conformal log-potential $\varepsilon_i=\ln\psi(\sigma_i)$ on triangulation vertices. The Dirichlet form is the standard weighted graph energy built from edge-area coefficients; equating the second-order Regge action to half that form is the discrete step toward continuum Laplace-type kinetics.
This module isolates the final geometric target. A concrete component comparison packages weak-field data, independent dual weights, the off-diagonal component match, and the Schläfli row sum. The module doc records that it "separates the independent dual-weight construction from the weak-field coefficient matrix and records the theorem that turns that geometric computation into ReggeComponentComparison."
Upstream, the genuine-component Dirichlet reduction already states that any genuine component package reduces via the weak-field conformal reduction once the Schläfli row sum is present. The present theorem only feeds a concrete comparison through that packaging map.
proof idea
One-line term proof. Lift the concrete comparison $C$ to a genuine component package by the packaging map genuineComponentPackage_of_concrete, then apply the upstream theorem genuine_component_dirichlet_reduction. That upstream result is itself the weak-field conformal reduction under the Schläfli row-sum hypothesis already stored in the package; no further algebraic work occurs here.
why it matters
Terminal citation point of the Regge component comparison stack: once dual weights and off-diagonal Hessian matches are built from incidence data (sibling constructions such as incidence dual weights and canonical weak-field data), this identity hands the second-order action to the Dirichlet form used in continuum matching. The abstract genuine-package reduction already existed; this theorem is the form gravity authors invoke after a fully concrete geometric computation on an arbitrary 3D triangulation.
In the Recognition Science gravity program it is the discrete side of the weak-field bridge: second-order Regge kinetics become a weighted graph Dirichlet energy, the natural precursor to continuum Laplace kinetics on the recognition ledger. No downstream consumers are wired yet, so it currently closes the ReggeComponentTheorem3DProof module rather than feeding a named parent theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.