DiscreteBianchiContractedAtVertex
plain-language theorem explainer
The contracted discrete Bianchi identity at a triangulation vertex is defined to be the Schläfli identity at that vertex. Anyone citing Track 1.C of the quantum-gravity plan, or the Regge kinematic constraint ∇_μ G^{μν}=0 in discrete form, uses this name. The body is a pure definitional alias: no proof obligations beyond the Schläfli sum.
Claim. For abstract Regge data $R$ on vertex set $V$ and bone set $B$, and for any vertex $v\in V$, the contracted discrete Bianchi identity at $v$ is the proposition that the Schläfli identity holds at $v$: for every coordinate direction $i\in\{0,1,2,3\}$, $\sum_{b\in B}\varepsilon_b\,\partial A_b/\partial x_v^{i}=0$, where $\varepsilon_b$ is the deficit angle and $A_b$ the bone area.
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 continuum GR that identity is the kinematic reason the Einstein–Hilbert action is diffeomorphism-covariant; in Regge calculus the same role is played by covariance of the Regge action under vertex variations.
Abstract Regge data package vertex positions in $\mathbb{R}^4$, an incidence relation between bones and vertices, deficit angles (holonomies around bones), bone areas, and the vertex-area gradients $\partial A_b/\partial x_v$. The Schläfli identity at $v$ asserts that the deficit-weighted sum of those gradients vanishes componentwise. Classical Regge calculus identifies that sum with the contracted Bianchi constraint at the vertex.
This module therefore separates the geometric content (Schläfli) from the GR name (contracted Bianchi) and equates them at the structural level, leaving a full unconditional Schläfli proof as later Mathlib geometry work.
proof idea
Definitional alias, not a derived theorem. The body is exactly the Schläfli-at-vertex proposition: the four-component vanishing of $\sum_b \varepsilon_b,\partial A_b/\partial x_v$. No tactics, no lemmas. The companion equivalence theorem is then Iff.rfl, confirming the two names are definitionally the same proposition.
why it matters
Gives the GR-facing name used throughout Track 1.C. Downstream, the structural theorem that every Schläfli-satisfying Regge triangulation obeys contracted Bianchi at every vertex is a one-line appeal to this alias; the master certificate and the one-statement Track 1.C theorem package that fact together with the definitional equivalence. Gravity Track 1.B/C residual interfaces import the same name so physical finite-probe residuals can sit next to the kinematic Bianchi clause without re-stating Schläfli sums.
In the Recognition framework this is the discrete kinematic half of making a Regge action covariant under vertex moves, parallel to how continuum Bianchi protects diffeomorphism invariance. It does not yet force $D=3$ or the eight-tick octave; those live in the Unified Forcing Chain. The remaining open piece is an unconditional geometric proof of Schläfli on general simplicial complexes; until then results stay conditional on Schläfli-satisfying data (with the flat zero-deficit witness already inhabited).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.