Pith. sign in
module module moderate

IndisputableMonolith.Gravity.D2QuadratureInstances

show as:
view Lean formalization →

Constructs the flat (zero-potential) D2 quadrature instances used as the base sector of the product-filter analysis. Every tetrahedron probe is replaced by the zero potential while cardinality, local correspondence, cell volumes, and spacing schedules are held fixed. Gravity analysts cite it for the flat-sector one-statement and the damped flat Regge product limit. Arguments are explicit instance constructions plus filter and energy identities inherited from the damped-schedule closure.

claimOn a fixed D2 mesh, the flattened slice keeps the same cardinality, local correspondence, cell-volume schedule, and spacing schedule, and replaces every tetrahedron probe by the zero potential $\phi\equiv 0$. The associated flat family realizes the quadrature target with vanishing canonical Dirichlet energy, and the damped flat full Regge product tends to zero in the product filter.

background

D2 gravity work in Recognition Science tracks discrete Dirichlet-type energies on tetrahedral meshes and their continuum limits under product filters. The upstream module D2DampedScheduleClosure closes the second open analytic input of the D2 scoping audit: the uniform residual that used to be a supplied hypothesis field is now derived from the damped schedule, with theorem status and no RS-internal axioms.

This module builds the flat sector on that closed schedule. The flattened slice keeps mesh combinatorics and geometric schedules fixed and sets every probe potential to zero. Sibling constructions include the flat family, its quadrature integral, the identification of the D2 quadrature target on the flat sector, and the product-filter datum for the damped flat family. Canonical Dirichlet energy of the zero probe is identically zero, which anchors residual and limit statements.

proof idea

The module is a construction and identity layer, not a single deep existence proof. Flattened-slice and flat-family definitions copy cardinality, correspondence, volumes, and spacings, then substitute the zero potential. Energy and integral lemmas reduce by direct evaluation on the constant-zero probe (canonical Dirichlet energy vanishes; quadrature integrals of uniform probes collapse). Filter data for the damped flat product is assembled from the upstream damped-schedule closure and checked against the master quadrature target. The one-statement for the D2 flat sector packages these equalities; the tendsto-zero claim for the damped flat full Regge product follows by feeding that filter datum into the closed residual machinery.

why it matters in Recognition Science

Supplies the concrete flat-sector instances that the downstream module D2ScalarDirichletQuadratureLimit imports. That parent treats the curvature-bearing scalar Dirichlet limit as the remaining named open analytic input, while claiming theorem status for what is already closed. The flat sector is the base case against which nonzero probes and curvature residuals are measured: vanishing energy, exact quadrature target match, and damped product tending to zero give the reference limit before curvature-bearing analysis. In the broader gravity thread this is the zero rung of the D2 product-filter ladder, not a forcing-chain (T0–T8) step, but it is required scaffolding for any discrete-to-continuum Dirichlet claim in the RS gravity stack.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (12)