momLoadBearingWitness_vals
plain-language theorem explainer
On the two-site phase space, the load-bearing momentum witness evaluates to configuration values (0,1) and conjugate momenta (1,0). Anyone proving that the Mom–Ham bracket is nonzero at this phase cites these four equalities. The proof is a one-line simp unfolding of the piecewise definition of the witness.
Claim. Let $\Phi=(\phi,\pi)$ be the load-bearing momentum witness in the two-site phase space over $\mathbb{Z}/2\mathbb{Z}$. Then $\phi(0)=0$, $\phi(1)=1$, $\pi(0)=1$, and $\pi(1)=0$.
background
This module strengthens the point-split Hamilton–Kirchhoff–Toda (HKT) dynamical target after an adversarial pass showed the weak schema is decoy-inhabitable by a quartic zero-momentum configuration. The strong class adds load-bearing momentum, advection tied to the Mom–Ham bracket calculus, and kinetic regularity, so that the quartic zero-momentum decoy is excluded while an honest Hamiltonian dynamical inhabitant remains.
Phase space on two sites is a pair of real-valued fields on $\mathbb{Z}/2\mathbb{Z}$ (configuration and conjugate momentum). The load-bearing witness is the explicit point whose configuration is the indicator of site 1 and whose momentum is the indicator of site 0. The four pointwise values of that witness are recorded here so downstream bracket computations can unfold without re-expanding the definition.
proof idea
One-line wrapper: simp unfolds the definition of the load-bearing witness phase, whose two components are piecewise if j = 0 then ... else ... on $\mathbb{Z}/2\mathbb{Z}$. Each of the four equalities is then immediate by case evaluation at $0$ and $1$.
why it matters
The sole downstream consumer is the theorem that the Mom–Ham bracket of the two site-momentum generators is nonzero at this witness phase. That nonzero bracket is the concrete load-bearing check used to keep the honest Hamiltonian dynamical target inside the strong class and to kill the quartic zero-momentum decoy.
In the Wave C2 repair narrative, weak-class rigidity is abandoned (the balanced-quartic falsifier shows it is false); discrimination moves to the strong class and ultimately to the canonical-momentum target. These four values are the arithmetic substrate of that discrimination gate: without them the bracket witness cannot fire. No ledger flag is flipped; the result is pure scaffolding for the strong-class inhabitant and the decoy exclusion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.