Pith. sign in
module module high

IndisputableMonolith.Gravity.SevenGaps.DiracAlgebraContinuum

show as:
view Lean formalization →

Defines continuum momentum-flux density D(t)=p(t)·q'(t) and the sampling mesh that turns the dynamic lattice Dirac bracket into a quadrature-ready continuum object. Gravity workers on the Seven Gaps residual DAG cite the continuum densities, Wronskian, and sampledDynamicBracketSum. The module banks mesh bounds and norm controls so the rate-h shape theorems can pass to the continuum limit.

claimOn continuum phase data $(q,p)$, the momentum-flux density is $D(t)=p(t)\cdot q'(t)$. The continuum Dirac density and continuum Wronskian package the flux against the dynamic structure profile. On a mesh of step $h\in(0,1]$, the sampled dynamic bracket sum is the Riemann sum of that density, ready for the quadrature limit.

background

This module sits in the QG Seven Gaps campaign (Pillar 1, constraint algebra), Wave C2 residual R4: the continuum shape of the dynamic Dirac bracket. Upstream, WeightedHypersurfaceBracket generalizes the frozen hypersurface deformation theorem to a fixed background weight $w$ in the stiffness slot. DynamicStructureBracket closes R0+R1 on two sites: the naive frozen partials fail once $g$ depends on $q$, so the bracket must carry dynamic structure functions.

DynamicStructureContinuumSmearing extends fixed-background continuum reach so the structure profile is induced by a continuum field $q$ via $G(x)=1+(q x)^2$, matching the lattice law. QuadratureLimit supplies the Phase 2a toolkit: hinge sums converge to continuum integrals, axiom-clean.

Local objects are the continuum momentum-flux $D(t)=p\cdot q'$, the continuum Dirac density built from it, the continuum Wronskian, and a unit-interval mesh of step $h$ with membership and norm-bound lemmas for sampling.

proof idea

Definition-and-lemma module, not a single theorem. It introduces continuumMomentumFlux, continuumDiracDensity, continuumWronskian, and sampledDynamicBracketSum as the freestanding Riemann shape of the dynamic bracket. Mesh infrastructure (mesh_step, mesh_lt, mesh_le_one, mesh_nonneg, sample_mem_Icc, Ioo_mesh_subset_Icc, exists_norm_bound_on_Icc) supplies the elementary interval and bound facts needed to feed QuadratureLimit. No deep tactic proof lives here; the content is the continuum packaging that Binding and Audit later attach to HamDynN.

why it matters in Recognition Science

Feeds three parents. DiracAlgebraContinuumBinding binds the freestanding Riemann shape sampledDynamicBracketSum to the genuine lattice bracket of HamDynN after periodic wrap treatment, then lands the ledger terminal dirac_algebra_continuum_limit for 1-periodic C¹ data. DiracAlgebraContinuumAudit runs the axiom audit on the real rate-h / shape theorems (ledger name held free pending HamDynN binding repair; headline theorems must print within propext, Classical.choice, Quot.sound). Gap5ConstraintResidualDAG names residuals for dynamic Dirac structure functions and HKT rigidity under gap5_constraint_recovery.

In the campaign plan this is Wave C2 R4: continuum limit of the dynamic structure-function bracket, the continuum counterpart of the lattice Dirac algebra that recovers the hypersurface deformation algebra with dynamic weights.

scope and limits

used by (3)

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

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (25)