track1BCStructuralCert
plain-language theorem explainer
Packages the Regge–Einstein–Hilbert continuum witness and the contracted discrete Bianchi witness into one structural certificate for the gravity master-theorem hypothesis. Anyone discharging Session 97's combined Track 1.B/1.C input cites this object for non-vacuous inhabitation on the flat substrate. The body is a pure field assignment from four already-established canonical witnesses.
Claim. There is a structural certificate whose fields are: the Regge–EH continuum structural property (convergence of the abstract Regge action to the Einstein–Hilbert action under a geometric residual bound linear in lattice spacing); the contracted discrete Bianchi structural property (under the Schläfli identity at every vertex); their conjunction; and an inhabitant of the master-theorem hypothesis that demands both pieces.
background
This module closes the structural side of Gravity Tracks 1.B and 1.C for the Session 97 master theorem. Track 1.B is discrete-to-continuum convergence: under a named residual hypothesis $|S_{\mathrm{Regge}}-S_{\mathrm{EH}}|\le C\cdot\mathrm{spacing}$ along any refinement schedule, the Regge action tends to the Einstein–Hilbert action as spacing shrinks. Track 1.C is the contracted second Bianchi identity on the Regge substrate: under the Schläfli identity at every vertex, the contracted discrete Bianchi holds at every vertex (imported from Geometry.DiscreteBianchi).
Both pieces are kinematic. Canonical witnesses live on a flat (Unit-typed) substrate and only show the structural Props are inhabited, not that a physical triangulation satisfies the residual bound or Schläfli. Abstract Regge and EH actions are spacing-parameterized functions; the continuum structural Prop quantifies over spacing and compares them. The certificate structure bundles those Props, their conjunction, and the master-hypothesis inhabitant built from them.
proof idea
Pure structure construction, not a tactic proof. The four fields of the certificate are filled by direct assignment: the Regge–EH continuum field to the flat-substrate continuum witness (which reduces by unfolding the abstract actions and rfl); the discrete Bianchi field to the Unit/Schläfli canonical witness; the conjunction field to the theorem that pairs those two witnesses; and the master-hypothesis field to the pre-built inhabitant that installs the structural Props and their holds-proofs into the Session 97 hypothesis record.
why it matters
Supplies the single packaged object that track1BCStructuralCert_inhabited uses to prove the certificate type is nonempty, giving the module its one-statement structural closure. Downstream, that inhabitation is how the master theorem's RegEHContinuumAndBianchi hypothesis is discharged at the structural level without RS-internal axioms or sorry. In the broader Recognition gravity program this is the kinematic bridge from discrete Regge data to continuum EH plus Bianchi conservation, sitting under the forcing-chain geometry (D=3, eight-tick discrete time) rather than replacing it. Unconditional Track 1.B/1.C still needs the geometric residual proof and a Schläfli proof for a concrete physical triangulation; this certificate deliberately stops at the structural layer so those multi-session Mathlib geometry obligations remain isolated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.