concretePhysicalBianchiProp
plain-language theorem explainer
The physical D2 Bianchi clause states that for arbitrary vertex and bond types, every Schläfli-satisfying Regge datum obeys the contracted discrete Bianchi identity at every vertex. Discrete-gravity and master-theorem auditors cite it as the concrete Bianchi half of the unconditional Regge–EH continuum-and-Bianchi witness. It is a definitional wrapper: a universal quantification of the Track-1.C physical Schläfli–Bianchi master proposition.
Claim. For all types $V$ and $B$ with $B$ finite, every Schläfli-satisfying Regge datum $R$ on $(V,B)$ and every vertex $v\in V$ satisfy the contracted discrete Bianchi identity of $R$ at $v$.
background
This module closes the unconditional route into the quantum-gravity master theorem by installing theorem-built witnesses for five inputs that the older conditional master theorem took as arguments. The D2 slot is a pair: a Regge-to-Einstein–Hilbert continuum clause and a discrete Bianchi clause. The primary route names physical content directly rather than endpoint receipts.
The upstream Track-1.C master clause says that Schläfli-satisfying Regge data obey the contracted discrete Bianchi identity at every vertex: for fixed vertex type $V$ and finite bond type $B$, every SchlafliReggeData $R$ and every $v\in V$ satisfy the contracted identity on the underlying Regge data. Schläfli data are the discrete curvature carriers in the Regge calculus setting used throughout the gravity track.
The present definition lifts that fixed-type clause to a single proposition by quantifying over all $V$ and finite $B$. That matches the module doc’s Bianchi half of the primary D2 witness: “for any vertex and bond types, every Schläfli-satisfying Regge datum obeys the contracted discrete Bianchi identity at every vertex.”
proof idea
Definitional, not a proof. The body is the universal statement $\forall, V, B, [\mathrm{Fintype}, B]$, the Track-1.C physical Schläfli–Bianchi master proposition at $(V,B)$. No tactics or lemmas fire here; the companion inhabitance theorem discharges the Prop by introducing $V,B$ and applying the upstream master-proposition theorem.
why it matters
This Prop is the Bianchi field of the primary D2 witness canonicalRegEHContinuumAndBianchiWitness, which pairs it with the physical product-filter Regge/EH continuum clause and supplies both inhabitance proofs. The same Prop is reused on the audit endpoint-receipt D2 witness, so both routes share one physical Bianchi statement.
The non-circularity audit discloses that the D2 Bianchi field equals this definition by rfl, pinning the master-theorem interface to the Schläfli contracted-Bianchi content rather than an opaque placeholder. In the Recognition gravity stack this is the discrete conservation half of the Regge calculus bridge into the continuum Einstein–Hilbert side of D2; it does not itself invoke the forcing chain T0–T8, but it is required infrastructure for the unconditional master-theorem closure surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.