DiscreteBianchiContractedCert
plain-language theorem explainer
Master certificate for Gravity Track 1.C: under the Schläfli hypothesis on abstract Regge data, the contracted discrete Bianchi identity holds at every vertex; Schläfli and contracted Bianchi are definitionally equivalent; and the hypothesis space is inhabited by the flat substrate. Quantum-gravity auditors cite it as the one-object partial closure of Track 1.C. It is a structure packing three named propositions, not a proved identity from simplex geometry.
Claim. A certificate over vertex type $V$ and finite bone type $B$ comprises three facts: (1) for every Schläfli-satisfying Regge triangulation $R$ and every vertex $v$, the contracted discrete Bianchi holds at $v$; (2) for every abstract Regge datum $R$ and vertex $v$, contracted discrete Bianchi at $v$ if and only if the Schläfli identity at $v$; (3) the type of Schläfli-satisfying Regge triangulations is nonempty (flat all-deficits-zero witness).
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.
Abstract Regge data supply vertex positions in $\mathbb{R}^4$, bone incidence, deficit angles, bone areas, and vertex-area gradients. The Schläfli identity at $v$ is the componentwise vanishing of $\sum_b \varepsilon_b\cdot(\nabla_v A_b)$. The contracted discrete Bianchi at $v$ is defined to be that same proposition, so the two are definitionally identical. Schläfli-satisfying Regge data are Regge data carrying a proof of Schläfli at every vertex; that named hypothesis is the structural premise of Track 1.C pending a full simplex-geometry proof of Schläfli.
proof idea
No proof body: this is a structure whose three fields are propositions. Downstream, a single noncomputable constructor fills them by applying three already-proved facts: the implication from Schläfli data to contracted Bianchi at every vertex; the definitional iff between contracted Bianchi and Schläfli at a vertex; and inhabitation of Schläfli data by the flat (all-deficits-zero) substrate. A one-line inhabited theorem then wraps that constructor.
why it matters
This is the master cert object for Track 1.C partial closure in the Geometry.DiscreteBianchi module (structural theorem status: zero sorry, zero RS-internal axiom). It packages the conditional form of contracted discrete Bianchi under the Schläfli hypothesis, the structural equivalence that makes the two names interchangeable, and a non-vacuity witness so the hypothesis is not empty.
Downstream, discreteBianchiContractedCert inhabits the structure, and discreteBianchiContractedCert_inhabited records nonemptiness; those feed the one-statement Track 1.C theorem section. In the broader RS gravity program this is the discrete kinematic half of Einstein-tensor conservation on the Regge side, complementary to continuum Track 1.B. It does not yet discharge the multi-session Mathlib geometry work needed for unconditional Schläfli from simplex volume-area relations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.