D2ResidualVanishingTarget
plain-language theorem explainer
Names the second open analytic input of the D2 classical-recovery witness: uniform control of the full nonlinear Regge-minus-quadrature residual on the product filter, for a canonical periodic six-tet refinement family. Anyone citing the D2 reduction or damped-schedule residual theorems uses this Prop as the residual hypothesis. The body is a one-line alias of the product-filter uniform residual target already carried as a field on the physical instance.
Claim. For a base filter $\ell$ on index type $\alpha$, a canonical periodic six-tet cubic volume-quadrature refinement family $F$ indexed by $\rho$, and a refinement filter $\mathcal{R}$ on $\rho$, the residual-vanishing target asserts that the (full nonlinear Regge action minus the quadrature) residual is uniformly controlled along the product filter built from $\ell$ and $\mathcal{R}$.
background
The D2 scoping module audits the classical Regge-to-Einstein-Hilbert recovery path on the canonical periodic six-tet cubic torus. The master witness consumed downstream is a product-filter continuum target: full nonlinear Regge aggregates must tend to the continuum Einstein-Hilbert/Dirichlet integral. That witness is not closed from primitives; it is a reduction to two analytic fields on the physical six-tet instance.
Those fields are quadrature convergence (the discrete volume rule tends to the continuum integral) and uniform residual control (the difference between the full nonlinear Regge functional and that quadrature is squeezed uniformly on the product filter). The second field is exactly what this definition packages as a named proposition, so the open frontier is not buried inside a structure field named uniform_residual.
Locally, the module status is theorem-grade for the reduction itself (zero sorry): once both named targets hold, a triangle-inequality argument yields full product-filter convergence. Non-product and non-flat triangulations are out of scope.
proof idea
No proof: this is a Prop-valued definition. The body is a pure abbreviation of CanonicalPeriodicTetSixTetVolumeQuadratureProductUniformResidualTarget applied to the given refinement family and refinement filter. All mathematical content lives in that residual-target predicate; this name exists only to surface the second open D2 input in the audit vocabulary used by d2_reduction and the damped-schedule closures.
why it matters
This definition is the citation handle for remaining target 2 in the honest D2 audit. The reduction theorem d2_reduction (and its packaged form d2_reduction_statement) takes it as the residual hypothesis alongside the quadrature-convergence target, and concludes that the full nonlinear Regge aggregate converges to the continuum EH/Dirichlet integral on the product filter.
Downstream, the damped-schedule module discharges this target outright: d2_residual_vanishing_target_damped proves it for spacing-damped families from local curvature correspondence plus damping to zero, and d2_damped_schedule_closure_one_statement bundles that with quadrature-proxy preservation so full D2 convergence reduces to the quadrature limit alone. The flat-sector one-statement then closes residual vanishing with no supplied analytic field on the flattened damped route.
In the broader gravity track this is the residual half of the classical-recovery input to the unconditional master theorem's concrete physical Regge-EH continuum proposition. It does not touch the forcing chain (T5-T8) or the RCL; it is pure continuum-limit bookkeeping for Regge calculus on the six-tet cubic torus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.