flatReggeData_schlafli
plain-language theorem explainer
Flat Regge data (identically zero deficit angles) satisfies the Schläfli identity at every vertex. Anyone packaging a canonical flat witness for Track 1.C discrete Bianchi cites this. The argument is a one-line simplification: zero deficits make every summand vanish, so the finite sum is zero.
Claim. For types $V,B$ with $B$ finite, and for every vertex $v\in V$, the flat Regge data on $(V,B)$ satisfies the Schläfli identity at $v$: for each coordinate index $i\in\{0,1,2,3\}$, $\sum_{b\in B}\varepsilon_b\,\partial A_b/\partial x_v^{(i)}=0$, where every deficit angle $\varepsilon_b$ is zero by construction of the flat data.
background
This module is Gravity Track 1.C: the contracted discrete Bianchi identity on a Regge substrate, closed as a structural theorem (0 sorry). In Regge calculus the continuum constraint $\nabla_\mu G^{\mu\nu}=0$ becomes, at each interior vertex $v$, the Schläfli identity
$\sum_{b\ni v}\varepsilon_b,\partial A_b/\partial x_v=0$,
with $\varepsilon_b$ the deficit at bone $b$ and $A_b$ its area. That identity is the kinematic condition making the Regge action covariant under vertex variations.
Abstract Regge data packages vertex positions, incidence, deficit angles, bone areas, and vertex-area gradients. The named property Schläfli-at-vertex asserts the sum above vanishes componentwise on $\mathrm{Fin},4$. Flat Regge data is the trivial witness: zero deficits, zero areas, zero positions, and universal incidence. Its doc states the identity holds vacuously because the sum of zero times anything is zero.
proof idea
Introduce the vertex $v$ and the coordinate index $i:\mathrm{Fin},4$. Unfold the definition of flat Regge data. Every deficit angle is the constant zero function, so each product $\varepsilon_b\cdot(\partial A_b/\partial x_v^{(i)})$ is zero and the finite sum over bones collapses to $0$. No external lemmas are required beyond definitional simplification.
why it matters
This theorem is the proof field of the packaged witness flatSchlafliReggeData, whose doc calls it "a Schläfli-satisfying Regge triangulation (non-vacuous witness)." That witness shows the type of Schläfli-satisfying Regge data is inhabited, so the structural scaffold for Track 1.C is not empty.
In the quantum-gravity master plan, Track 1.C equates the contracted discrete Bianchi with Schläfli at the structural level. The flat case is the base witness before nontrivial curved data is built. It does not yet discharge the full simplex-geometry proof of Schläfli from volume-area calculus; it closes the zero-deficit corner that the module explicitly promises.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.