RegEHContinuumAndBianchi
plain-language theorem explainer
Packages the two open D2 classical-recovery hypotheses for Recognition Science gravity: continuum convergence of the Regge action to Einstein-Hilbert with an explicit residual bound, and the discrete contracted Bianchi identity (Schläfli) on the Regge substrate. Anyone invoking the conditional quantum-gravity master theorem cites this as the classical-recovery slot. Pure structure definition: two Props plus inhabitation witnesses; no proof content.
Claim. A hypothesis package of two assertions: (i) the Regge action converges to the Einstein-Hilbert action in the continuum limit, with an explicit geometric residual bound; (ii) the contracted second Bianchi identity holds on the discrete Regge substrate (via the Schläfli identity). Both are currently open and are supplied as named hypothesis inputs to the conditional master theorem.
background
The Gravity MasterTheorem module authors the conditional master statement of the Recognition Science quantum-gravity program (Track 7.A). Eight of twelve clauses are already discharged from existing Lean theorems; five open tracks remain as hypothesis inputs. This structure is the input for Tracks 1.B and 1.C, the D2 classical-recovery piece.
Regge calculus discretizes spacetime by piecewise-flat simplicial complexes whose deficit angles encode curvature. Continuum recovery means the Regge action approaches the Einstein-Hilbert action with a controlled residual. The contracted second Bianchi identity is the discrete conservation law that, in the continuum, yields $\nabla^\mu G_{\mu\nu}=0$; on the lattice it is the Schläfli identity relating edge lengths and dihedral angles.
Spatial dimension $D=3$ is already forced upstream by the T8 step of the forcing chain. The present package does not re-derive that fact; it only bundles the still-open geometric estimates needed to recover classical GR from the discrete substrate.
proof idea
No proof body: the declaration is a structure definition. It exposes two fields of type Prop (continuum Regge-to-Einstein-Hilbert convergence, and discrete contracted Bianchi) together with two inhabitation fields that witness those Props. Downstream consumers take an inhabitant of the whole structure as a hypothesis input and project the two witnesses. Closing Tracks 1.B and 1.C means constructing a concrete term of this structure from a geometric residual estimate and a discrete Schläfli identity proof.
why it matters
This is the D2 classical-recovery slot in the twelve-clause master statement. The master-plan template requires both Regge-to-Einstein-Hilbert continuum convergence and discrete contracted Bianchi as one conjunct. Downstream, the master statement definition and the conditional master theorem take an inhabitant of this structure as their first hypothesis; the one-statement form quantifies over it. The deeper-partial master theorem likewise threads it, and ConditionalSlot wrappers surface the same Prop in consumer type signatures.
Until Tracks 1.B and 1.C close, the unconditional master theorem cannot be stated. The package therefore gates classical GR recovery inside the Recognition framework: without continuum Regge convergence and discrete Bianchi, the discrete recognition substrate does not yet recover Einstein gravity with local conservation. Framework landmarks already in place (T0-T8 forcing, cost uniqueness, Lorentzian $1+3$) sit upstream; this structure is the remaining geometric bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.