canonicalRegEHContinuumAndBianchiWitness
plain-language theorem explainer
Primary D2 witness packing physical Regge-to-Einstein–Hilbert product-filter continuum convergence with the Schläfli contracted discrete Bianchi identity. Gravity auditors and the zero-argument quantum-gravity master assembly cite it as the unconditional D2 input. It is a four-field structure instance: two concrete physical propositions plus their holds proofs, with no endpoint-receipt indirection.
Claim. The canonical D2 witness is an inhabitant of the Regge/EH-plus-Bianchi structure whose continuum clause is the physical product-filter convergence proposition (normalized full nonlinear Regge aggregate $\to$ continuum Einstein–Hilbert integral on the canonical periodic six-tet cubic torus), whose Bianchi clause is the Schläfli contracted discrete Bianchi identity (for any vertex and bond types), and whose two holds fields are the corresponding proofs of those propositions.
background
This module closes the older conditional quantum-gravity master theorem by installing theorem-built witnesses for its five external inputs. The D2 slot is the continuum and Bianchi package: Regge calculus on a simplicial ledger must recover the Einstein–Hilbert continuum action under refinement, and the discrete curvature data must obey a contracted Bianchi identity at every vertex.
The primary route names physical content directly. The Regge/EH clause asserts that for any product-filter refinement data on the canonical periodic six-tet cubic torus, the normalized full nonlinear Regge aggregate converges to the supplied continuum EH integral. The Bianchi clause asserts that every Schläfli-satisfying Regge datum obeys the contracted discrete Bianchi identity at every vertex. An older endpoint-receipt packaging is retained only as an audit alternate.
Upstream continuum-bridge work identifies discrete ledger energy with Laplacian action via shared-face weights; this witness sits at the gravity layer that consumes those facts as master inputs.
proof idea
Pure structure construction, not a tactic proof. The four fields of the Regge/EH-plus-Bianchi master structure are assigned to the sibling concrete physical propositions and their holds theorems: continuum proposition and proof for the Regge-to-EH clause; Schläfli Bianchi proposition and proof for the discrete Bianchi clause. No further rewriting or endpoint-receipt composition occurs on this primary route.
why it matters
This is the D2 input consumed by the zero-argument assembly that builds the RS quantum-gravity master from five canonical witnesses (D2 continuum+Bianchi, D3 amplitude linearity, D4 Page transfer, D5 PTA band, D5 strong-field channels). Downstream non-circularity audit theorems disclose that the Regge field equals the concrete product-filter convergence proposition and the Bianchi field equals the Schläfli contracted-Bianchi proposition, then fold both into the all-witness-fields theorem and the one-statement non-circularity certificate: the master consumes only standalone theorems.
In the Recognition gravity stack this closes the continuum and identity half of the discrete-to-continuum bridge that the conditional master previously took as hypotheses. It does not by itself claim a full physical quantum-gravity framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.