d2_bianchi_field_is

This module audits the unconditional quantum-gravity master theorem field by field. A referee objection is that witness structures of shape $\Sigma(P:\mathrm{Prop}), P$ can be inhabited by trivial placeholders, so the master claim is only as strong as the concrete propositions in its slots. For each atom the audit supplies an rfl-level disclosure of what proposition the field actually is, plus a standalone proof that it holds without assuming the master conclusion.

The D2 witness packages two physical clauses: product-filter Regge-to-Einstein–Hilbert continuum convergence, and a Schläfli-based contracted discrete Bianchi identity. The Bianchi proposition is the universal statement that, for any vertex and bond types, every Schläfli-satisfying Regge datum obeys the contracted discrete Bianchi identity at every vertex. The canonical witness fills its discrete-Bianchi field with exactly that proposition and records a separate holding proof.

One-line term proof by rfl. The canonical Regge/EH continuum-and-Bianchi witness is defined with its discrete contracted-Bianchi field set equal to the concrete physical Bianchi proposition, so the equality is definitional and needs no further lemmas.

Peer-review finding F1 / Rec 2 demands that every master-theorem witness field be inspectably non-self-referential. This disclosure pins the D2 Bianchi slot to a named Schläfli contracted-Bianchi $\forall$-statement rather than True or the master conclusion itself. Together with the sibling field disclosures and the unconditional holding proofs, it supports the module claim that the master conjunction is assembled from independently proved, concretely named propositions. No downstream consumers are recorded yet; the declaration is audit infrastructure for the gravity master theorem, not a computational lemma on the phi-ladder or T0–T8 chain.