hamDynLocalProfile
plain-language theorem explainer
Defines the honest local Hamiltonian density used by HamDyn on the CanonicalMom target: H(a,b,p)=(1/2)(p^{2}+(1+a^{2})(b−a)^{2}). Gravity and HKT-rigidity authors cite it as the concrete profile that inhabits the repaired point-split class. The body is a pure function definition, scaled by 1/2 so Fréchet derivatives match the const-mul calculus lemmas.
Claim. The honest HamDyn local profile is the map $H:\mathbb{R}^3\to\mathbb{R}$ given by $H(a,b,p)=\tfrac12\bigl(p^2+(1+a^2)(b-a)^2\bigr)$.
background
In the SevenGaps HKT stack, a local Hamiltonian profile is simply a real function of three scalars $(a,b,p)$: the two point-split field values and the conjugate momentum. The type LocalHamProfile is the abbreviation $\mathbb{R}\to\mathbb{R}\to\mathbb{R}\to\mathbb{R}$.
This module (Wave C2, gap5) repairs the CanonicalMom class after the strong point-split rigidity statement was killed by a balanced-quartic falsifier. Session B exhibits an honest HamDyn inhabitant of HKTPointSplitTargetDynCanonicalMom and banks a DEFINED-only rigidity statement for later sessions to prove.
The factor $1/2$ is deliberate: it aligns the Fréchet derivative data with HasFDerivAt.const_mul, so downstream smoothness and PDE lemmas can quote standard calculus without extra constants.
proof idea
Pure definition: the profile is the lambda $(a,b,p)\mapsto \tfrac12\bigl(p\cdot p+(1+a\cdot a)\cdot((b-a)\cdot(b-a))\bigr)$. No proof obligations; the scaling is chosen only for derivative bookkeeping.
why it matters
This is the concrete density that makes the honest HamDyn target inhabit the CanonicalMom class. Downstream it is the witness profile in hamDyn_solve_profile_FE_quadratic (the PDE Prop over CanonicalMom), and it feeds the gauge lemmas hamDyn_constantKineticSlope, hamDyn_constantVacuumGauge, hamDyn_HbPIndependent, hamDyn_HpLinearInP, plus ContDiff-2 smoothness (hamDynLocalProfile_contDiff2) and the density-equality bridge hamDynDensity_eq_localProfile.
Those facts package into the smooth-scoped rigidity data used to prove the repaired N=2 CanonicalMom rigidity statement. The module leaves gap5_constraint_recovery false: this definition supports the CanonicalMom route, not a flip of the ledger flag. It sits in the gravity/HKT branch of Recognition Science, separate from the T0–T8 forcing chain, but supplies the local energy density whose quadratic structure the rigidity PDEs exploit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.