regEHContinuumAndBianchiWitness

Track 1.B/1.C is the classical-recovery load-bearing piece (D2) of the RS gravity master theorem. Track 1.B asserts discrete-to-continuum convergence of the Regge action to the Einstein-Hilbert action: under a named geometric-residual bound $|S_{\mathrm{Regge}}-S_{\mathrm{EH}}|\le C\cdot h$ along a refinement schedule, the actions agree as lattice spacing $h\to 0$. Track 1.C asserts the contracted second Bianchi identity on the Regge substrate, obtained from the Schläfli identity at every vertex (Session 98, Geometry.DiscreteBianchi).

This module ships only the structural forms. The Regge-EH structural Prop says the abstract Regge and EH actions (parameterized by spacing) are equal for every spacing; on the flat canonical substrate both vanish, so equality is immediate. The discrete-Bianchi structural Prop is existential: some finite Schläfli-satisfying triangulation exists. The master-theorem structure RegEHContinuumAndBianchi packages both Props together with proofs that they hold, and is documented as the open D2 classical-recovery hypothesis closed by Track 1.B/1.C sessions.

Unconditional closure still needs the actual geometric residual estimate and a Schläfli proof for a physical (non-flat) Regge triangulation.

Pure structure inhabitant, not a tactic proof. The four fields of RegEHContinuumAndBianchi are assigned directly:

• continuum Prop ← regge_eh_continuum_structural_prop (∀ spacing, abstract Regge action = abstract EH action);
• continuum witness ← regge_eh_continuum_canonical_witness (intro spacing; unfold both abstract actions; rfl, since both are identically zero on the flat substrate);
• Bianchi Prop ← discrete_bianchi_structural_prop (∃ finite Schläfli-satisfying Regge data);
• Bianchi witness ← discrete_bianchi_canonical_witness (packages the inhabited SchlafliReggeData instance on Unit).

No further rewriting or geometric estimate is performed here.

This witness is the concrete object that lets the Session-97 master theorem run with zero open hypothesis inputs on the classical-recovery slot. Downstream it is plugged straight into rs_quantum_gravity_master_structural and the one-statement form, into MasterTheoremStructuralCert, and into the honest-scope statement that records Nonempty RegEHContinuumAndBianchi. Inside the same module it is the master_hypothesis_witness field of track1BCStructuralCert and appears in track1BC_one_statement.

Framework role: classical GR recovery on the discrete substrate (Regge calculus → continuum EH, plus Bianchi consistency) is the bridge from the eight-tick / D=3 forcing chain to continuum gravity. The structural form closes the Lean skeleton; the dynamical upgrade (geometric residual + physical Schläfli) remains the open multi-session geometric task flagged in the module doc and in the honest-scope statement.