monotone_additive_isLinear
plain-language theorem explainer
Any monotone additive map f : ℝ → ℝ is homogeneous over ℝ: f(x) = f(1)·x. Recognition Science cites this as the completeness-free regularity brick that replaces ContinuousOn in the additive Cauchy step under the d'Alembert reduction of the Recognition Composition Law. The proof pins rationals by the additive monoid homomorphism, then squeezes irrationals with density of ℚ and monotonicity, never invoking least-upper-bound completeness.
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)\cdot x$ for every real $x$.
background
Cauchy's additive equation $f(x+y)=f(x)+f(y)$ on $\mathbb{R}$ admits wild solutions once the axiom of choice is allowed, unless a regularity hypothesis is imposed. Classically one assumes continuity (or measurability). The Recognition Science cost-forcing chain needs the same conclusion without presupposing continuum completeness: the classical J-uniqueness route used ContinuousOn, which the §9 program aims to retire.
The local setting is the monotone d'Alembert route in Primitive Recognition Calculus. After the change of variables that turns the Recognition Composition Law into d'Alembert's functional equation, one obtains an even normalized solution $H$ of the form $\cosh\circ(\text{additive})$. Monotonicity of that additive inner map is the order-theoretic substitute for continuity.
The argument uses only Archimedean density of the rationals (exists_rat_btwn) and the additive monoid-homomorphism structure on $f$. No least-upper-bound axiom appears. Sibling results package the nonnegative restriction and feed the cosh-family assembly.
proof idea
First $f(0)=0$ from additivity at $(0,0)$. Package $f$ as an additive monoid homomorphism $F:\mathbb{R}\to+\mathbb{R}$. Rational homogeneity $f(q)=f(1)\cdot q$ is then map_ratCast_smul plus simplification.
Set $c:=f(1)$. Monotonicity gives $c\ge 0$. If $c=0$, sandwich $f(x)$ between values at rationals above and below $x$ to force $f(x)=0$. If $c>0$, prove $f(x)=c\cdot x$ by le_antisymm: each strict inequality $f(x)>c x$ or $f(x)<c x$ produces a rational between $x$ and $f(x)/c$, and monotonicity plus rational homogeneity yields a numerical contradiction. The squeeze uses only density of $\mathbb{Q}$, not completeness.
why it matters
This is the load-bearing §9 regularity brick for completeness-free cost forcing. Downstream, dAlembert_diff_eq_of_monotone and dAlembert_S_add_of_monotone use monotonicity to fix signs in the cosh addition formulae; phi_mul_of_monotone and dAlembert_cosh_of_monotone assemble the even normalized monotone d'Alembert solution as $\cosh\circ\text{linear}$; composition_law_monotone_forces_cosh_family closes the RCL side.
In the ledger factorization path it is re-exported and dualized to antitone_additive_isLinear, then consumed by ledgerLinearResponse_from_primitiveLedgerPosting_monotone and the non-vacuous directional variant. That replaces the analytic continuity gate in the additive Cauchy step that the RCL reduction lands on.
Framework landmark: T5 J-uniqueness classically needed continuum analysis; with this brick the continuum posit dissolves on the cost side down to one unit of scale. The §9 question (order-theoretic substitute for continuity on an Archimedean ordered field) is closed positively here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.