SchlafliReggeData
plain-language theorem explainer
Packages a Regge triangulation together with the Schläfli identity at every vertex: the named structural hypothesis of Track 1.C. Anyone citing the conditional discrete Bianchi theorems works relative to this type. It is a pure structure extension of abstract Regge data by one universal vertex constraint; no proof content.
Claim. A Schläfli–Regge datum on vertex set $V$ and bone set $B$ (with $B$ finite) is an abstract Regge triangulation $(x_v,\iota,\varepsilon_b,A_b,\partial A_b/\partial x_v)$ such that for every vertex $v\in V$ the Schläfli identity holds: $\sum_{b\in B}\varepsilon_b\,\partial A_b/\partial x_v^{(i)}=0$ for each spatial component $i=0,1,2,3$.
background
Track 1.C of the quantum-gravity master plan asks for the contracted discrete Bianchi identity on a Regge substrate: the discrete stand-in for $\nabla_\mu G^{\mu\nu}=0$. In Regge calculus that identity is kinematic and coincides with the classical Schläfli identity at each interior vertex, $\sum_{b\ni v}\varepsilon_b,\partial A_b/\partial x_v=0$, where $\varepsilon_b$ is the deficit angle (holonomy around bone $b$) and $\partial A_b/\partial x_v$ is the bone-area gradient with respect to the position of an incident vertex.
ReggeData supplies the abstract fields: vertex positions in $\mathbb{R}^4$, incidence, deficit angles, bone areas, and the vertex-area gradients. SchlafliIdentityAtVertex R v is the componentwise vanishing of the deficit-weighted sum of those gradients at $v$. The full geometric proof that every physical triangulation obeys Schläfli is multi-session Mathlib work; this module therefore isolates the identity as a named hypothesis and proves everything else relative to it.
proof idea
No proof: this is a structure definition. It extends ReggeData V B by a single field schlafli asserting SchlafliIdentityAtVertex at every vertex. Downstream theorems read that field directly (e.g. discrete_bianchi_contracted_from_schlafli is the one-line application R.schlafli v).
why it matters
This is the carrier type for Track 1.C's structural half-closure. The parent theorem discrete_bianchi_contracted_from_schlafli states that every inhabitant satisfies the contracted discrete Bianchi at every vertex; the master cert DiscreteBianchiContractedCert and the one-statement form discrete_bianchi_contracted_one_statement quantify over it. Gravity-side interfaces (PhysicalReggeEHBianchiInterface, physicalSchlafliBianchiMasterProp, discrete_bianchi_structural_prop) import the same hypothesis so continuum residuals can sit on a proved kinematic constraint.
The module already supplies a non-vacuous witness (flatSchlafliReggeData: all deficits zero) and an inhabitedness theorem, so the hypothesis space is not empty. What remains open is the unconditional Schläfli identity for genuine curved triangulations; until that lands, every Bianchi claim stays conditional on this structure. Framework role: kinematic covariance of the Regge action under vertex variations, the discrete analog of diffeomorphism invariance behind Einstein's equations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.