hamDynLocalProfile_contDiff2
plain-language theorem explainer
The honest HamDyn local Hamiltonian density is twice continuously differentiable as a real map on phase space (a,b,p). Gravity and HKT-rigidity authors cite it to discharge the ContDiff-2 packaging obligation for the ADM anchor profile. The proof is an explicit algebraic ContDiff construction: projections, products, and sums yield C^∞ of the quadratic polynomial, then of_le downgrades to C².
Claim. The honest HamDyn local profile $h(a,b,p) = \frac12\bigl(p^2 + (1+a^2)(b-a)^2\bigr)$ satisfies the ContDiff-2 obligation: the map $(a,b,p)\mapsto h(a,b,p)$ from $\mathbb{R}^3$ to $\mathbb{R}$ is $C^2$.
background
This module is the Wave C2 gap5 session on CanonicalMom rigidity under a ContDiff-2 hypothesis (binding D-qg-hkt-rigidity-route, re-scope N-qg-hkt-localham-contdiff2). The standard HKT smoothness package LocalHamSmooth only identifies Frechet coefficients of the profile; it does not license differentiating those coefficients as maps on $\mathbb{R}$. The ContDiff-2 obligation therefore asks that the local profile, viewed as a single map $\mathbb{R}\times\mathbb{R}\times\mathbb{R}\to\mathbb{R}$, be $C^2$ before any $\partial/\partial r$ isolation step in the PDE route.
The honest HamDyn density is the concrete ADM anchor
$h(a,b,p)=\frac12\bigl(p^2+(1+a^2)(b-a)^2\bigr)$,
written with the factor $1/2$ so Frechet data match HasFDerivAt.const_mul. Packaging it as a triple map is the sibling profileMap. Module finding: ContDiff-2 alone does not force the linear-$h_p$ / $p$-free-$h_b$ ansatz; the smooth counterexample sqrtAffineProfile satisfies the alternating FE yet violates that ansatz. The unconditioned quadratic FE solve therefore stays open.
proof idea
Unfold the obligation to ContDiff ℝ 2 (profileMap hamDynLocalProfile). Build $C^\infty$ of the three coordinate projections on $\mathbb{R}\times\mathbb{R}\times\mathbb{R}$ via contDiff_fst and contDiff_snd. Close under multiplication and addition to get $C^\infty$ of $p^2$, of $1+a^2$, of $(b-a)^2$, and of their structured sum. Scale by the constant $1/2$ with contDiff_const.mul. A funext/rfl identity equates profileMap hamDynLocalProfile to that explicit polynomial. Rewrite and apply ContDiff.of_le (top $\ge 2$) to finish. No external lemmas beyond Mathlib ContDiff algebra and the profile definition.
why it matters
Discharges the ContDiff-2 half of the "honest HamDyn ContDiff-2 + ansatz" landing listed in the module finding. Downstream, it is the smoothness witness inside hamDynSmoothScopedData (smooth-scoped rigidity data for the HamDyn point-split target), and it is passed verbatim into the nonempty-class certificates hamDynCalibratedJet, hamDynRCLKinetic, and hamDynKineticNormalized. Those certificates show that calibrated-jet, RCL-kinetic, and kinetic-normalized CanonicalMom rigidity classes are inhabited by the ADM anchor, so the corresponding rigidity theorems are not vacuous.
It also feeds the status flag theorem hktCanonicalMomRigidityC2Status_flags, which records smooth-scoped rigidity closed while leaving the unconditioned PDE lemma and full CanonicalMom rigidity open. Framework role: local gravity/HKT side of the Recognition cost ladder; the kinetic term is the recognition jet at unit chart weight. Does not flip gap5_constraint_recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.