additive_nonnegOnNonneg_isMonotone
plain-language theorem explainer
An additive map $f:\mathbb{R}\to\mathbb{R}$ that stays non-negative on non-negative inputs is monotone on all of $\mathbb{R}$. Anyone wiring ledger cost into the d'Alembert factorization gate cites this as the pure order shadow of non-negative posted mass. The argument is short algebra: $f(0)=0$, then $f(b)=f(b-a)+f(a)$ with $f(b-a)\ge 0$ when $a\le b$. No continuity is used.
Claim. Let $f:\mathbb{R}\to\mathbb{R}$ satisfy $f(x+y)=f(x)+f(y)$ for all $x,y\in\mathbb{R}$, and $f(x)\ge 0$ whenever $x\ge 0$. Then $f$ is monotone: $a\le b$ implies $f(a)\le f(b)$.
background
This module isolates the remaining algebraic condition for the T4-to-T5 bridge: derive the recognition composition law from the recognition ledger rather than assume it analytically. A ledger is a double-entry collection of recognition events; free-ledger theorems already give unconditional additivity of posted mass. The missing piece is that a two-variable combiner, linear in its second argument, yields the rightAffine field of the d'Alembert factorization gate.
The present lemma is the one-variable order fact behind that bridge. Additivity alone forces $f(0)=0$. Non-negativity on the cone $x\ge 0$ is the order shadow of ledger cost never decreasing when non-negative defect mass is posted. Together these pin monotonicity on all of $\mathbb{R}$ with no topology.
Upstream arithmetic is ordinary real cancellation (add_zero, sub_add_cancel); the ledger structures supply the semantic reading, not the algebra.
proof idea
First specialize additivity at $(0,0)$ and cancel to get $f(0)=0$. Fix $a\le b$. Rewrite $b=(b-a)+a$ and apply additivity, then cancel the sum, obtaining $f(b)=f(b-a)+f(a)$. The cone hypothesis gives $f(b-a)\ge 0$ because $b-a\ge 0$. Linear arithmetic finishes $f(a)\le f(b)$. The whole proof is four short have-blocks plus linarith; no continuity, measurability, or completeness lemma is invoked.
why it matters
Downstream, ledgerLinearResponse_from_primitiveLedgerPosting_nonneg applies this fact slicewise in the second argument of a primitive ledger posting: global cost non-negativity upgrades to a completed real ledger-linear response, which is exactly the input the free-ledger combiner needs for the d'Alembert gate. That gate, with symmetry, boundary law, and unit diagonal, forces the RCL polynomial and thereby the T5 J-uniqueness step ($J(x)=(x+x^{-1})/2-1$) in the forcing chain.
The doc-comment is explicit that this is only the order shadow of ledger-cost non-negativity. The honesty note on the parent theorem matters: the global non-negativity hypothesis is vacuous for the target combiner off the physical cone $u\ge 0$; the genuine physical case lives on that cone via the directional sibling. This lemma still closes the monotone half of the algebraic bridge cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.