kinetic_coefficient_unique
plain-language theorem explainer
Any two real constants that both present the same local Hamiltonian momentum response as a pure multiple of momentum must coincide. Gravity workers reducing the HKT kinetic-normalization premise cite this uniqueness step. The proof evaluates both presentations at a single test point and finishes by linear arithmetic.
Claim. Let $h$ be a local Hamiltonian density profile and $S$ a smooth structure on $h$. If constants $c_1,c_2\in\mathbb{R}$ both satisfy $S.hp(a,b,p)=(2c_i)\,p$ for all field values $a,b$ and momentum $p$, then $c_1=c_2$.
background
The ambient setting is Pillar 1 work item 1: halving the disclosed kinetic premise on HKT targets. A LocalHamProfile is a real ternary density $h(a,b,p)$. A LocalHamSmooth structure packages the three partials of $h$, written $ha$, $hb$, $hp$, together with a cellwise Fréchet-differentiability witness on the two-phase space.
The load-bearing disclosed premise in the sibling rigidity module asserts that the momentum response is linear and field-independent, $$S.hp,a,b,p=(2,c_{\mathrm{Kin}}),p\quad(c_{\mathrm{Kin}}\neq 0).$$ Section 2 of this module shows that field-independence plus vanishing at zero momentum already forces linearity, via the point-split functional equation on every canonical-momentum target. Once linearity is forced, the coefficient itself must be unique; that is the present claim.
No recognition-cost input is used here. The argument lives entirely inside the local Hamiltonian calculus and the ambient canonical-momentum axioms.
proof idea
Instantiate both universal equalities at the single test point $(a,b,p)=(0,0,1)$. The two right-hand sides become $2c_1$ and $2c_2$, so the left-hand sides (identical values of $S.hp$) yield $2c_1=2c_2$. Close by linarith. No lemmas beyond the two hypotheses are required; the argument is pure point evaluation plus linear arithmetic.
why it matters
Uniqueness is the bookkeeping step that makes the kinetic coefficient a well-defined invariant of a universal-response target, rather than an artifact of the readout point. It underwrites the equivalence of the two model classes recorded immediately below: every universal-response target is kinetic-normalized, and conversely, so Section 2 is an equivalence rather than an enlargement of the model class.
Downstream, the same coefficient language appears in the jet-cost counterexample jetCost_not_rcl, which shows that a calibrated jet family still violates the Recognition Composition Law. That negative result is why Section 7 cannot carry the load and Section 8 must impose the composition law itself. Within the broader RS gravity stack, the theorem is local infrastructure for the HKT kinetic channel; it does not yet touch the open question whether momentum and spatial link are distinct ledger channels under additive posting of $J$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.