LocalMomSmooth
plain-language theorem explainer
Smoothness package for a local nearest-neighbor momentum profile on the two-site lattice: three partial-profile maps plus a Fréchet derivative certificate for each cell map. HKT/gravity workers cite it when assembling smeared momentum functionals and evaluating Poisson brackets against the Hamiltonian. Pure structure definition bundling Frechet cell data; no proof body.
Claim. A smoothness package for a local momentum profile $f:\mathbb{R}^3\to\mathbb{R}$ consists of three profiles $f_d,f_p,f_r$ and the assertion that for every site $j\in\mathbb{Z}/2\mathbb{Z}$ and phase-space point $x$, the cell map $y\mapsto f(q_{j+1}-q_j,\pi_j,\pi_{j+1})$ is Fréchet differentiable at $x$ with derivative $f_d\cdot(dq_{j+1}-dq_j)+f_p\cdot d\pi_j+f_r\cdot d\pi_{j+1}$, coefficients evaluated on the cell arguments of $x$.
background
The ambient phase space is the canonical lattice model: configuration $q:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$ paired with conjugate momentum $\pi$, here specialized to $n=2$. Coordinate functionals extract $q_i$ and $\pi_i$ as continuous linear maps on that product.
A local momentum profile is a map $f:\mathbb{R}^3\to\mathbb{R}$ giving the cell density $m_j=f(d_j,\pi_j,\pi_{j+1})$ with bond length $d_j=q_{j+1}-q_j$. Translation covariance is built in by depending only on differences of $q$.
This module repairs the unsplit Hojman–Kuchař–Teitelboim dynamic target: the unsplit momentum–Hamiltonian field is uninhabitable for honest nearest-neighbor profiles against the frozen quadratic Hamiltonian (singular when $p_0+p_1=0$). The repaired API uses smeared point-split momentum densities; the present structure supplies the Frechet cell data those densities need.
proof idea
Structure definition, not a proved theorem. It bundles three sibling profiles (partials in the bond, source-momentum, and target-momentum slots) with a single field asserting HasFDerivAt for every cell map on PhaseSpace 2. The claimed derivative is the linear combination of coordQ (j+1) - coordQ j, coordP j, and coordP (j+1) with coefficients from those three profiles. Downstream lemmas simply project this field (e.g. the one-line wrapper that reads off the cell derivative).
why it matters
Load-bearing data package for the point-split HKT repair on the two-site lattice. Downstream, the cell derivative is reified as an explicit continuous linear map, then lifted by weighted sum to the smeared momentum functional, yielding Fréchet differentiability of the full momentum observable. Directional evaluations in the $q$ and $\pi$ axes feed bracket identities, including the no-go witness computation that recovers ${M,H}=(N_0+N_1)(-\partial_d f+\partial_p f-\partial_r f)$ at the singular unsplit point. The module states explicitly that no rigidity theorem is proved and no ledger flag is flipped; the unsplit Dyn target remains as the falsification-adjacent record, while the strong point-split class is the load-bearing replacement. Touches the open Prop that the analogous no-go against campaign HamDyn is still unresolved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.