antitone_additive_isLinear
plain-language theorem explainer
Any additive map f : ℝ → ℝ that is antitone must be linear through the origin: f(x) = f(1)·x for all real x. Citation target for the directional (order) half of the ledger-to-factorization bridge, where RCL response slopes are negative for u < −1. Proof negates f, applies the monotone additive-linearity lemma, and recovers the claim by elementary algebra.
Claim. If $f:\mathbb{R}\to\mathbb{R}$ satisfies $f(x+y)=f(x)+f(y)$ for all real $x,y$ and is antitone, then $f(x)=f(1)\cdot x$ for every real $x$.
background
The module builds the T4-to-T5 bridge from the recognition ledger rather than from analytic continuity. Free-ledger additivity is already unconditional; the remaining algebraic gate is a ledger-linear response in the second argument of a two-variable combiner, which (with symmetry, boundary law, and unit diagonal) forces the RCL polynomial through the d'Alembert factorization gate.
Order regularity replaces continuity for the additive Cauchy equation on ℝ. The sibling result states that monotone additive maps are linear: $f(x)=f(1)\cdot x$. The present theorem is the antitone twin. In the RCL setting the response slope $2(u+1)$ is negative for $u<-1$, so the second-argument response is antitone on those slices, not monotone; both branches are required.
No continuity, measurability, or completeness hypotheses appear. The argument is pure order plus Cauchy additivity.
proof idea
Define $g(t):=-f(t)$. Additivity of $f$ immediately yields additivity of $g$ (one simp/ring step). Antitonicity of $f$ is equivalent to monotonicity of $g$ via neg_le_neg_iff. Apply the upstream lemma monotone_additive_isLinear to $g$ to obtain $g(x)=g(1)\cdot x$, i.e. $-f(x)=(-f(1))\cdot x$. Rewrite the right-hand side as $-(f(1)\cdot x)$ and cancel the global minus sign by linarith.
why it matters
Feeds the single downstream consumer ledgerLinearResponse_from_primitiveLedgerPosting_directional, which upgrades primitive ledger posting plus per-slice directional regularity (monotone or antitone in the second argument) to a full real ledger-linear response. That theorem is the genuine order replacement for the analytic continuity gate: the canonical RCL combiner has response slope $2(u+1)$ of fixed sign on each fixed-$u$ slice, so the hypothesis is consistent with its conclusion.
In the forcing chain this sits on the T4-to-T5 bridge: ledger structure forces the Recognition Composition Law polynomial rather than assuming it analytically. The antitone branch is mandatory because half the $(u,v)$-plane has negative slope; without it the directional route would be incomplete for the RCL response.
Closes the second order-regularity arm needed before factorization forcing can discharge rightAffine from ledger data alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.