flattenSlice
plain-language theorem explainer
Flattening a D2 quadrature slice keeps lattice sizes, local correspondence, cell volumes, and spacing schedules fixed, while every tetrahedron conformal probe is replaced by the zero potential. Gravity analysts use it to build the unconditional flat sector of the D2 reduction. The body is a pure structure copy that installs zeroPotential on the canonical encoded periodic Freudenthal torus.
Claim. Given a canonical periodic tet-six-tet volume quadrature slice $S$ along a filter $\ell$, the flattened slice has the same cardinalities $N_x,N_y,N_z$, the same local lattice correspondence, and the same cell-volume and spacing schedules as $S$, but every tetrahedron probe equals the zero conformal potential on the canonical encoded periodic Freudenthal torus of $S$.
background
This module sits on top of the damped-schedule closure for the D2 reduction of the nonlinear Regge aggregate. After residual damping is discharged, the remaining analytic input is the cross-cardinality quadrature limit. The module splits that input into a flat sector (closed unconditionally) and a curved sector (reduced to a scalar Dirichlet limit).
A quadrature slice packages lattice sizes $N_x,N_y,N_z$, a local lattice-manifold correspondence, cell-volume and spacing schedules along a filter, and a family of tetrahedron conformal probes. The zero conformal potential on a 3D triangulation is the vertex function that is identically zero. The canonical encoded periodic Freudenthal torus supplies the triangulation $K$ on which that potential is evaluated.
Flattening is the operation that freezes every geometric schedule and replaces every probe by that zero potential. Downstream, the canonical Dirichlet energy of the zero potential vanishes, so the flattened quadrature proxy is exactly zero.
proof idea
Definitional structure copy, not a proof. All cardinality, instance, inequality, local-correspondence, cell-volume, and spacing fields are taken verbatim from the input slice. The data record keeps the same limit cell volume, cell-volume schedule and its tendsto, and spacing schedule with its two spacing hypotheses. Only tetProbe changes: for every index it returns zeroPotential on the triangulation $K$ of canonicalEncodedPeriodicFreudenthalTorus built from the slice's sizes and edge lengths. NeZero instances are reintroduced locally so that torus constructor typechecks.
why it matters
This is the atomic flat-sector constructor for D2. flatFamily applies it pointwise to every slice of a refinement family, and flattenSlice_quadratureIntegral proves the flattened proxy equals zero because the canonical Dirichlet energy of the zero potential vanishes. Together they make the quadrature target hold at the flat continuum integral $0$ with no extra hypothesis.
Combined with the already-closed damped residual, that yields dampedFlat_fullReggeProduct_tendsto_zero: the full nonlinear Regge aggregate of the damped flat family converges to the flat Einstein-Hilbert value on the product filter. The resulting dampedFlatProductFilterData is the first D2 master datum whose both analytic fields are theorems, consuming only Track 1.B local-correspondence data carried by every slice.
The curved sector remains open: genuine curvature-bearing probes still need the scalar Dirichlet Riemann-sum limit. Flattening isolates that open content by giving a fully closed comparison case.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.