nlPUnit_package
plain-language theorem explainer
Continuity, swap-oddness, balance-vanishing, and unit normalization still admit a non-additive momentum on LedgerState: the packaged witness nlPUnit. Anyone citing the Gap5 composition-law no-go uses this to rule out debit-credit parity as a stand-in for the kinetic condition. The proof is a five-field term that assembles prior continuity, oddness, vanishing, unit, and non-additivity lemmas.
Claim. There exists a momentum observable $p$ on ledger states such that $p$ is continuous, swap-odd, $p(z)=0$ whenever $z$ is balanced, $p(1,0)^2=1$, and yet $p$ fails additivity under consolidation: it is not true that $p(z+w)=p(z)+p(w)$ for all states $z,w$.
background
Gap5 attacks unconditional momentum additivity from the recognition composition law (RCL). The consumer theorem already shows that additivity plus continuity, balance-vanishing, and unit normalization $p(1,0)^2=1$ force EnergyEqualsCost. What remains is whether RCL itself selects additivity.
On the chart carrier LedgerState, ambient cost is $J$ (the T5 unique cost, also written $\cosh(\log x)-1$), which satisfies RCL independently of any momentum $p$. Two continuous, balance-vanishing, unit-normalized observables already disagree on additivity: signed imbalance (additive) and absolute imbalance (fails at consolidating $(1,0)$ with $(0,1)$).
This package strengthens the non-additive side: swap-oddness (debit-credit parity under swap) is added to the companion list. The module doc states the verdict: composition-law independence lands as a two-package witness, not a class theorem over all cost systems.
proof idea
Pure term-mode packaging. The goal is a five-way conjunction, discharged by the anonymous constructor
⟨nlPUnit_continuous, nlPUnit_swap_odd, nlPUnit_balance_vanishing, nlPUnit_unit, nlPUnit_not_additive⟩.
Each conjunct is a prior lemma about the same map: continuity; swap-oddness; vanishing on balanced states; squared unit value $1$ at $(1,0)$; and the explicit non-additivity counterexample. No new algebra is done here.
why it matters
Feeds the parent momentumAdditivityCompositionVerdict as the field swap_odd_unit_still_not_additive. That verdict is the Gap5 headline no-go: RCL on ambient $J$ plus continuity, balance-vanishing, and unit normalization do not force momentum additivity, even after adding swap-oddness.
In the Recognition chain this protects the kinetic-conditional route to EnergyEqualsCost. B1's kinetic additivity remains an independent input; debit-credit parity is not a substitute. The module pairs this witness with the additive imbalance package and the absolute-imbalance failure to show both additive and non-additive momenta survive every companion the consumer still uses except additivity itself.
Landmark tie-in: ambient cost is the T5 $J$-unique functional satisfying RCL; the argument is chart-local on LedgerState, consistent with the stated scope that this is a two-package witness, not a quantified class result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.