ledgerLinearResponse_from_primitiveLedgerPosting_monotone
plain-language theorem explainer
Primitive ledger-posting semantics plus global monotonicity in the posted-mass argument yields full real ledger-linear response for a two-variable combiner. Cited by the monotone factorization gate and the monotone-forces-RCL theorem as the order-regularity half of the T4-to-T5 bridge. Proof builds the centered right response, gets additivity from the free ledger, then applies the monotone-additive-implies-linear lemma and rearranges.
Claim. Let $P:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ satisfy primitive ledger-posting semantics (symmetry, zero boundary $P(u,0)=2u$, unit diagonal $P(1,1)=6$, and additive response to free defect-ledger sums). If for every fixed $u$ the map $v\mapsto P(u,v)$ is monotone, then $P$ has ledger-linear response: $P(u,v)=(P(u,1)-P(u,0))\,v+P(u,0)$ for all $u,v$, together with the free-ledger additivity already present in the semantics.
background
Phase 3 of the foundation asks that the T4-to-T5 bridge be derived from the recognition ledger rather than assumed analytically. This module isolates the remaining algebraic condition: if a two-variable combiner has ledger-linear response in its second argument, then together with symmetry, the boundary law, and the unit diagonal, the d'Alembert factorization gate forces the Recognition Composition Law (RCL) polynomial.
Primitive ledger-posting semantics means the second coordinate is fed by actual free defect-ledger costs, and posting ledgers additively is the operation the combiner sees. Ledger-linear response strengthens this to an explicit affine law $P(u,v)=(P(u,1)-P(u,0))v+P(u,0)$, with free-ledger additivity pinned to the existing free-ledger theorem.
The key upstream regularity lemma is that every monotone additive map $f:\mathbb{R}\to\mathbb{R}$ is linear: $f(x)=f(1)\cdot x$. That replaces the classical continuity gate in the additive Cauchy step. A companion theorem upgrades posted-ledger additivity to ordinary right-posted additivity on $\mathbb{R}$.
proof idea
Refine the LedgerLinearResponse structure, copying symmetry, zero boundary, unit diagonal, and free-ledger additivity from the primitive semantics. The only field to prove is rightResponse.
Fix $u$ and define the centered response $r(t):=P(u,t)-P(u,0)$. Right-posted additivity (from the primitive semantics via the companion lemma) gives $r(x+y)=r(x)+r(y)$. Global monotonicity of $v\mapsto P(u,v)$ passes to $r$ by subtracting the constant $P(u,0)$. Apply monotone-additive-implies-linear to conclude $r(v)=r(1)\cdot v$, i.e. $P(u,v)-P(u,0)=(P(u,1)-P(u,0))v$. One linarith finishes the affine identity.
why it matters
This is the monotone special case of the order-regularity route from the free recognition ledger to ledger-linear response, feeding three parents: the monotone factorization gate (which supplies the full FactorizationAssociativityGate), the nonnegativity variant (which reduces global cost nonnegativity to this theorem), and the direct RCL-forcing theorem that concludes $P$ equals the canonical RCL combiner with no continuity or completeness hypotheses.
In the forcing chain this sits on the T4-to-T5 bridge: once ledger-linear response is in hand, the existing gate forces the RCL polynomial $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$, whose unique solution is the J-cost of T5. The doc-comment is explicit that global monotonicity is vacuous for the target combiner (RCL response slope $2(u+1)$ is negative for $u<-1$); the genuine non-vacuous order route is the directional (monotone-or-antitone per slice) theorem. This form is kept as a special case, a proof component for the nonnegativity path, and a non-vacuous statement on the physical cost cone $u\ge -1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.