function
plain-language theorem explainer
Definitional structure packaging a field-independent momentum response φ (with φ(0)=0) for the HKT kinetic half-premise reduction. Gravity and cost-algebra developments cite it when collapsing “linear in p with constant coefficient” to mere field-independence. No proof body: it is a data carrier, not a theorem.
Claim. A structure recording a momentum response $\varphi$ with $\varphi(0)=0$ such that the canonical momentum density takes the field-independent form $S_{hp}(a,b,p)=\varphi(p)$. Under the ambient point-split functional equation on canonical-momentum targets, this is the data from which linearity of $\varphi$ (nonzero constant coefficient) is forced.
background
Module setting is Pillar 1 work item 1: halving the disclosed premise of KineticNormalizedCanonicalMom. That premise asserted both linearity in momentum and field-independence of the coefficient,
$$S.hp,a,b,p=(2,c_{\mathrm{Kin}}),p,\qquad c_{\mathrm{Kin}}\neq 0.$$
Four kill theorems in the sibling rigidity module show the conclusion fails without that load. Here one keeps only field-independence plus vanishing at zero momentum, $S.hp,a,b,p=\varphi(p)$ with $\varphi(0)=0$.
The ambient CanonicalMom axioms include a point-split functional equation separately linear in each momentum slot. Recognition cost (J-cost, RCL, T5 uniqueness) is deliberately not an input: the module states that nothing about recognition enters the linearity forcing. Upstream cost infrastructure (functional equation, convexity, symplectic action) supplies the algebraic skeleton; the forcing chain’s D=3 / eight-tick material is ambient context only.
proof idea
Definitional structure: no proof tactics and no term-mode argument. It declares the carrier for the universal (field-independent) momentum response used by the surrounding lemmas.
Those lemmas do the work: the point-split equation evaluated at a free pair such as $(a_0,a_0+1)$ produces a nonzero denominator (vanishing would give $0=c_{\mathrm{Mom}}\cdot g(a_0)\cdot r$, false at $r=1$), so a response that cannot hide field dependence cannot hide nonlinearity either. The structure simply names the $\varphi$ slot those arguments act on.
why it matters
Earns its place as the reduced load-bearing surface of the HKT kinetic premise: field-independence alone, not an a-priori linear ansatz. Parent results in this module lift it to full kinetic normalization (kinetic_normalization_of_universal_response, the UniversalKineticCanonicalMom ↔ normalized equivalence) and record the restatement as channel separation $h=K(p)+U(a,b)$ with $K$ stationary at zero momentum.
Downstream, action/Hamiltonian energy and admissible-path machinery, together with CostAlgebraData (RCL cost carrier), consume the same kinetic/cost interface. Framework landmark contact is indirect: channel separation is the two-channel shadow of additive posting $\Phi(x)=\sum_i J(x_i)$ from the J-Hessian story; whether momentum and spatial link are distinct ledger channels remains an open item explicitly deferred by the module doc. No T0–T8 step is discharged here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.