monotone_additive_isLinear
plain-language theorem explainer
Any monotone additive map f : ℝ → ℝ is homogeneous of degree one: f(x) = f(1)·x for all real x. Analysts and Recognition-Science foundation work cite it as the order-theoretic stand-in for continuity in Cauchy's functional equation. The proof packages f as an additive monoid homomorphism, gets Q-linearity from scalar transport, then closes the real case by rational density and a two-sided contradiction on the slope f(1).
Claim. Let $f:\mathbb{R}\to\mathbb{R}$ satisfy $f(x+y)=f(x)+f(y)$ for all real $x,y$ and be monotone nondecreasing. Then $f(x)=f(1)\,x$ for every real $x$.
background
The module builds the T4-to-T5 bridge from the recognition ledger rather than from analytic input. Free-ledger combiners already give unconditional additivity in the second argument; what remains is a regularity condition strong enough to force the completed real linear response used by the d'Alembert factorization gate, and thence the Recognition Composition Law polynomial.
Classically, Cauchy's equation on $\mathbb{R}$ needs a continuity (or measurability) gate to kill pathological Hamel solutions. Here that gate is replaced by monotonicity: an order hypothesis available without invoking completeness of the continuum as an analytic black box. The same brick appears in the Primitive Recognition Calculus monotone d'Alembert development as the "§9 regularity-substitute."
Upstream arithmetic facts used only as bookkeeping are the usual identities $n+0=n$, $0\cdot n=0$, and $n\cdot 1=n$ on the logic-derived naturals, together with the order relation and its antisymmetry. The real work is Mathlib's additive-homomorphism scalar map on rational casts plus density of $\mathbb{Q}$ in $\mathbb{R}$.
proof idea
From additivity at $(0,0)$ one gets $f(0)=0$. Package $f$ as an AddMonoidHom $F:\mathbb{R}\to+\mathbb{R}$. Mathlib's map_ratCast_smul then yields $f(q)=f(1)\cdot q$ for every rational $q$.
Set $c:=f(1)$. Monotonicity gives $c\ge 0$. If $c=0$, sandwich any $x$ between rationals above and below: monotonicity plus the rational formula force $f(x)\le 0$ and $f(x)\ge 0$, so $f(x)=0=c\cdot x$.
If $c>0$, prove $f(x)=c\cdot x$ by le_antisymm. Each direction is by contradiction: if $f(x)>c\cdot x$ (resp. $<$), density supplies a rational strictly between $x$ and $f(x)/c$; monotonicity plus the rational formula then produce incompatible inequalities on $f(x)$.
why it matters
This lemma is the order-regularity replacement for the continuity gate in the additive Cauchy step of the ledger-to-factorization bridge. Downstream, antitone_additive_isLinear reduces the decreasing case to this one by applying it to $-f$; that second branch is required because the RCL response slope $2(u+1)$ is negative for $u<-1$.
Both feed ledgerLinearResponse_from_primitiveLedgerPosting_monotone and the genuine non-vacuous route ledgerLinearResponse_from_primitiveLedgerPosting_directional (monotone or antitone per fixed first cost $u$). Those complete the real linear response that, 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$.
The same statement is re-exported in PRCMonotoneDAlembert, where it underwrites the monotone-fixed d'Alembert difference and $S$-addition identities (cosh/sinh addition without a continuity hypothesis). The §9 question whether analytic continuity can be replaced by a purely order-theoretic hypothesis is closed affirmatively here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.