LocalHamSmooth_hp_unique
plain-language theorem explainer
For a fixed local Hamiltonian profile, the momentum-slot field of any two smooth witnesses agrees at every configuration-momentum triple. HKT kinetic-normalized rigidity cites this so hp is profile-determined, not witness-dependent. The argument is Fréchet uniqueness of the local-cell derivative, then evaluation on the pure p-direction.
Claim. Fix a local Hamiltonian profile $h$. If $S_1$ and $S_2$ are any two $C^1$ witnesses for $h$, then for all real $a,b,p$ the momentum-slot partials agree: the $hp$ field of $S_1$ at $(a,b,p)$ equals that of $S_2$.
background
This module closes Wave C4/C5 gap5: mod-vacuum kill plus kinetic-normalized rigidity. A LocalHamProfile packages the local Hamiltonian density shape on a two-site cell; LocalHamSmooth is a $C^1$ witness supplying Fréchet data for that profile, including a momentum-slot field conventionally written $hp(a,b,p)$.
Phase points are built by fePhase: the cell $(q_0,q_1,\pi_0,\pi_1)=(a,b,p,r)$ in PhaseSpace 2. The local-cell map is Fréchet differentiable along each smooth witness (hasFDerivAt_localCell). The private evaluation lemma localCellD_eval_p0 identifies the derivative of that map, tested on the pure $\pi_0$-direction $(0,e_0)$, with the witness field $hp(a,b,p)$.
Uniqueness of Fréchet derivatives is the only analytic input: two derivatives of the same map at the same point must coincide as continuous linear maps.
proof idea
Form the phase point $x=\mathrm{fePhase}(a,b,p,0)$. Both smooth witnesses supply a Fréchet derivative of the local-cell functional at slot $0$ and point $x$ via hasFDerivAt_localCell. HasFDerivAt.unique equates those two continuous linear maps. Congruence evaluates both maps on the pure $p_0$-direction $(0,\mathrm{Pi.single},0,1)$. The evaluation lemma localCellD_eval_p0 rewrites each side as the corresponding $hp(a,b,p)$, and simpa finishes.
why it matters
The sole downstream consumer is vacuumKinetic_not_kineticNormalized, the load-bearing exclusion that the variable-kinetic vacuum counterexample is not kinetic-normalized: its $hp$ is not globally of the form $2 c_{\mathrm{Kin}} p$. Without witness-independence of $hp$, that comparison could depend on which smooth lift one chose.
In the gap5 ledger this is the Fréchet half of kinetic-normalized rigidity: intensivity and FTC recovery are theorem-derived for the normalized class, while the vacuum kinetic target is ruled out as an inhabitant. It sits under the C5 upgrade binding (D-gap5-acceptance-adjudication) after the mod-vacuum kill half. No T0–T8 landmark is directly invoked; the result is pure local analytic rigidity inside the HKT gravity sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.