with
plain-language theorem explainer
Packages the structural, hypothesis-gated form of Gravity Tracks 1.B and 1.C: a geometric residual bound for Regge-to-Einstein-Hilbert continuum convergence, plus the Schläfli identity hypothesis for contracted discrete Bianchi. Anyone wiring the master-theorem input RegEHContinuumAndBianchi cites this bundle. It is a pure structure definition (no proof body); inhabitation is supplied by separate canonical witnesses on a flat substrate.
Claim. A structure that carries the named structural hypotheses for combined Track 1.B/1.C: (i) a geometric residual bound $|S_{\mathrm{Regge}}-S_{\mathrm{EH}}|\le C\cdot\mathrm{spacing}$ along any refinement schedule, under which the Regge action converges to the Einstein-Hilbert action as lattice spacing tends to zero; (ii) the Schläfli identity at every vertex, under which the contracted discrete Bianchi identity holds at every vertex. The fields are structural propositions, not unconditional theorems.
background
Module Gravity.Track1BCStructural ships the structural witness for the master-theorem hypothesis RegEHContinuumAndBianchi. Track 1.B is discrete-to-continuum convergence of the Regge action to the Einstein-Hilbert action; its structural form assumes a named geometric-residual bound $|S_{\mathrm{Regge}}-S_{\mathrm{EH}}|\le C\cdot\mathrm{spacing}$ for any refinement schedule. Track 1.C is the contracted second Bianchi identity on the Regge substrate (from Geometry.DiscreteBianchi); its structural form assumes the Schläfli identity at every vertex.
Both pieces are kinematic content under named hypotheses. Canonical witnesses on a flat substrate give non-vacuous inhabitation. Abstract action maps parameterized by lattice spacing (abstract_regge_action, abstract_eh_action) and the corresponding structural propositions sit alongside this structure in the same module. Fully unconditional closure still needs the actual residual estimate and a Schläfli proof on a physical Regge triangulation.
proof idea
No proof. The declaration is a structure (definitional packaging) with proof_style def_or_abbrev and an empty body. It only assembles the geometric-residual and Schläfli structural propositions as fields; separate canonical-witness declarations inhabit those fields on a flat substrate.
why it matters
This structure is the data shape behind the combined structural witness regEHContinuumAndBianchiWitness, which inhabits the Session 97 master-theorem hypothesis RegEHContinuumAndBianchi from Gravity.MasterTheorem. It records that Track 1.B/1.C enter the gravity master theorem as structural Props (residual bound + Schläfli), not as unconditional theorems. The module claims 0 sorry and 0 RS-internal axiom for this structural layer (closure 2026-05-22). Unconditional Track 1.B/1.C remains open multi-session geometric work in simplicial geometry. No direct downstream edges are recorded for this declaration itself; its role is to type the witness that feeds the master theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.