module module moderate

`IndisputableMonolith.Gravity.SevenGaps.HKTKineticNormalizedRigidity`

Infrastructure for kinetic-normalized HKT CanonicalMom rigidity in the SevenGaps gravity campaign: vacuum kinetic profiles, Hamiltonian density, and kill theorems under a disclosed linear-in-momentum premise. Gap5 close-status and recognition-cost kinetic work import it. Mix of vacuum-sector definitions, ContDiff calculus, and explicit counterexamples that defeat unconditioned rigidity.

claimIn the HKT vacuum sector, define kinetic amplitudes $A$, weights $W$, and $K$, a local profile, and Hamiltonian density on phase data $(a,b,p)$. Under the disclosed premise $\partial_p H = 2 c_{\mathrm{Kin}}\, p$ with $c_{\mathrm{Kin}}\neq 0$, the kinetic-normalized CanonicalMom rigidity claim is set up and shown false in the vacuum-shift cases already killed upstream; supporting lemmas include positivity of $A$ and $1+x^2\neq 0$.

background

Gap5 of the SevenGaps gravity campaign concerns continuum-algebra HKT rigidity for CanonicalMom. Upstream, HKTCanonicalMomRigidityPDE fixes the analytic setting: $\mathrm{ContDiff},\mathbb{R},2$ of the local profile $\mathbb{R}^3\to\mathbb{R}$ is the standard HKT smoothness hypothesis (binding D-qg-hkt-rigidity-route). Upstream HKTVacuumSectorKill shows the unconditioned rigidity proposition is false: a vacuum-shift density at $n=2$ is an explicit killer (branch A gauge-scope adjudication).

This module re-scopes rigidity after that kill by normalizing the kinetic sector. It introduces vacuum kinetic objects $A$, $W$, $K$, a local profile, and Hamiltonian density, plus elementary $\mathbb{Z}/2\mathbb{Z}$ arithmetic and positivity facts ($A>0$, $1+x^2\neq 0$). The implementation note prefers inverses on $\mathbb{R}$ first because product-space inversion at top smoothness times out.

The disclosed constraint carried forward is linearity of the momentum derivative of the Hamiltonian: $\partial_p H = (2 c_{\mathrm{Kin}}) p$ with nonzero constant $c_{\mathrm{Kin}}$. That premise is what later pillars try to halve or derive from recognition cost.

proof idea

Not a single theorem: a definition-and-kill module. It builds vacuum kinetic $A$, $W$, $K$, equates $W$ to a design form, packages a local profile and Hamiltonian density, then records positivity and nonvanishing lemmas needed for normalized rigidity statements.

Argumentative spine imports the C2 ContDiff-2 PDE rigidity session and the C3 vacuum-sector kill. Kill theorems here instantiate the vacuum counterexample under the kinetic-normalized CanonicalMom packaging, so rigidity fails once the linear-$p$ Hamiltonian premise is fixed rather than left unconditioned. Calculus support comes from Mathlib ContDiff, Deriv, FDeriv, and mean-value imports; no deep new PDE proof lives in the module body beyond wiring those facts to the vacuum kinetic densities.

why it matters in Recognition Science

Closes the kinetic-normalized packaging of gap5 HKT rigidity after the vacuum kill, so downstream ledgers can flip status bits without re-opening unconditioned CanonicalMom claims. Gap5ConstraintCloseStatus imports it to bind fullTheoryBenchmarks.gap5_constraint_recovery = true, sevenGapsCampaignStatus.gap5_continuum_algebra_hkt_open = false, and gap5ResidualDAGStatus.hktRigidityOpen = false.

HKTKineticFromRecognitionCost treats this module's KineticNormalizedCanonicalMom as Pillar 1 work item 1: it carries the disclosed premise $S.hp,a,b,p = (2 c_{\mathrm{Kin}}) p$ with $c_{\mathrm{Kin}}\neq 0$, and cites four kill theorems here showing the rigidity conclusion is false under that premise, motivating derivation of the kinetic law from recognition cost rather than assumption. The audit module imports the same surface for bookkeeping.

In the broader RS gravity stack this is continuum HKT bookkeeping, not a T0–T8 forcing step; it keeps gap5 from claiming more rigidity than the vacuum sector allows.

scope and limits

