flatFamily
plain-language theorem explainer
Pointwise flattening of a canonical six-tet volume quadrature refinement family: every tetrahedron probe is replaced by the zero potential. Anyone citing the unconditional flat-sector D2 closure (quadrature target at the continuum value 0) builds on this object. The body is a one-field structure update applying flattenSlice to each slice.
Claim. Given a canonical periodic six-tet volume quadrature refinement family $F$ indexed along a filter $\ell$, form a new family of the same type whose slice at each refinement index $r$ is the zero-potential flattening of $F$'s slice at $r$.
background
This module sits on top of the damped-schedule closure for the D2 reduction of discrete Regge gravity to continuum Einstein-Hilbert. The remaining analytic input is a cross-cardinality quadrature limit: proxies built from tetrahedron probes must tend to the continuum integral along refinement.
A CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily packages, for each refinement index, a periodic six-tet cubic Dirichlet instance together with Track 1.B local-correspondence data. The sibling flattenSlice replaces every tetrahedron probe by the zero potential. Canonical Dirichlet energy of the zero potential vanishes, so flattened quadrature proxies are identically zero.
The module's first goal is the flat sector: after flattening, the quadrature target holds at continuum value $0$ with no hypothesis, and combining with damped residual closure yields full nonlinear Regge product-filter convergence to $0$.
proof idea
Definition, not a proof. The structure is rebuilt with the same ambient types and filter; only the slice field changes, set to fun r => flattenSlice (F.slice r). All other fields of the refinement-family structure are inherited from $F$ by the where elaboration.
why it matters
This is the construction that makes the flat sector of D2 close unconditionally. Downstream, flatFamily_quadrature_target shows the flattened family's quadrature proxies are identically zero, hence tend to the flat Einstein-Hilbert value $0$ along every refinement filter, with no analytic hypothesis. That feeds d2_quadrature_target_flat (audit vocabulary) and, with the damped-schedule residual theorem, dampedFlat_fullReggeProduct_tendsto_zero and the packaged master datum dampedFlatProductFilterData whose quadrature and residual fields are both theorems.
The one-statement summary d2_flat_sector_one_statement cites this family as the object on which flat-sector D2 is closed end to end. Scalar-limit variants in D2ScalarDirichletQuadratureLimit recover the same product-filter convergence via the Dirichlet route. The curved sector remains open: genuine Riemann-sum content for curvature-bearing probes is not settled by flattening.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.