genuine_component_dirichlet_reduction
plain-language theorem explainer
For any genuine 3D Regge component package on a triangulation, the second-order weak-field Regge action of a vertex log-potential equals half the Dirichlet form built from the package edge areas. Discrete-gravity workers cite this to pass from Cayley-Menger/Hessian geometry into the conformal Laplacian energy already proved for weak-field Regge data. The proof is a one-line application of the existing weak-field conformal reduction, feeding it the package data and its bundled Schläfli row-sum.
Claim. Let $K$ be a 3D triangulation and let $P$ be a genuine geometric component package on $K$: weak-field Regge data $W$ whose off-diagonal bilinear coefficients match a symmetric nonnegative geometric area matrix, together with a Schläfli row-sum condition on $W$. Then for every log-potential $\varepsilon$ on the vertices of $K$, the second-order Regge action of $W$ at $\varepsilon$ equals $\tfrac12$ times the Dirichlet form of the edge-area weights of $W$ evaluated on $\varepsilon$.
background
In the RS gravity stack, 3D Regge calculus is linked to a weak-field conformal ansatz on edge lengths. A log-potential $\varepsilon$ is a vertex assignment $\varepsilon_i=\ln\psi(\sigma_i)$; the canonical conformal edge lengths are $L_{ij}\propto\exp((\varepsilon_i+\varepsilon_j)/2)$, reducing to the background scale when $\varepsilon\equiv 0$.
This module is the bridge from a geometrically computed package (Cayley-Menger volumes, dihedral angles, Hessian) to the already-proved weak-field conformal Regge reduction. The package bundles weak-field Regge data $W$, a symmetric nonnegative geometric area matrix that matches the off-diagonal bilinear coefficients of $W$, and a Schläfli row-sum witness on $W$.
The upstream reduction states that, once the Schläfli row-sum holds, the quadratic Regge action collapses exactly to half the graph Dirichlet form with those edge-area weights. The present theorem simply specializes that identity to packages produced by the genuine 3D Hessian computation.
proof idea
One-line term proof. Apply the existing weak-field conformal reduction lemma to the package's weak-field data $W$ and its bundled Schläfli row-sum witness, at the given log-potential $\varepsilon$. No new algebra: the package interface already supplies exactly the hypotheses that lemma requires (data plus row-sum), so the equality is inherited verbatim.
why it matters
This is the hinge that turns a geometrically computed 3D Hessian package into the Dirichlet-form identity already available in the weak-field conformal bridge. The module doc states the goal explicitly: supply a genuine component package, instantiate the existing comparison interface, and inherit the Dirichlet reduction proved in the weak-field conformal Regge file.
Downstream, once a concrete component comparison is built, the companion theorem applies this result after converting the concrete package into a genuine one, so the final 3D Regge component theorem inherits the reduction immediately ("the existing Dirichlet reduction applies immediately").
In the broader RS gravity story it links discrete curvature (Regge) to continuum Laplacian energy in the weak-field limit of the recognition ledger. It does not itself derive Newton's $G$ or the continuum Einstein equations; it closes the discrete quadratic-action step on which those continuum claims rest.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.