Pith. sign in
module module high

IndisputableMonolith.Gravity.SevenGaps.Gap5ConstraintResidualDAG

show as:
view Lean formalization →

Residual DAG module for Gap 5 of the Seven Gaps gravity campaign. It packages typed residuals for background-weight underdetermination, dynamic structure brackets, continuum smearing, Dirac-algebra continuum limits, and HKT rigidity/one-site falsification. Downstream close-status and full-theory ledger flips import this graph. Structure is a named residual inventory bound to upstream Wave C2 proofs, not a single new theorem.

claimGap 5 residual DAG: a certified inventory of typed residuals for constraint recovery, covering (i) background-weight underdetermination of the structure function in the Dirac bracket, (ii) dynamic two-site structure brackets with $G(x)=1+(q x)^2$, (iii) continuum smearing and rate-$h$ bracket-shape limits, (iv) binding of sampled dynamic brackets to lattice $\mathrm{HamDynN}$ brackets, and (v) HKT rigidity versus one-site counterexamples.

background

Gap 5 in the Seven Gaps QG campaign is continuum constraint algebra and HKT-style rigidity: recovering a Dirac hypersurface-deformation algebra whose structure functions depend on the canonical metric data, not on a frozen background weight.

Upstream modules supply the pieces. The dynamic structure-function blocker records that bracket_HamW_HamW and its continuum smear keep the weight fixed while phase space varies, whereas full ADM needs the inverse spatial metric in that slot. DynamicStructureBracket closes the R0 decoy (naive reuse of frozen HamW partials fails by an uncompensated $\partial g/\partial q$) and the genuine two-site dynamic bracket. Continuum smearing extends fixed-background reach so $G$ is induced by a continuum profile $q$. DiracAlgebraContinuum and its binding land the sampled-lapse Wronskian rate-$h$ residual and bind freestanding Riemann shapes to lattice brackets after periodic wrap, yielding the ledger terminal for 1-periodic $C^1$ data. HKT modules supply dynamic targets and one-site counterexamples.

This module does not re-prove those facts; it names them as typed residuals in one DAG for Gap 5.

proof idea

Definition and status module, not a monolithic proof. It imports the Wave C2 residual stack (blocker, bracket, continuum smearing, Dirac continuum and binding, hypersurface deformation, HKT target and one-site counterexample, full-theory ledger) and exposes sibling TypedResidual_gap5_* nodes: background-weight blocker, dynamic bracket, phase-space-dependent Dirac, continuum smearing residual, dynamic bracket-shape continuum, Dirac-algebra continuum limit, HKT rigidity (frozen and live), one-site falsification, dyn-target defined, and the combined dynamic-Dirac-and-HKT residual. Each node points at an upstream certified statement or named open; the DAG is the argument structure for later close-status binding.

why it matters in Recognition Science

Parent consumer is Gap5ConstraintCloseStatus (Wave C5), which binds ledger flags so that fullTheoryBenchmarks.gap5_constraint_recovery = true, sevenGapsCampaignStatus.gap5_continuum_algebra_hkt_open = false, and gap5ResidualDAGStatus.hktRigidityOpen = false without import cycles through FullTheoryLedger. The module is the residual map that makes those Bool flips auditable: every Gap 5 claim is either a typed residual closed by an upstream theorem or an explicitly named open (HKT rigidity path). In the RS gravity campaign this is the bookkeeping layer between local Dirac/HKT mathematics and the master full-theory ledger, not a new physical law. Framework contact is constraint recovery for continuum gravity (structure functions, hypersurface deformations), downstream of the discrete eight-tick and $D=3$ forcing only insofar as the lattice models sit in that setting.

scope and limits

used by (1)

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

depends on (9)

Lean names referenced from this declaration's body.

declarations in this module (24)