concreteM_rowSum_zero
plain-language theorem explainer
On the eight-vertex Freudenthal local star, every row of the concrete second-variation coefficient matrix sums exactly to zero. Component-comparison and weak-field bridge work cite this as the discrete gauge/zero-mode identity for the flat-sector package. The proof unfolds the Laplacian Regge data and applies the general Laplacian row-sum lemma to the concrete area weights.
Claim. For every concrete local Regge star $S$ and every local vertex $i$ in the eight-vertex chart, $\sum_j M_{ij}(S)=0$, where $M(S)$ is the second-variation coefficient matrix of the weak-field Laplacian Regge data built from the geometric area/face weights of $S$.
background
This module supplies a fully concrete finite flat-sector Regge package that the weak-field bridge can consume without new geometric axioms. The local chart has eight vertices (a cubic cell / Freudenthal star). A concrete star carries background edge length and hinge area scales; the area-weight matrix is zero on the diagonal and equal to the background hinge area off diagonal, and is symmetric.
The second-variation matrix is not an arbitrary Cayley-Menger Hessian. It is the bilinear coefficient matrix of the graph-Laplacian Regge data induced by those area weights: off diagonal one has $M_{ij}=-A_{ij}$, and the quadratic form is the corresponding Dirichlet energy. The module doc is explicit that full differentiable Cayley-Menger determinants and arbitrary-triangulation dihedral derivatives are not yet in the stack; only this regular flat-sector model is closed.
Upstream, the Laplacian coefficient row-sum identity already guarantees that any such Laplacian Regge matrix has vanishing row sums once the weight matrix is symmetric. This theorem specializes that fact to the concrete star.
proof idea
Introduce the row index $i$. Unfold the concrete coefficient matrix and the concrete weak-field Regge data, which are defined as the bilinear coefficients of Laplacian Regge data on the area-weight matrix. Rewrite via the identification of bilinear coefficients with Laplacian coefficients for that data, then apply the general Laplacian row-sum lemma at the concrete area weights and index $i$. Symmetry of the area weights is passed in so the Laplacian package applies. No separate finite-sum arithmetic is needed.
why it matters
Zero row sums are one of the three algebraic identities the concrete component comparison must hit: off-diagonal $M_{ij}=-A_{ij}$, every row sums to zero, and the second-order action equals the Dirichlet form with those geometric weights. Downstream, the Freudenthal Regge component certificate packages this theorem as its row_sum field alongside the area and dihedral derivative facts and the Dirichlet identification.
In the Recognition geometry stack this is the discrete zero-mode / constant-shift invariance of the flat-sector second variation: adding a constant to the conformal factor does not change the quadratic form. That matches the weak-field conformal Regge interface the bridge already uses. It does not yet force $D=3$ or the eight-tick octave by itself; those live in the forcing chain. It does close the first fully concrete finite model that a future full Cayley-Menger derivative computation must match.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.