differentiable_zeroMom2
plain-language theorem explainer
The weighted sum of vanishing momentum densities on the two-site phase space is a differentiable real function of the phase-space point. Anyone assembling the quartic zero-momentum decoy target cites this to discharge the kinetic-regularity (differentiability) obligation in the weak point-split schema. The proof is a one-line reduction: the sum is identically zero, hence constantly differentiable.
Claim. For any weight function $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}}_0(x,j)$ on the two-site phase space is differentiable over $\mathbb{R}$, where $\rho^{\mathrm{mom}}_0$ is the identically vanishing momentum density.
background
The ambient setting is the Wave C2 repair of the point-split HKT target. An adversarial pass showed that the weak dynamical point-split schema is decoy-inhabitable by a quartic zero-momentum configuration; this module isolates that decoy and excludes it from the strong class via a load-bearing momentum axiom.
Phase space on $n$ sites is the product of configuration and conjugate momentum fields on the periodic lattice $\mathbb{Z}/n\mathbb{Z}$. Here $n=2$. The vanishing momentum density is the constant-zero model density used as the decoy momentum; the weighted sum over the two sites is therefore a real-valued functional on that phase space.
Upstream, zeroMom2_eq_zero already records that the weighted sum equals the zero function pointwise. Differentiability of constant maps is then immediate from the standard calculus library.
proof idea
Term-mode, two steps. Rewrite the weighted sum via the identity that it equals the constant-zero function on phase space. Then apply the library fact that every constant real-valued map is differentiable. No case split on the weight or on the phase-space coordinates is required.
why it matters
Feeds the construction of the quartic zero-momentum decoy target, the formal witness that the weak point-split schema is decoy-inhabitable. That decoy supplies the kinetic-regularity field of the weak inhabitant while keeping momentum identically zero, so the strong-class load-bearing momentum gate can reject it. In the module narrative this is part of the discrimination gate: honest Hamiltonian advection passes the strong class, the quartic zero-momentum decoy fails. Strong-class rigidity itself is already dead and moves to the canonical-momentum target; this lemma only closes a regularity side-condition on the decoy side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.