D2ScopeStatus
plain-language theorem explainer
Status record for the D2 classical-recovery claim (nonlinear Regge calculus to continuum Einstein-Hilbert on the canonical periodic six-tet torus). Four booleans mark what is proved versus still open: the reduction itself, quadrature convergence, residual vanishing, and general triangulations. Gravity auditors and master-theorem consumers cite it to read the honest frontier without opening data structures. Pure structure definition; no proof content.
Claim. A four-field boolean status record for D2 classical recovery on the canonical periodic six-tetrahedron torus: whether the reduction (quadrature convergence plus vanishing Regge residual imply full nonlinear Regge $\to$ continuum Einstein-Hilbert on the product filter) is proved; whether the quadrature-convergence analytic target remains open; whether the uniform residual-vanishing target remains open; and whether the extension beyond the canonical triangulation remains open.
background
D2 is the classical-recovery witness consumed by the unconditional gravity master theorem: full nonlinear Regge action on the canonical periodic six-tet cubic torus converges to the continuum Einstein-Hilbert / Dirichlet integral on a product filter. The module frames this as peer-review finding F2 / Rec 3: the witness is a real Tendsto statement, not a vacuous True.
Reading the physical six-tet instance, the datum carries two analytic hypothesis fields: quadrature convergence of the canonical periodic six-tet rule to the continuum EH integral, and a uniform envelope on the (full nonlinear Regge minus quadrature) residual. The combination of those two by a triangle-inequality squeeze is a genuine theorem; the honest status is therefore a reduction, not a from-primitives closure.
This structure is the audit surface that names those pieces separately so open analytic inputs are not buried inside a large data structure.
proof idea
No proof: a four-field structure declaration. Each field is a Bool flag. The companion value d2ScopeStatus fills them as reduction_proved := true and the three open-frontier flags true. Downstream code reads the record rather than re-deriving scope from nested hypotheses.
why it matters
Pins the honest D2 frontier for the gravity master theorem path. Downstream, d2ScopeStatus is the sole inhabitant cited by the audit module: reduction proved on the canonical periodic six-tet torus; quadrature target, residual target, and general-triangulation extension all still open. That matches the module claim that fullReggeProduct_tendsto_continuum is a genuine squeeze theorem conditional on two analytic inputs, not a primitives-to-continuum closure.
Without this record, reviewers would have to unpack PhysicalSixTetCubicDirichletInstance hypothesis fields to learn what remains. The structure makes the open questions first-class: discharge D2QuadratureConvergenceTarget from mesh geometry, discharge D2ResidualVanishingTarget for the nonlinear residual envelope, and extend past the canonical six-tet triangulation. It does not itself touch T0-T8 forcing, RCL, or the phi ladder; it is a gravity-side scoping artifact for classical recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.