concretePhysicalBianchiProp_holds
plain-language theorem explainer
Every Schläfli-satisfying Regge datum obeys the contracted discrete Bianchi identity at every vertex, for arbitrary vertex and bond types. Gravity auditors cite this as the Bianchi half of the primary D2 witness that closes the unconditional master theorem. The proof is a one-line handoff to the physical Schläfli–Bianchi master proposition on Track-1 residuals.
Claim. The concrete physical Bianchi proposition holds: for any vertex type $V$ and bond type $B$, every Schläfli-satisfying Regge configuration on those types obeys the contracted discrete Bianchi identity at every vertex.
background
This module closes the five inputs of the older conditional quantum-gravity master theorem by installing zero-argument, theorem-built witnesses. The D2 slot is a pair: a Regge-to-Einstein–Hilbert continuum clause and a discrete Bianchi clause. The Bianchi clause is the proposition proved here.
In discrete gravity, the classical Schläfli identity relates variations of deficit angles and edge lengths. The contracted discrete Bianchi identity is the discrete stand-in for $\nabla^a G_{ab}=0$: at each vertex the weighted sum of hinge deficits vanishes once the Schläfli relations hold. The module states the physical content directly: for any vertex and bond types, every Schläfli-satisfying Regge datum obeys that contracted identity at every vertex.
An alternate audit route still routes D2 through endpoint receipts from the handoff integration layer; the primary witness names this physical proposition instead of those receipts.
proof idea
Term-mode wrapper. Introduce the vertex type $V$, bond type $B$, and the unused residual hypothesis, then discharge by exact application of Track1BCPhysicalResidual.physicalSchlafliBianchiMasterProp_holds at those $V$ and $B$. No local algebra: the entire content lives in that upstream master proposition on physical Schläfli–Bianchi residuals.
why it matters
This is the Bianchi half of the primary D2 witness. Downstream, canonicalRegEHContinuumAndBianchiWitness packages it with the physical product-filter Regge/EH continuum theorem as MasterTheorem.RegEHContinuumAndBianchi, with no endpoint-receipt indirection. The same Bianchi proof is reused by the endpoint-route audit witness.
In the Recognition gravity stack, D2 is one of the five inputs that turn the conditional master theorem into an unconditional closure surface. The Bianchi clause supplies discrete diffeomorphism consistency (contracted Bianchi) for Schläfli-satisfying Regge data, pairing with continuum EH convergence so the master theorem can treat Regge calculus as a controlled discrete Einstein theory rather than an ad-hoc lattice model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.