discrete_bianchi_contracted_one_statement
plain-language theorem explainer
Packages Track 1.C of the quantum-gravity master plan into one structural statement: every Schläfli-satisfying Regge triangulation obeys the contracted discrete Bianchi identity at every vertex; that identity is definitionally equivalent to the Schläfli identity on arbitrary Regge data; and a Schläfli-satisfying witness exists. Cite it when quoting the one-statement form of discrete Bianchi on the Regge substrate. Proof is a three-component term assembling prior lemmas.
Claim. For vertex type $V$ and finite bone type $B$: (i) every Regge triangulation satisfying the Schläfli identity at all vertices obeys the contracted discrete Bianchi identity at every vertex; (ii) for arbitrary Regge data $R$ and vertex $v$, contracted discrete Bianchi at $v$ holds if and only if the Schläfli identity holds at $v$; (iii) the type of Schläfli-satisfying Regge data on $(V,B)$ is nonempty.
background
Track 1.C of the quantum-gravity master plan asks for the contracted discrete Bianchi identity on a Regge substrate: the discrete analog of $\nabla_\mu G^{\mu\nu}=0$. In Regge calculus that kinematic constraint is the Schläfli identity at each interior vertex $v$,
$$\sum_{b\ni v}\varepsilon_b,\partial A_b/\partial x_v=0,$$
with $\varepsilon_b$ the deficit angle and $A_b$ the bone area.
ReggeData packages abstract triangulation data (vertex positions in $\mathbb{R}^4$, incidence, deficit angles, bone areas, and vertex-area gradients). SchlafliIdentityAtVertex R v asserts the componentwise vanishing of the deficit-weighted area-gradient sum over bones. DiscreteBianchiContractedAtVertex is defined to be that same proposition, so the two names are definitionally identified. SchlafliReggeData is Regge data carrying a proof that Schläfli holds at every vertex: the named structural hypothesis of Track 1.C.
The module is a structural scaffold (0 sorry, 0 RS-internal axiom). Full unconditional Schläfli from simplex geometry remains multi-session Mathlib work; here the identity is the hypothesis, and Bianchi is recovered from it.
proof idea
Term-mode triple, no tactics. The three conjuncts are discharged by three prior results in order:
discrete_bianchi_contracted_from_schlafli: on anySchlafliReggeData, the structure fieldschlaflisuppliesDiscreteBianchiContractedAtVertexat each vertex (one-line projection).discreteBianchi_eq_schlafli:Iff.rfl, because contracted Bianchi is defined as the Schläfli identity.SchlafliReggeData_inhabited: nonemptiness via the canonical flat (zero-deficit) witness, which satisfies Schläfli trivially.
The whole theorem is therefore a packaging wrapper, not a new geometric argument.
why it matters
This is the TRACK 1.C ONE-STATEMENT structural form named in the doc-comment: the master-plan clause discrete_bianchi_contracted packaged as a single conjunction. Downstream consumers of Track 1.C can cite one declaration instead of three siblings.
In the Recognition gravity program, discrete Bianchi is the kinematic reason the Regge action is covariant under vertex variations, matching continuum $\nabla_\mu G^{\mu\nu}=0$. Closing the structural half of Track 1.C separates what is definitional/Regge-calculus folklore (equivalence and conditional implication) from the open geometric half (unconditional Schläfli from simplex volume-area calculus).
No used_by edges yet; the declaration is a terminal packaging point for the structural scaffold closed 2026-05-22. It does not touch T0–T8 forcing, RCL, or the phi-ladder; those live elsewhere. The remaining open path is the unconditional Schläfli proof that would discharge the SchlafliReggeData hypothesis in physical triangulations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.