reg_eh_continuum_and_bianchi_structural_holds
plain-language theorem explainer
Both the structural Regge-to-Einstein-Hilbert continuum property and the structural discrete Bianchi property hold simultaneously. Gravity auditors cite this as the combined Track 1.B/1.C witness feeding the master-theorem hypothesis package. The proof is a pure pairing of the two flat-substrate canonical witnesses.
Claim. The structural Regge--Einstein-Hilbert continuum property and the structural discrete Bianchi property both hold: under a named geometric-residual bound $|S_{\mathrm{Regge}}-S_{\mathrm{EH}}|\le C\cdot\mathrm{spacing}$, the Regge action converges to the Einstein-Hilbert action as lattice spacing tends to zero, and under the Schläfli identity at every vertex the contracted discrete Bianchi identity holds at every vertex.
background
This module closes the structural half of Gravity Tracks 1.B and 1.C for the master-theorem input that packages Regge-EH continuum convergence with discrete Bianchi. Track 1.B concerns discrete-to-continuum passage: abstract Regge and Einstein-Hilbert actions are parameterized by lattice spacing, and the structural proposition asserts that whenever a geometric residual bound of the form $|S_{\mathrm{Regge}}-S_{\mathrm{EH}}|\le C\cdot\mathrm{spacing}$ holds along a refinement schedule, the Regge action converges to the EH action as spacing shrinks to zero.
Track 1.C imports the contracted second Bianchi identity on a Regge substrate. Its structural form states that, given the Schläfli identity at every vertex, the contracted discrete Bianchi identity holds at every vertex. Both pieces are kinematic: they ship content under named hypotheses, with flat-substrate (Unit-typed Schläfli triangulation) canonical witnesses supplying non-vacuous inhabitation rather than a full geometric residual or physical-triangulation Schläfli proof.
proof idea
Term-mode pair constructor. The left conjunct is discharged by the canonical witness for the structural Regge-EH continuum proposition (flat substrate). The right conjunct is discharged by the canonical witness for the structural discrete Bianchi proposition (Unit-typed Schläfli triangulation). No further rewriting or tactic search is required; the theorem is exactly the product of those two inhabitants.
why it matters
This is the single combined holds-statement consumed by the Track 1.B/1.C structural certificate, which in turn inhabits the master-theorem hypothesis input RegEHContinuumAndBianchi from Gravity.MasterTheorem (Session 97). Downstream the certificate records the two canonical witnesses, this conjunction, and the master-hypothesis witness in one package, retiring the combined continuum-plus-Bianchi obligation from the conditional master list.
In the broader Recognition gravity program this is kinematic scaffolding for discrete gravity: Regge calculus as the lattice avatar of Einstein-Hilbert, with discrete Bianchi guaranteeing local conservation structure on the substrate. Unconditional Track 1.B/1.C closure still needs the actual geometric residual proof and a Schläfli identity for a concrete physical Regge triangulation (multi-session simplicial-geometry work). The present result only certifies that the structural Props are inhabited and may be fed upward.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.