module module moderate

`IndisputableMonolith.Gravity.SevenGaps.HKTCanonicalMomTarget`

Defines the canonical-momentum HKT target at lattice size n = 2: structure density of shape 1 + q_j^2 together with quartic-balanced Hamiltonian and momentum densities and the MomBalanced predicate. Gravity and continuum-algebra workers cite it as the concrete model class for gap-5 rigidity. The module is definitional scaffolding plus elementary ZMod-2 and balance lemmas, not a rigidity proof.

claimAt $n=2$, fix the structure profile $s_j = 1 + q_j^2$ and the quartic-balanced Hamiltonian and momentum densities built from bulk and momentum profile factors. Declare the balanced-momentum predicate on those densities, and record the elementary $\mathbb{Z}/2\mathbb{Z}$ arithmetic and balance identities needed to feed the local functional equation and point-split targets.

background

Gap 5 of the Seven Gaps gravity campaign asks for continuum-algebra / HKT rigidity of the discrete Hamiltonian–momentum package. Upstream, the strengthened point-split target excludes decoy zero-momentum quartics and ties advection to load-bearing momentum; the local-profile functional equation at $n=2$ reduces the dynamical ham_ham identity for local profiles to a product form $\mathrm{momDensity}_j = h_b(j), h_p(j+1)$. The full-theory ledger tracks when those pillars flip to machine-checked true.

This module supplies the concrete model side of that attack: a structure density of the same shape as the dynamical structure profile, namely $1+q_j^2$, together with quartic-balanced Hamiltonian density, momentum density, advection legs, and momentum-bracket density at $n=2$. The named balance predicate packages the algebraic relation those densities must satisfy before rigidity or functional-equation extraction can begin.

Notation is lattice-local: indices run in $\mathbb{Z}/2\mathbb{Z}$ at $n=2$, and the small arithmetic lemmas (zero-plus-one, one-plus-one, successor inequality) are bookkeeping for that period-2 setting.

proof idea

Definition module with supporting lemmas, not a rigidity theorem. It introduces the structure and density constructors (quartic-balanced ham/mom/advection/bracket forms at $n=2$), the MomBalanced predicate, and a balance identity relating them. The only proofs are elementary: $\mathbb{Z}/2\mathbb{Z}$ addition facts and the algebraic check that the quartic-balanced package satisfies the balance relation. No functional equation is solved here; that work is deferred to the rigidity session that imports this target.

why it matters in Recognition Science

Canonical-momentum rigidity (Wave C2 gap5, design route D-qg-hkt-rigidity-route-20260722) imports this module as the model class on which the alternating functional equation from ham_ham plus local/structure/canonical profiles is extracted. The audit module and the gap-5 constraint-recovery close status also depend on it, so ledger flips for gap5_constraint_recovery, continuum-algebra HKT open, and HKT rigidity open are gated on a well-typed target rather than an ad-hoc density package.

In the broader Recognition gravity stack this is the n=2 groundwork that lets the strengthened point-split and local FE modules talk to a single balanced momentum model, instead of a decoy-inhabitable weak class. It does not itself close gap 5; it is the named target those closers act on.

scope and limits

Does not prove HKT or continuum-algebra rigidity of the canonical-momentum class.
Does not solve the local or alternating functional equation; only defines densities and balance.
Does not exclude decoys by itself; that is the job of the strong point-split target upstream.
Does not flip full-theory or seven-gaps ledger flags; downstream status modules bind those.
Restricted to n = 2 quartic-balanced profiles; no general-n or continuum limit claim.

used by (3)

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

IndisputableMonolith.Gravity.SevenGaps.Gap5ConstraintCloseStatus module_import
IndisputableMonolith.Gravity.SevenGaps.HKTCanonicalMomRigidity module_import
IndisputableMonolith.Gravity.SevenGaps.HKTCanonicalMomTargetAudit module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.FullTheoryLedger module_import
IndisputableMonolith.Gravity.SevenGaps.HKTLocalFunctionalEquation module_import
IndisputableMonolith.Gravity.SevenGaps.HKTPointSplitStrong module_import

declarations in this module (53)

lemma zmod2_zero_add_one L33
lemma zmod2_one_add_one L34
lemma zmod2_succ_ne L35
def quarticBalancedStructure2 L41
def quarticBalancedHamDensity2 L45
def quarticBalancedMomDensity2 L51
def quarticBalancedHamAdvFrom2 L56
def quarticBalancedHamAdvTo2 L61
def quarticBalancedMomBracketDensity2 L67
def quarticBalancedHam2 L72
def MomBalanced L75
theorem quarticBalanced_balance L78
theorem MomBalanced_closed L85
def MomBalancedD L95
lemma hasFDerivAt_MomBalanced L102
theorem differentiable_MomBalanced L123
theorem pderivQ_MomBalanced L127
theorem pderivP_MomBalanced L135
theorem bracket_MomBalanced_MomBalanced L143
theorem bracket_MomBalanced_quarticHam L176
theorem bracket_quarticBalancedHam_quarticBalancedHam L235
theorem quarticBalancedStructure2_not_constant L246
def quarticBalancedNondegPhase L253
theorem quarticBalancedHamDensity2_nondeg L256
def quarticBalancedLoadPhase L262
theorem quarticBalanced_mom_load_bearing_witness L266
theorem quarticBalanced_kinetic_regular_witness L286
def quarticBalancedWeakTarget L307
def quarticBalancedStrongTarget L381
def constConfigPhase L396
theorem not_HKTRigidityStatementPointSplitDynN2Strong L401
structure HKTPointSplitTargetDynCanonicalMom L429
def hamDynLocalProfile L445
def hamDynLocalHa L449
def hamDynLocalHb L452
def hamDynLocalHp L455
def hamDynLocalCellD L460
lemma hamDynLocalCellD_eq_profilePartials L469
lemma hasFDerivAt_hamDynLocalCell_raw L483
lemma hasFDerivAt_hamDynLocalCell L511
def hamDynLocalSmooth L521
theorem hamDynDensity_eq_localProfile L527
theorem structureDyn_eq_g L532
theorem momDynDensity_canonical L537
def hamDynPointSplitTargetCanonicalMom L543
theorem hktPointSplitTargetDynCanonicalMom_nonvacuous L554
def canonicalMomSepPhase L560
theorem quarticBalanced_fails_canonical_mom L563
theorem canonicalMom_excludes_balanced_quartic L576
def HKTRigidityStatementPointSplitDynN2Canonical L611
structure HKTCanonicalMomStatus L628
def hktCanonicalMomStatus L638
theorem hktCanonicalMomStatus_flags L644