D2QuadratureConvergenceTarget
plain-language theorem explainer
Names the first open analytic target of the D2 Regge-to-Einstein-Hilbert audit: a varying-cardinality six-tet quadrature family must tend to a fixed continuum EH/Dirichlet integral along a refinement filter. Anyone citing the D2 reduction or the damped-schedule closure uses this Prop as the remaining quadrature hypothesis. The body is a pure abbreviation of the cross-cardinality Tendsto target already defined on the physical six-tet instance.
Claim. For a base filter $\ell$ on index type $\alpha$, a refinement-parameter type $\rho$, a varying-cardinality family $F$ of canonical periodic six-tet volume-quadrature slices along $\ell$, a refinement filter $\mathcal{R}$ on $\rho$, and a real continuum integral $I$, the named target asserts that the finite six-tet quadrature proxies of $F$ converge to $I$ along the cross-cardinality product schedule determined by $\mathcal{R}$.
background
The D2 classical-recovery witness in the master theorem asks that every product-filter datum on the canonical periodic six-tet cubic torus satisfy full nonlinear Regge-to-continuum EH convergence. That datum carries two analytic fields: quadrature convergence of the six-tet rule to the continuum EH/Dirichlet integral, and uniform control of the (full nonlinear Regge minus quadrature) residual. The genuine theorem is only the triangle-inequality squeeze that combines those two inputs.
A varying-cardinality refinement family is a map from a refinement parameter to finite six-tet quadrature slices. The cross-cardinality target compares those slice proxies to a fixed continuum integral along a refinement filter, as a Tendsto statement (not a triviality). This module's job is to name that first remaining target explicitly so it is not buried inside a structure field.
Upstream, the physical six-tet cubic Dirichlet instance already packages the slice family and the cross-cardinality Tendsto Prop; the continuum bridge identifies discrete Laplacian/hinge action with continuum Dirichlet energy. The audit therefore reduces D2 to geometry-level analysis rather than claiming a from-primitives closure.
proof idea
No proof content: the declaration is a definitional abbreviation. It sets the named D2 quadrature-convergence Prop equal to the existing cross-cardinality finite-to-integral target on a canonical periodic six-tet volume-quadrature refinement family, passing through the same refinement filter and continuum integral. Downstream proofs simply unfold or apply this alias when they need the audit vocabulary.
why it matters
This is Remaining Target 1 in the honest D2 scoping audit: the open frontier item that must still be discharged from primitive mesh geometry for a full from-primitives D2 closure. The reduction theorem in this module states that quadrature convergence plus residual vanishing imply full product-filter Regge-to-EH convergence; this Prop is the first conjunct of that reduction.
Downstream, the damped-schedule closure reduces full D2 further to quadrature alone (damping derives the residual), and the flat-sector instances discharge the target at continuum value $0$ with no hypothesis. The scalar Dirichlet energy-limit implication also lands here: if graph-Dirichlet energies tied to the quadrature proxies converge, this target holds. In the Recognition gravity stack this is the named analytic gate between discrete Regge calculus on the six-tet cubic torus and continuum Einstein-Hilbert recovery, not a forcing-chain (T0-T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.