d2_target_is_convergence
plain-language theorem explainer
On any canonical periodic six-tet product-filter datum, the D2 physical Regge–EH target is definitionally the statement that the full nonlinear Regge aggregate tends to the continuum integral along the product filter. Gravity auditors cite it to show the master D2 witness is a real Tendsto claim, not a vacuous True. The proof is a one-line definitional equality (rfl).
Claim. For types $\alpha,\rho$, a filter $\ell$ on $\alpha$, and any canonical periodic six-tet volume-quadrature product-filter datum $D$ over $\ell$, the concrete physical Regge–Einstein–Hilbert product-filter target of $D$ equals the assertion that the full nonlinear Regge aggregate of $D$'s family tends, along the product of $D$'s refinement filter with $\ell$, to the neighborhood filter of $D$'s continuum integral.
background
The module is an honest scoping audit of classical recovery D2 (Regge calculus to continuum Einstein–Hilbert) inside the unconditional master theorem. The D2 witness consumed upstream is a universal quantification over canonical periodic six-tet cubic Dirichlet product-filter data: every such datum $D$ must satisfy a named physical target.
That target is not a placeholder. Reading the product-filter structure, $D$ carries two analytic hypothesis fields: quadrature convergence of the canonical periodic six-tet rule to the continuum EH/Dirichlet integral, and a uniform residual bound on the full nonlinear Regge minus quadrature difference. The genuine theorem that combines them is a triangle-inequality squeeze yielding full Regge product-filter convergence to the continuum integral.
This declaration isolates the meaning of the target itself: it is literally a Filter.Tendsto statement for the full nonlinear Regge aggregate, not True and not a restatement of the master conclusion. Spatial dimension $D=3$ (forced by T8) sits in the ambient geometry of the six-tet cubic torus, but is not re-proved here.
proof idea
Term-mode proof by rfl. Unfolding the definition of the concrete physical Regge–EH product-filter target on $D$ yields exactly the stated Filter.Tendsto of the full nonlinear Regge aggregate along the product of the refinement filter with the parameter filter, toward the neighborhoods of the continuum integral. No lemmas are applied; the equality is definitional.
why it matters
Peer-review findings on D2 asked that the classical-recovery witness not hide a real analytic claim inside a data structure or collapse it to True. This theorem answers that demand: the product-filter target is disclosed as genuine continuum convergence of the full nonlinear Regge aggregate.
It sits beside the module's reduction statement (quadrature convergence plus vanishing residual envelope imply full Regge→EH on the product filter) and the named remaining targets (quadrature convergence from primitive mesh geometry; residual vanishing). Those remain the open frontier; this result only pins what the target is.
In the broader RS gravity stack it keeps the master theorem's D2 hypothesis honest: classical recovery is a reduction to two analytic fields, not a from-primitives closure. No downstream consumers are recorded yet; the value is audit clarity for anyone reading the unconditional master path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.