track1BC_one_statement
plain-language theorem explainer
Structural Track 1.B (Regge action equals Einstein-Hilbert at every lattice spacing) and Track 1.C (existence of a Schläfli-satisfying Regge triangulation, hence contracted discrete Bianchi) both hold, and the master classical-recovery hypothesis packing them is inhabited. Classical-recovery and continuum-limit arguments in the gravity stack cite this as the single combined structural closure. The proof is a term triple of the two canonical witnesses plus the master-structure inhabitant.
Claim. The structural Regge-to-Einstein-Hilbert continuum property holds (for every lattice spacing the abstract Regge action equals the abstract Einstein-Hilbert action), the structural discrete Bianchi property holds (there exist finite types witnessing a Schläfli-satisfying Regge triangulation), and the master hypothesis structure that packages both continuum convergence and contracted discrete Bianchi is inhabited.
background
This module ships the structural witness for Tracks 1.B and 1.C feeding the gravity master theorem. Track 1.B is discrete-to-continuum convergence of the Regge action to the Einstein-Hilbert action. The structural form asserts that for every real lattice spacing the abstract Regge and EH actions agree; on the flat-substrate canonical witness both actions are zero, so the difference vanishes identically. The unconditional form (a residual bound $|S_{\mathrm{Regge}}-S_{\mathrm{EH}}|\le C\cdot\mathrm{spacing}$ along a refinement schedule) remains open geometric work.
Track 1.C is the contracted second Bianchi identity on a Regge substrate, drawn from Geometry.DiscreteBianchi. Its structural form is existence of a Schläfli-satisfying triangulation, which forces contracted discrete Bianchi at every vertex. The master structure from Gravity.MasterTheorem packages both pieces as the load-bearing D2 classical-recovery hypothesis input; its doc calls it "Currently OPEN; closed by Track 1.B/1.C sessions."
proof idea
Pure term proof: a triple constructor. The first component is the Regge-EH canonical witness, which introduces an arbitrary spacing, unfolds the two abstract actions, and closes by rfl (both are definitionally zero on the flat substrate). The second is the discrete-Bianchi canonical witness: Unit vertex and bond types with the inhabited Schläfli-Regge data instance. The third is a Nonempty package around the master-structure inhabitant, whose fields are exactly those two structural props filled by the same two witnesses.
why it matters
This is the one-statement structural closure of Tracks 1.B and 1.C. It inhabits the Session-97 master hypothesis that the continuum limit of Regge gravity plus contracted discrete Bianchi hold, the D2 classical-recovery piece required before Einstein gravity can be recovered from the discrete Recognition substrate. The module status line records structural theorem with zero sorry and zero RS-internal axiom (closure 2026-05-22).
No downstream used_by edges are recorded yet; the declaration is a terminal packaging theorem inside the Track 1.B/1.C module. The doc is explicit that fully unconditional closure (geometric residual estimate plus Schläfli on a physical triangulation) remains multi-session geometric work in simplicial-geometry tooling. Framework context: continuum recovery of GR on the discrete lattice whose spatial dimension is forced to $D=3$ and whose tick structure is the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.