Does not prove unconditioned CanonicalMom rigidity; vacuum kill already falsifies that form.
Does not derive $c_{\mathrm{Kin}}$ from recognition cost; that is deferred to HKTKineticFromRecognitionCost.
Does not close full gap5 alone; close-status and ledger Bool flips live downstream.
Does not establish ContDiff-2 of arbitrary HKT profiles; it consumes the C2 PDE session hypotheses.
Does not treat non-vacuum sectors or $n\neq 2$ shift densities as killers here.

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.HKTKineticFromRecognitionCost module_import
IndisputableMonolith.Gravity.SevenGaps.HKTKineticNormalizedRigidityAudit module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.HKTCanonicalMomRigidityPDE module_import
IndisputableMonolith.Gravity.SevenGaps.HKTVacuumSectorKill module_import

declarations in this module (85)

lemma zmod2_zero_add_one L36
lemma zmod2_one_add_one L37
lemma zmod2_zero_add_two L38
lemma zmod2_one_add_two L39
def vacuumKineticA L43
def vacuumKineticW L45
def vacuumKineticK L50
theorem vacuumKineticW_eq_design L54
def vacuumKineticLocalProfile L59
def vacuumKineticHamDensity L62
theorem one_add_sq_ne_zero L65
theorem vacuumKineticA_pos L68
theorem vacuumKineticA_ne_zero L71
theorem vacuumKineticW_diag L74
theorem vacuumKinetic_diag L77
def vacuumKineticHbClosed L81
def vacuumKineticHpClosed L84
theorem contDiff_vacuumKineticA L90
theorem contDiff_vacuumKinetic_kinTerm L97
theorem contDiff_vacuumKinetic_wTerm L105
theorem vacuumKinetic_profile_contDiff L111
theorem vacuumKineticLocalProfile_contDiff2 L119
theorem hasDerivAt_vacuumKinetic_p L125
theorem hasDerivAt_vacuumKineticK_b L144
theorem hasDerivAt_vacuumKineticW_b L182
theorem hasDerivAt_vacuumKinetic_b L199
def vacuumKineticLocalHa L214
def vacuumKineticLocalHb L218
def vacuumKineticLocalHp L222
theorem vacuumKineticLocalHp_eq_closed L226
theorem vacuumKineticLocalHb_eq_closed L239
theorem vacuumKinetic_FE L252
theorem vacuumKinetic_localCoeff_eq_structure_mom L265
def vacuumKineticCellCoords L278
def vacuumKineticCellCoordsD L281
lemma hasFDerivAt_vacuumKineticCellCoords L284
lemma hasFDerivAt_vacuumKineticLocalCell L289
def vacuumKineticLocalSmooth L340
def vacuumKineticHamAdvFrom L348
def vacuumKineticHamAdvTo L352
theorem vacuumKineticHam_eq_LocalHamFromProfile L356
theorem differentiable_vacuumKineticHam L361
theorem bracket_bilinear_basis_zmod2 L368
theorem mom_ham_split_vacuumKinetic L427
theorem ham_ham_vacuumKinetic L474
def vacuumKineticNondegPhase L487
theorem vacuumKinetic_nondeg L490
def vacuumKineticWeakTarget L496
theorem vacuumKinetic_kinetic_regular_witness L527
def vacuumKineticStrongTarget L554
theorem vacuumKineticDensity_eq_localProfile L568
def vacuumKineticCanonicalMomTarget L573
def coincidentPhaseKin L585
theorem not_HKTRigidityModVacuumStatementN2 L589
theorem vacuumKinetic_structure_nonconstant L620
theorem fe_diagonal_trivial L625
theorem vacuumKinetic_fails_modVacuum_hamShape L632
structure KineticNormalizedCanonicalMom L668
def HKTRigidityKineticNormalizedN2 L679
lemma localCellD_eval_p0 L694
lemma localCellD_eval_b0 L702
theorem LocalHamSmooth_hp_unique L712
theorem LocalHamSmooth_hb_unique L724
theorem hasDerivAt_profileMap_p L737
theorem hasDerivAt_profileMap_b L749
def cellCoords0 L761
def cellCoords0D L764
lemma hasFDerivAt_cellCoords0 L767
theorem cellCoords0_fePhase L773
theorem LocalHamSmooth_hp_eq_fderiv L777
theorem LocalHamSmooth_hb_eq_fderiv L813
theorem hasDerivAt_hp_of_normalized L850
theorem hasDerivAt_hb_of_normalized L857
theorem kinetic_split_of_intensivity L867
theorem hb0_of_intensivity_FE L897
theorem gradient_recovery_of_intensivity L918
theorem alternating_FE_of_profile L980
theorem ftc_recovery_of_normalized L1049
theorem HKTRigidityKineticNormalizedN2_holds L1079
def hamDynKineticNormalized L1109

… and 5 more