SchlaefliRowSum
plain-language theorem explainer
The Schläfli row-sum property requires that the bilinear coefficient matrix built from first-order area and deficit responses has vanishing row sums at every vertex. Discrete-gravity researchers cite it when confirming that uniform conformal shifts on a flat background induce no net curvature change. The definition directly encodes the algebraic content of Schläfli's identity applied to the linearized Regge data.
Claim. For weak-field Regge data $W$ on $n$ vertices, whose fields are the symmetric first-order responses $dA_{ij}$ and $dδ_{ij}$, the row-sum condition is $∀ i, ∑_j dA_{ij} · dδ_{ij} = 0$.
background
The module develops the finite-dimensional algebra that reduces the Regge action under a conformal edge-length ansatz to a discrete Dirichlet form. WeakFieldReggeData packages the linear responses of hinge areas and deficit angles together with their symmetry axioms; the induced bilinear coefficient is the pointwise product of these responses. The local setting is the three-layer decomposition: conformal Taylor expansion of edge lengths, graph-Laplacian identity for zero-row-sum matrices, and the geometric hypothesis that flat backgrounds obey the Schläfli row-sum condition.
proof idea
The definition is a one-line wrapper that states the universal quantification over vertices of the row sum of the bilinear coefficient matrix equaling zero.
why it matters
SchlaefliRowSum supplies the central hypothesis for the main reduction theorems weak_field_conformal_reduction and weak_field_conformal_reduction_kappa, which convert the second-order Regge action into half the Laplacian action on the edge-area graph. It encodes the geometric input that uniform conformal modes produce no curvature change, thereby closing the algebraic step from the linearized Regge bilinear form to the Dirichlet energy that appears in the discrete gravity sector of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.