nlPUnit_unit
plain-language theorem explainer
Unit normalization for the nonlinear momentum coordinate: on the pure-credit ledger state (1,0), the squared value equals 1. Anyone assembling the swap-odd non-additive package cites this. The proof is a one-line numerical unfolding of the definitions.
Claim. Let the ledger imbalance be $z_1 - z_2$, let $\mathrm{nlP}(m) = m + m^3$, and let the unit-normalized nonlinear momentum be $\mathrm{nlP}(\mathrm{imbalance}(z))/2$. Then on the pure-credit state $(1,0)$ one has $\bigl(\mathrm{nlP}(\mathrm{imbalance}(1,0))/2\bigr)^2 = 1$.
background
This module sits in the Gap-5 attack on unconditional momentum additivity. The consumer theorem already shows that additivity under consolidation, continuity, balance-vanishing, and unit normalization $p(1,0)^2 = 1$ force EnergyEqualsCost. The remaining question is whether the recognition composition law alone selects additivity.
Ledger states are pairs; imbalance is the net $z_1 - z_2$, defined by subtraction with no cost. The nonlinear map $\mathrm{nlP}(m) = m + m^3$ reparametrizes that imbalance; dividing by 2 yields the unit-normalized coordinate used here. Absolute imbalance is a competing continuous, balance-vanishing, unit-normalized observable that fails additivity, so the composition law cannot force additivity on this chart.
proof idea
One-line wrapper: norm_num unfolds nlPUnit, nlP, and imbalance on the concrete point $(1,0)$. Imbalance is $1-0=1$, $\mathrm{nlP}(1)=1+1^3=2$, division by 2 gives 1, and $1^2=1$. No lemmas beyond definitional reduction.
why it matters
Feeds nlPUnit_package, the swap-odd witness that continuity, swap-oddness, balance-vanishing, and unit normalization still leave room for a non-additive momentum. That package is the constructive half of the module verdict: the composition law does not select additivity, and debit-credit parity is not a substitute for the kinetic condition. Unit normalization is one of the four companion hypotheses the EnergyEqualsCost consumer still consumes; discharging it for this nonlinear coordinate keeps the no-go tight. Framework context is Gap-5 gravity scaffolding around ledger momentum, not the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.