canonicalWeakFieldData_rowSum
plain-language theorem explainer
For any incidence-consistent 3D Regge triangulation, the canonical weak-field data built from incidence dual weights satisfies the Schläfli row-sum identity. Discrete-gravity and Regge-calculus workers cite it when packaging dual weights into the weak-field coefficient matrix for component comparison. The proof is a one-line instantiation of the general Laplacian-Regge row-sum lemma on the canonical dual weight and its symmetry.
Claim. For every finite 3D Regge triangulation $K$ that is incidence-consistent, the canonical weak-field data constructed from the incidence dual weights of $K$ satisfies the Schläfli row-sum condition.
background
A 3D Regge triangulation here is a finite abstract complex (vertices, edges, tetrahedra) with nondegenerate squared-edge data on each tetrahedron. Incidence consistency strengthens the scaffold: local tetrahedral edge slots match global edge endpoints (up to orientation), and a local closed-form Schläfli identity is available so global Schläfli need not be supplied by the caller.
The canonical dual weight on a vertex pair is the sum, over edges, of the incidence-defined edge-pair weights; it is symmetric. Canonical weak-field data packages those weights into the coefficient matrix of the weak-field conformal Regge expansion. Schläfli row-sum is the discrete variational consistency condition on that matrix (each row sums as required by the discrete Schläfli identity).
This module separates the independent dual-weight construction from the weak-field matrix and records the theorems that turn the geometric computation into a Regge component comparison.
proof idea
Term-mode one-liner. Instantiate the general lemma that any Laplacian-style Regge data built from a symmetric dual weight satisfies Schläfli row-sum, feeding it the canonical dual weight of $K$ and the theorem that this weight is symmetric in its two vertex arguments. No further algebraic work is done here.
why it matters
Downstream, the concrete component comparison built from canonical incidence weights takes its weak-field data to be exactly this canonical package; the present theorem discharges the row-sum obligation on that data (the sibling off-diagonal match theorem handles the remaining coefficient identity). Together they turn the geometric dual-weight computation into a full ReggeComponentComparison.
In the Recognition Science gravity stack this sits inside the 3D Regge component theorem, the discrete-geometry bridge that connects the forced eight-tick octave and $D=3$ (forcing steps T7–T8) to a concrete weak-field coefficient comparison. Without row-sum, the discrete action would fail first-order variational consistency.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.