SchlaefliRowSum
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not compute explicit values of dArea or dDeficit from Cayley-Menger or dihedral formulas.
- Does not verify the row-sum condition for any concrete lattice geometry.
- Does not address non-conformal or higher-order perturbations.
formal statement (Lean)
311def SchlaefliRowSum {n : ℕ} (W : WeakFieldReggeData n) : Prop :=
proof body
Definition body.
312 ∀ i : Fin n, ∑ j : Fin n, bilinearCoefficient W i j = 0
313
314/-- The second-order Regge action functional in the conformal mode.
315 Plugging the conformal expansion of `ℓ²` into the linearized Regge
316 action and collecting the order-`ξ²` terms gives this bilinear:
317
318 S^(2)[ξ] = (1/4) · Σ_{i,j} (ξ_i + ξ_j)² · M_{ij}
319 = (1/4) · Σ_{i,j} (ξ_i² + 2 ξ_i ξ_j + ξ_j²) · M_{ij}.
320
321 The factor `1/4` comes from the `(ξ_i + ξ_j)/2` factors entering
322 twice (once from `A_h^(1)`, once from `δ_h^(1)`).
323
324 With the Schläfli row-sum property, the `ξ_i² + ξ_j²` parts
325 vanish on summation and the `2 ξ_i ξ_j` part rearranges via §2 into
326 the Dirichlet form on differences. -/