LocalHamSmoothContDiff2Obligation
plain-language theorem explainer
Defines the C² smoothness obligation on a local Hamiltonian profile: the map (t₁,t₂,t₃) ↦ h(t₁,t₂,t₃) must be ContDiff of order 2 on ℝ³. Cited by the CanonicalMom rigidity PDE session whenever ∂/∂r isolation of the alternating functional equation is needed. Pure definitional Prop packaging Mathlib ContDiff; no proof content.
Claim. For a local Hamiltonian profile $h:\mathbb{R}\times\mathbb{R}\times\mathbb{R}\to\mathbb{R}$, the C² obligation holds when the joint map $(t_1,t_2,t_3)\mapsto h(t_1,t_2,t_3)$ is twice continuously Fréchet differentiable over $\mathbb{R}$.
background
In the HKT CanonicalMom rigidity route (gap 5, session C1), the alternating functional equation is extracted from the ham-ham identity at $n=2$ under local, structure, and canonical profile ansätze. The weaker class LocalHamSmooth only recovers the phase-space Fréchet coefficients $h_a$, $h_b$, $h_p$ of $h\circ\mathrm{coords}$; it does not make those coefficient maps differentiable as functions of a single real slot.
Differentiating the alternating FE in the momentum coordinate $r$ is therefore unlicensed on that class alone. This definition re-scopes the hypothesis: demand joint $C^2$ regularity of the profile as a map $\mathbb{R}^3\to\mathbb{R}$ (equivalently, a slotwise HasDerivAt package) before any $\partial/\partial r$ isolation step.
The surrounding module lands the complete alternating FE, algebraic PDE sub-lemmas, and an assembly skeleton for later rigidity; it deliberately does not flip gap-5 constraint recovery or claim the full point-split dynamical uniqueness theorem.
proof idea
Definitional abbreviation only. The body is the Mathlib predicate ContDiff ℝ 2 applied to the uncurried profile map fun t : ℝ × ℝ × ℝ => h t.1 t.2.1 t.2.2. No tactics, no lemmas, no reduction.
why it matters
This Prop is the smoothness gate for the CanonicalMom PDE core. Downstream, LocalHamSmoothContDiff2Obligation_iff equates it with ContDiff of the profile map; concrete profiles discharge it (hamDynLocalProfile_contDiff2, sqrtAffineProfile_contDiff2, vacuumKineticLocalProfile_contDiff2). The package SmoothScopedCanonicalMomData bundles it with the linear ansatz and gauges for rigidity assembly.
Equally important are the negative findings it enables: ContDiff-2 plus the alternating FE do not force p-independence of $h_b$, nor a linear-$h_p$ ansatz (not_forced_hb_p_independent_of_contDiff2_FE, not_forced_linear_hp_of_contDiff2_FE). Those counterexamples pin the remaining wall: smoothness alone is insufficient; the linear/momentum-independent ansätze must be imposed separately before the algebraic core can force the gradient coupling $h_b(a,b)\cdot\mathrm{kinCoeff}(b,a)=c_{\mathrm{Mom}}\cdot(b-a)\cdot g(a)$.
Sits inside the gravity seven-gaps program toward HKT rigidity; does not yet close gap 5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.