discreteBianchiContractedCert
plain-language theorem explainer
Canonical certificate packaging Track 1.C: on any finite bone set, every Schläfli-satisfying Regge triangulation obeys the contracted discrete Bianchi identity at every vertex; Schläfli and Bianchi are definitionally equivalent; and the Schläfli hypothesis space is nonempty. Gravity-track auditors cite it as the assembled master cert. Construction is pure field-wiring of three prior lemmas.
Claim. For vertex type $V$ and bone type $B$ with $B$ finite, there is a master certificate asserting: (i) for every Schläfli-satisfying Regge datum $R$ and every vertex $v\in V$, the contracted discrete Bianchi identity holds at $v$; (ii) at each vertex the contracted discrete Bianchi is definitionally equivalent to the Schläfli identity $\sum_{b\ni v}\varepsilon_b\,\partial A_b/\partial x_v=0$; (iii) the type of Schläfli-satisfying Regge data is inhabited (witnessed by the flat zero-deficit substrate).
background
Track 1.C of the quantum-gravity plan targets 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 the kinematic constraint making the action covariant under vertex moves. Module status is structural theorem (zero sorry, zero RS-internal axiom).
Abstract Regge data supply bones, deficit angles $\varepsilon_b$, and bone areas $A_b$. The Schläfli identity at a vertex $v$ is $\sum_{b\ni v}\varepsilon_b,\partial A_b/\partial x_v=0$. The contracted discrete Bianchi at a vertex is stated as a parallel named property. Schläfli-satisfying Regge data are those Regge data that obey Schläfli at every vertex.
Upstream, discreteBianchi_eq_schlafli records the definitional identification (Iff.rfl). discrete_bianchi_contracted_from_schlafli is the conditional Track 1.C theorem: any Schläfli-satisfying $R$ obeys contracted Bianchi at every $v$ by projecting the Schläfli field. SchlafliReggeData_inhabited witnesses nonemptiness via the flat zero-deficit substrate.
proof idea
One-line structure constructor. The three certificate fields are filled by existing results: discrete_bianchi_at_every_vertex is discrete_bianchi_contracted_from_schlafli (Schläfli hypothesis projects to contracted Bianchi at each vertex); schlafli_iff_bianchi is discreteBianchi_eq_schlafli (definitional equivalence); hypothesis_space_inhabited is SchlafliReggeData_inhabited V B (flat witness). No new algebra.
why it matters
Assembles the master cert for Track 1.C partial closure: contracted discrete Bianchi on every vertex of any Schläfli-satisfying Regge triangulation, plus structural equivalence and a nonempty hypothesis space. Downstream, discreteBianchiContractedCert_inhabited is the one-line Nonempty wrapper around this value, feeding the module's one-statement Track 1.C theorem block.
In the continuum the second Bianchi identity underwrites local conservation; here the discrete analog is identified with Schläfli, a pure simplicial kinematic identity. Full unconditional Schläfli (simplex volume-area calculus, vertex variations) remains multi-session Mathlib geometry work; this cert closes the structural layer and keeps the gravity track's kinematic constraint package inhabitable without axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.