differentiable_MomDyn
plain-language theorem explainer
For any real weight profile on the two-site lattice, the smeared dynamic momentum functional is everywhere differentiable on phase space. Gravity workers building Hojman–Kuchař–Teitelboim point-split targets cite this to justify Poisson brackets and Fréchet derivatives of momentum against Hamiltonian densities. The proof is a one-line lift from the existing Fréchet derivative lemma at each point.
Claim. For every weight $w:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$, the map $x\mapsto\sum_{j\in\mathbb{Z}/2\mathbb{Z}} w(j)\,\rho_{\mathrm{mom}}(x,j)$ on two-site phase space is differentiable over $\mathbb{R}$.
background
This module repairs the unsplit HKT dynamic target. The unsplit momentum–Hamiltonian identity is uninhabitable for smooth nearest-neighbor momentum against a frozen quadratic Hamiltonian at $n=2$: advection forces a singular relation when $p_0+p_1=0$. The repaired API uses smeared point-split momentum densities already present in the HamDyn brackets, with separate source and target advection densities.
MomDyn w is the linear smear of the local dynamic momentum density against a weight $w$ on $\mathbb{Z}/2\mathbb{Z}$. Phase space is the product of configuration and momentum coordinates on two sites. Differentiability of this smear is the analytic prerequisite for evaluating Poisson brackets of momentum against Hamiltonian densities in the point-split target schema.
The upstream lemma supplies an explicit Fréchet derivative of MomDyn w at every point, obtained by matching the product/difference form of the density against standard calculus rules on the product manifold.
proof idea
Term-mode one-liner. At each phase-space point $x$, invoke the upstream Fréchet lemma hasFDerivAt_MomDyn w x, which produces HasFDerivAt (MomDyn w) (MomDynD w x) x. Convert that witness to DifferentiableAt via the standard Mathlib coercion .differentiableAt, then package the pointwise family as global Differentiable.
why it matters
Point-split HKT targets require differentiable momentum smears so that the split momentum–Hamiltonian bracket identity can be stated and checked. Downstream, this theorem feeds the honest HamDyn inhabitant hamDynPointSplitTarget, the vacuum-kinetic weak target, the vacuum-shift weak target, and the concrete split identity mom_ham_split_vacuumKinetic.
In the SevenGaps gravity campaign the unsplit Dyn target remains as a falsification-adjacent record; the load-bearing class is the strong point-split target. Differentiability of the momentum sector is bookkeeping, not a rigidity theorem: no ledger flag is flipped here, and the module explicitly records that no rigidity is proved. The result sits inside the repaired Wave C2 R5 path that replaces singular unsplit advection by smeared source/target densities on the two-site lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.