sqrtAffineProfile_contDiff2
plain-language theorem explainer
The square-root affine local Hamiltonian profile √(1+(b−a)²)·p is C² as a map ℝ³→ℝ. Anyone building the ContDiff-2 counterexample to forced linear-hp / p-free-hb ansatzes cites this smoothness certificate. The proof factors the profile into a strictly positive quadratic under a square root, multiplies by the momentum slot, and applies Mathlib ContDiff rules.
Claim. The local Hamiltonian profile $h(a,b,p)=\sqrt{1+(b-a)^2}\,p$ meets the ContDiff-2 smoothness obligation: the map $(a,b,p)\mapsto h(a,b,p)$ from $\mathbb{R}^3$ to $\mathbb{R}$ is twice continuously differentiable.
background
This module is Wave C2 gap5 of the HKT canonical-momentum rigidity route. The standard smoothness assumption for the local Hamiltonian is ContDiff-2 of the profile as a map $\mathbb{R}\times\mathbb{R}\times\mathbb{R}\to\mathbb{R}$. The obligation packages exactly that: a local profile $h$ satisfies it when $(a,b,p)\mapsto h(a,b,p)$ is $C^2$.
The square-root affine profile is the smooth witness $h(a,b,p)=\sqrt{1+(b-a)^2},p$. Its packaging as a triple map is the profile map. A supporting positivity lemma records that $1+(b-a)^2\neq 0$ everywhere, so the real square root is smooth on the image.
Upstream, the ContDiff-2 obligation was introduced because plain LocalHamSmooth identifies Frechet coefficients but does not license differentiating the functional equation in the momentum slot. Requiring $C^2$ of the profile (or an equivalent slotwise derivative package) is the re-scoped hypothesis before any $\partial/\partial r$ isolation step.
proof idea
Unfold the obligation to ContDiff ℝ 2 of the profile map. Build ContDiff ⊤ of the quadratic $t\mapsto 1+(t.2.1-t.1)^2$ from constants, projections, subtraction, and multiplication. Lift through Real.sqrt using the nowhere-zero lemma on $1+(b-a)^2$. Separately, the momentum projection $t\mapsto t.2.2$ is ContDiff ⊤. Identify the profile map with the product of those two maps by funext and rfl, then conclude ContDiff 2 of the product by of_le from ContDiff ⊤.
why it matters
This certificate is the smoothness half of the disclosed finding: ContDiff-2 alone does not force the linear-hp / p-free-hb ansatz used by the PDE route. Downstream, the two existence theorems not_forced_linear_hp_of_contDiff2_FE and not_forced_hb_p_independent_of_contDiff2_FE both demand the ContDiff-2 obligation on a witness; this theorem discharges it for the square-root affine profile, which satisfies the alternating FE with cMom=1 and g≡1 yet has momentum partial independent of p and b-partial linear in p.
The status aggregator hktCanonicalMomRigidityC2Status_flags records feAnsatzCounterexampleClosed = true on the strength of those findings. The unconditioned Prop solve_profile_FE_quadratic remains open; gap5_constraint_recovery must not be flipped. In the broader SevenGaps gravity stack this is honest scope correction on the HKT rigidity PDE path, not a closure of canonical-momentum rigidity itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.