LocalHamSmoothContDiff2Obligation_iff
plain-language theorem explainer
For any local Hamiltonian profile, the ContDiff-2 smoothness obligation is definitionally the same as twice continuous differentiability of its profile map on R^3. Anyone packaging HKT local-Ham smoothness under the ContDiff-2 route cites this. The proof is pure definitional reflexivity (Iff.rfl).
Claim. For every local Hamiltonian profile $h$, the ContDiff-2 smoothness obligation on $h$ holds if and only if the associated profile map $h\colon\mathbb{R}\times\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ is of class $C^{2}$ over $\mathbb{R}$.
background
This module is the Wave C2 gap-5 session on HKT canonical-momentum rigidity under a ContDiff-2 PDE route (binding D-qg-hkt-rigidity-route, re-scope N-qg-hkt-localham-contdiff2). The standard HKT smoothness assumption is that the local profile, viewed as a real function of three real arguments, is twice continuously differentiable.
A local Hamiltonian profile packages the local kinetic/potential data used by the HKT ansatz. The profile map sends such a profile to the concrete function $\mathbb{R}\times\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ on which calculus is performed. The ContDiff-2 obligation is the named Prop that records that smoothness demand in the gap-5 constraint stack.
The same module later exhibits a smooth FE witness (square-root affine profile) showing ContDiff-2 alone does not force the linear-$h_p$ / $p$-free-$h_b$ ansatz, so the unconditioned quadratic FE solve stays open.
proof idea
One-line term proof: Iff.rfl. The obligation is defined to be exactly ContDiff ℝ 2 (profileMap h), so the biconditional is definitional equality of propositions, not a nontrivial equivalence proof.
why it matters
This lands item (1) of the session finding: ContDiff-2 packaging via the named obligation. Downstream siblings use that packaging to state the FE counterexample (smooth witness satisfying the alternating FE with $c_{\mathrm{Mom}}=1$, $g\equiv 1$, yet non-linear momentum partials), the conditional ADM solve under the linear ansatz plus constant kinetic/vacuum gauges, and the smooth-scoped rigidity theorem. No used-by edges are recorded yet; the declaration is infrastructure for the gap-5 ContDiff-2 route rather than a physics endpoint.
It does not close gap-5 constraint recovery: the module header forbids flipping that flag. The open object remains the unconditioned Prop that would solve the profile FE quadratically without the linear ansatz.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.