abs_imbalance_not_additive
plain-language theorem explainer
Absolute imbalance on ledger states is not additive under consolidation: pairing a pure debit with a pure credit yields the balanced state, so the absolute imbalance is 0 rather than 1+1. Anyone citing the Gap5 momentum no-go (composition law does not force additivity) needs this counterexample. The proof is a direct two-point evaluation with arithmetic simplification.
Claim. It is not the case that for all ledger states $z,w$, $|\mathrm{imbalance}(z+w)| = |\mathrm{imbalance}(z)| + |\mathrm{imbalance}(w)|$. Explicitly, consolidating the pure debit $(1,0)$ with the pure credit $(0,1)$ gives the balanced state $(1,1)$, and $|\mathrm{imbalance}(1,1)| = 0 \neq 1+1$.
background
This module sits in the Gap5 momentum-additivity attack on the Recognition Science gravity ledger. The consumer theorem already shows that additivity under consolidation, continuity, balance-vanishing, and unit normalization force EnergyEqualsCost. The remaining question is whether the recognition composition law (RCL) alone selects that additivity.
The carrier is LedgerState, pairs of real ledger coordinates with componentwise addition as consolidation. The signed observable imbalance measures net debit-minus-credit; absolute imbalance is its absolute value. Balanced states have vanishing signed imbalance, hence vanishing absolute imbalance. The ambient cost is the standard J-cost, which satisfies RCL independently of any momentum observable.
The module exhibits two continuous, balance-vanishing, unit-normalized packages on the same carrier: signed imbalance (additive) and absolute imbalance (not additive). This theorem is the explicit failure of additivity for the absolute package.
proof idea
Assume for contradiction that absolute imbalance is additive for every pair of ledger states. Instantiate on the pure debit $(1,0)$ and pure credit $(0,1)$. Componentwise addition gives $(1,1)$. Unfolding the definition of imbalance and simplifying by norm_num yields $0 = 1 + 1$, a contradiction. The argument is a pure two-point counterexample; no continuity or RCL facts are used.
why it matters
This is the no-go half of the absolute-imbalance package. Downstream, abs_imbalance_package bundles continuity, balance-vanishing, unit normalization, and this non-additivity into one witness on the same carrier and RCL cost as the additive signed-imbalance package. That pair feeds momentum_additivity_independent_of_composition_law and the module verdict momentumAdditivityCompositionVerdict.
In framework terms, RCL (the T5 J-cost identity and its composition law) constrains cost functionals of positive ledger ratios, not momentum observables. Because both packages share the same RCL ambient cost and differ only on additivity, no derivation whose only inputs are RCL plus continuity, balance-vanishing, and unit normalization can conclude unconditional momentum additivity on this chart. Outcome (a) of the module header is thereby refuted by counterexample rather than left unbuilt.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.