discrete_bianchi_structural_prop
plain-language theorem explainer
Packages Track 1.C as an existential: some finite-edge Regge complex admits Schläfli data at every vertex. Gravity workers cite it when wiring the contracted discrete Bianchi into the master-theorem hypothesis. The body is a pure Prop abbreviation, not a proved identity.
Claim. There exist types $V$ (vertices) and $B$ (bonds/edges) with $B$ finite such that the type of Schläfli-satisfying Regge data on $(V,B)$ is inhabited. Under that data, the contracted second Bianchi identity holds at every vertex.
background
This module supplies the structural witness for the master-theorem input combining Track 1.B (Regge action $\to$ Einstein–Hilbert continuum limit) and Track 1.C (contracted discrete Bianchi on the Regge substrate). Both pieces are kinematic: named hypotheses plus non-vacuous flat/Unit witnesses; full geometric closure is deferred.
Upstream, SchlafliReggeData is a Regge triangulation that extends ordinary Regge data by a Schläfli identity at every vertex. That identity is the named structural hypothesis of Track 1.C: once it holds, the contracted discrete Bianchi identity holds vertexwise (Session 98, Geometry.DiscreteBianchi).
The Prop below does not assert Bianchi directly. It asserts existence of some finite-bond complex carrying such Schläfli data, so the Track 1.C half of the combined structural claim is inhabitably true.
proof idea
Definitional packaging only. The right-hand side is the existential
$\exists, V, B,[\mathrm{Fintype}, B],;\mathrm{Nonempty}(\mathrm{SchlafliReggeData}, V, B)$.
No tactics or lemmas fire here; inhabitation is supplied later by the Unit-typed canonical witness that applies SchlafliReggeData_inhabited.
why it matters
This is the Track 1.C half of the structural certificate that feeds Gravity.MasterTheorem.RegEHContinuumAndBianchi. Downstream, discrete_bianchi_canonical_witness proves the Prop via a Unit triangulation; reg_eh_continuum_and_bianchi_structural_holds conjoins it with the Regge–EH continuum Prop; regEHContinuumAndBianchiWitness and Track1BCStructuralCert install both halves as the master-theorem hypothesis inhabitant; track1BC_one_statement packages the one-line structural closure.
In the RS gravity program this is the discrete conservation law side of the Einstein equation on a Regge lattice: Schläfli $\Rightarrow$ contracted Bianchi at vertices. Unconditional closure still needs a physical triangulation with a proved Schläfli identity and the geometric residual bound for Track 1.B.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.