d2ScopeStatus
plain-language theorem explainer
Records the honest D2 classical-recovery scope on the canonical periodic six-tet torus: the reduction from quadrature-plus-residual hypotheses to full nonlinear Regge→EH continuum convergence is marked proved, while quadrature convergence, residual vanishing, and general triangulation remain open. Gravity auditors and master-theorem consumers cite this status snapshot. It is a pure structure instance with four Boolean flags.
Claim. On the canonical periodic six-tet torus, the D2 scope status is: the reduction is proved ($\mathrm{true}$), and the quadrature-convergence target, the residual-vanishing target, and the general-triangulation extension are each open ($\mathrm{true}$).
background
This module is the honest D2 (Regge → Einstein-Hilbert) scoping audit. The classical-recovery witness consumed by the master theorem is a product-filter continuum target on canonical periodic six-tet volume-quadrature data. That target is discharged by a full-Regge product limit, which itself is a genuine theorem: it combines two analytic hypothesis fields by a triangle-inequality squeeze.
Those fields are quadrature convergence of the six-tet rule to the continuum EH/Dirichlet integral, and a uniform residual bound on the full nonlinear Regge-minus-quadrature difference. The honest status of D2 is therefore a reduction, not a from-primitives closure: on this torus, quadrature convergence plus a vanishing residual envelope imply full nonlinear Regge → continuum EH convergence.
The structure being instantiated packages four Booleans: whether that reduction is proved, and whether the quadrature target, residual target, and general-triangulation extension remain open. Its doc-comment states the intended reading: reduction proved; two analytic inputs and general triangulation open.
proof idea
Definitional structure instance, not a proof. The four fields of the scope-status record are set by literals: reduction marked proved, and the three frontier flags marked open. No lemmas are applied; the body is pure data.
why it matters
Peer-review findings F2 / Rec 3 require that D2 not hide open analytic work inside a data structure. This status value is the machine-readable disclosure: the reduction (d2_reduction and its statement sibling) is claimed closed, while D2QuadratureConvergenceTarget, D2ResidualVanishingTarget, and general triangulation are named as the actual open frontier.
Downstream, the master theorem’s unconditional classical-recovery path consumes the continuum product-filter target; this audit keeps that consumption honest by separating proved reduction from unproved analytic inputs. No used-by edges are recorded yet; the value is the audit endpoint itself. It does not touch T0–T8 forcing, RCL, or the phi-ladder mass formula; it is gravity-side classical recovery bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.