nlPUnit
plain-language theorem explainer
Defines the unit-normalized nonlinear momentum on a ledger state: half of nlP applied to the net imbalance. Gravity and RS auditors cite it as the swap-odd counterexample package that meets continuity, balance-vanishing, and unit normalization yet fails consolidation additivity. The body is a one-line composition of existing chart maps.
Claim. For a ledger state $z=(z_1,z_2)$, let $m=z_1-z_2$ be the net imbalance. The unit-normalized nonlinear momentum is $p_{\mathrm{nl}}(z)=\frac{m+m^3}{2}$.
background
This module attacks unconditional momentum additivity from the recognition composition law alone. The consumer already shows that additivity under consolidation, continuity, balance-vanishing, and unit normalization $p(1,0)^2=1$ force EnergyEqualsCost; the remaining premise is whether RCL selects additivity.
On the chart carrier LedgerState, the net imbalance is $m(z)=z_1-z_2$ (subtraction only; no cost). The nonlinear map $\mathrm{nlP}(m)=m+m^3$ is the coordinate that defeats naive uniqueness of momentum. Ambient cost is $J$-cost, which satisfies RCL independently of any momentum observable.
The module exhibits two continuous, balance-vanishing, unit-normalized packages that disagree on additivity: plain imbalance (additive) versus absolute imbalance and this nonlinear unit map (non-additive).
proof idea
Pure definition: compose the net-imbalance projection with $\mathrm{nlP}(m)=m+m^3$, then divide by 2. No tactics or lemmas; the factor $1/2$ is the unit normalization so that $p_{\mathrm{nl}}(1,0)^2=1$.
why it matters
Supplies the swap-odd witness inside the additivity-attack verdict. Downstream theorems prove it is continuous, swap-odd, balance-vanishing, unit-normalized, and not additive under consolidation; nlPUnit_package bundles those facts. The packaged verdict records that RCL plus the companion axioms do not force additivity on this carrier, while a separate constructive path (net-imbalance reading plus 1D Cauchy) still discharges full additivity and EnergyEqualsCost. Landmark link: RCL on $J$-cost is ambient and momentum-blind, so momentum uniqueness needs an extra kinetic or Cauchy input, not composition alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.