track1BCStructuralCert_inhabited
plain-language theorem explainer
The Track 1.B/1.C structural certificate is inhabited: Regge-to-Einstein-Hilbert continuum convergence and the contracted discrete Bianchi identity both hold in structural form under named geometric hypotheses, via canonical witnesses. Anyone wiring the master theorem's RegEHContinuumAndBianchi hypothesis input cites this. The proof is a one-line term inhabitation by the prebuilt canonical certificate.
Claim. The type of Track 1.B/1.C structural certificates is nonempty: there exist a structural Regge--Einstein-Hilbert continuum proposition, a structural discrete Bianchi proposition, a proof of their conjunction, and a witness inhabiting the master-theorem hypothesis package for combined Regge--EH continuum convergence and discrete Bianchi.
background
This module supplies the structural witness for Gravity Tracks 1.B and 1.C in the Recognition Science master theorem. Track 1.B is discrete-to-continuum convergence of the Regge action to the Einstein-Hilbert action: under a named geometric-residual hypothesis of the form $|S_{\mathrm{Regge}}-S_{\mathrm{EH}}|\le C\cdot\mathrm{spacing}$ along any refinement schedule, the Regge action converges to the EH action as lattice spacing tends to zero. Track 1.C is the contracted second Bianchi identity on a Regge substrate: under the Schläfli identity at every vertex, the contracted discrete Bianchi holds at every vertex.
Both pieces are structural. They carry the kinematic content under named hypotheses, with canonical witnesses (flat substrate for Regge-EH; a Schläfli-satisfying triangulation for Bianchi) giving non-vacuous inhabitation. The certificate structure packages the two structural propositions, their conjunction, and a field inhabiting the master-theorem hypothesis input for the combined package.
proof idea
One-line term proof. The module already defines a canonical certificate whose four fields are the Regge-EH structural proposition, the discrete Bianchi structural proposition, a proof of their conjunction, and the master-hypothesis witness built from those props. The proof simply packages that canonical value as a term of type Nonempty of the certificate structure.
why it matters
The Session 97 gravity master theorem takes the combined Regge-EH continuum and discrete Bianchi package as a hypothesis input. This declaration shows that input is non-vacuously inhabited at the structural level, so the conditional master theorem can be instantiated without an empty hypothesis slot. Module status is structural theorem: zero sorry, zero RS-internal axiom, closure dated 2026-05-22.
It does not finish the fully unconditional Track 1.B/1.C closure. That still needs the geometric residual estimate and the Schläfli identity for a physical Regge triangulation (multi-session work in simplicial geometry). The graph currently lists no downstream users, so this is a leaf certificate ready for master-theorem wiring rather than an already-consumed lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.