Track1BCStructuralCert
plain-language theorem explainer
A certificate packing the structural Regge-to-Einstein-Hilbert continuum property, the structural contracted discrete Bianchi property, their conjunction, and an inhabitant of the master classical-recovery hypothesis. Gravity and discrete-geometry workers cite it when wiring Track 1.B/1.C into the Session 97 master theorem. It is a pure structure definition; inhabitation is supplied by the canonical flat-substrate witnesses.
Claim. A Track 1.B/1.C structural certificate is a record with four fields: (i) the structural Regge-EH continuum property (for every lattice spacing the abstract Regge action equals the abstract Einstein-Hilbert action); (ii) the structural discrete Bianchi property (there exists a finite Schläfli-satisfying Regge triangulation witnessing the contracted second Bianchi identity at every vertex); (iii) the conjunction of (i) and (ii); (iv) an inhabitant of the master hypothesis that packages discrete-to-continuum Regge$\to$EH convergence together with contracted discrete Bianchi.
background
Module Gravity.Track1BCStructural ships the structural witness for the master-theorem hypothesis input that combines Track 1.B (Regge action converges to Einstein-Hilbert as lattice spacing shrinks) and Track 1.C (contracted second Bianchi on the Regge substrate). Status is structural theorem: zero sorry, zero RS-internal axiom; unconditional geometric closure still needs residual estimates and Schläfli for a physical triangulation.
The structural Regge-EH property asserts that for every real spacing the abstract Regge action equals the abstract EH action. On the flat canonical substrate both actions vanish, so the equality is immediate. The structural discrete Bianchi property asserts existence of finite types $V,B$ with a nonempty Schläfli-Regge datum (from Geometry.DiscreteBianchi), which is enough to witness the contracted identity at every vertex.
Upstream, MasterTheorem.RegEHContinuumAndBianchi is the load-bearing D2 classical-recovery hypothesis: a Prop for continuum convergence with explicit error bound, a proof of that Prop, a Prop for contracted discrete Bianchi, and a proof of that Prop. The present certificate is the typed container that feeds those four slots with structural content.
proof idea
No proof body: the declaration is a structure. Its four fields are pure data obligations. Field one demands an inhabitant of the structural Regge-EH continuum Prop. Field two demands an inhabitant of the structural discrete Bianchi Prop. Field three demands a proof of their conjunction. Field four demands a value of type RegEHContinuumAndBianchi from MasterTheorem.
Downstream, the concrete value track1BCStructuralCert fills the fields by the flat-substrate canonical witnesses, the already-proved conjunction lemma, and the packaged master witness regEHContinuumAndBianchiWitness. The inhabited theorem is then a one-line Nonempty introduction.
why it matters
This structure is the typed interface between the structural Track 1.B/1.C work and the Session 97 master theorem. Downstream, track1BCStructuralCert inhabits it, and track1BCStructuralCert_inhabited records Nonempty of the certificate; the module's one-statement corollary then advertises combined structural closure of Regge-EH continuum plus contracted discrete Bianchi.
In the Recognition gravity program this is the D2 classical-recovery hinge: discrete curvature calculus must recover continuum Einstein-Hilbert kinematics and the Bianchi identity that enforces local conservation. The certificate makes that hinge machine-checkable under named geometric hypotheses, while leaving the hard residual and Schläfli proofs as future multi-session Mathlib simplicial-geometry work.
It does not touch the forcing chain T0-T8, the Recognition Composition Law, or the phi-ladder mass formula; its job is strictly the discrete-to-continuum gravity bridge inside Track 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.