requires
plain-language theorem explainer
Scaffolding marker for Gravity Track 1.B/1.C: structural witnesses for Regge-to-Einstein-Hilbert continuum convergence and the discrete contracted Bianchi identity still need upgrade to unconditional dynamical proofs. Cite it when auditing the master-theorem input RegEHContinuumAndBianchi. The body is an empty sorry stub; closure waits on a geometric residual bound and Schläfli on a physical triangulation.
Claim. The structural witnesses for Regge--Einstein-Hilbert continuum convergence and the discrete contracted Bianchi identity require upgrade to unconditional dynamical derivations: a geometric residual estimate $|S_{\mathrm{Regge}} - S_{\mathrm{EH}}| \le C \cdot \mathrm{spacing}$ under refinement, and the Schläfli identity at every vertex of a physical Regge triangulation.
background
Module Gravity.Track1BCStructural ships the combined structural witness for the master-theorem hypothesis RegEHContinuumAndBianchi. Track 1.B is discrete-to-continuum convergence of the Regge action to the Einstein-Hilbert action: under a named geometric-residual hypothesis $|S_{\mathrm{Regge}}-S_{\mathrm{EH}}|\le C\cdot\mathrm{spacing}$, the Regge action converges as lattice spacing tends to zero. Track 1.C is the contracted second Bianchi identity on the Regge substrate: under Schläfli at every vertex, the contracted discrete Bianchi holds at every vertex.
Both pieces are kinematic. Abstract Regge and EH actions are functions of lattice spacing; the flat substrate is the canonical non-vacuous witness (Regge action zero for any spacing). Unconditional closure is deferred to multi-session simplicial-geometry work: an actual residual proof plus Schläfli for a concrete physical triangulation.
proof idea
Empty sorry stub: no tactics, no term, no lemmas applied. The declaration records the upgrade obligation rather than discharging it. Downstream structural Props and canonical flat-substrate witnesses already inhabit the kinematic forms; this stub marks that those do not yet replace the named residual and Schläfli hypotheses with proved geometry.
why it matters
Sits on the critical path into Gravity.MasterTheorem's hypothesis RegEHContinuumAndBianchi. The module's witness regEHContinuumAndBianchiWitness already packages structural Props for both Track 1.B and 1.C; this scaffolding item is the explicit gap between that kinematic package and a dynamical, hypothesis-free derivation.
In the broader RS gravity story, continuum recovery of EH plus discrete Bianchi are the bridge from the recognition lattice to classical GR kinematics. Closing the residual estimate and Schläfli on a physical triangulation would convert the structural certificate into an unconditional Track 1.B/1.C theorem and remove the last named geometric hypotheses from that master-theorem input. Until then, any citation of full Track 1.B/1.C must flag those two open geometric obligations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.