ledgerLinearResponse_from_primitiveLedgerPosting_nonneg
plain-language theorem explainer
Primitive ledger-posting semantics plus the global order bound that posting nonnegative mass never lowers cost yields full ledger-linear response in the second argument. Anyone closing the T4–T5 bridge from the free ledger rather than analytic continuity cites this. The proof reduces nonnegativity to per-slice monotonicity via additive Cauchy on the centered response, then reuses the monotone gate.
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 right-posted additivity against free defect-ledger costs). If moreover $P(u,0)\le P(u,v)$ whenever $v\ge 0$, 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 pin.
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: free-ledger additivity is already unconditional; if a two-variable combiner has ledger-linear response in its second argument, the rightAffine field of the d'Alembert factorization gate follows, and with symmetry, boundary law, and unit diagonal the gate forces the RCL polynomial.
Primitive ledger-posting semantics is the ledger-native surface: the second coordinate is fed by actual free defect-ledger costs, and additive posting of ledgers is what 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)$, pinned to free-ledger additivity.
The nonnegativity hypothesis is the order shadow of ledger-cost nonnegativity: posting nonnegative defect mass never lowers cost. Doc-comment honesty note: the global form is vacuous for the canonical RCL combiner when $u<-1$; it holds on the physical cone $u\ge 0$.
proof idea
One-step reduction to the monotone gate ledgerLinearResponse_from_primitiveLedgerPosting_monotone. For fixed first cost $u$, center the second-argument slice as $f(v)=P(u,v)-P(u,0)$. Right-posted additivity (primitiveLedgerPosting_forces_rightPostedAdditive) gives Cauchy additivity of $f$. The global nonnegativity hypothesis rearranges to $f\ge 0$ on $[0,\infty)$. The sibling lemma additive_nonnegOnNonneg_isMonotone then yields monotonicity of $f$, hence of $v\mapsto P(u,v)$. Feed that monotone family into the monotone-to-linear-response theorem and finish.
why it matters
This is the ledger-internal order route from primitive posting to completed real linear response, feeding two parent theorems in the same module: factorizationGate_of_primitiveLedgerPosting_nonneg (supplies the full factorization associativity gate from ledger-native cost nonnegativity, not analytic continuity) and primitiveLedgerPosting_nonneg_forces_rcl (forces the canonical RCL combiner $P=\mathrm{rclCombiner}$).
In the forcing chain this closes the T4-to-T5 step toward J-uniqueness and the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. The only order input is the shadow of ledgerCost_nonneg. The doc-comment flags that global nonnegativity is vacuous off the physical cone; the directional sibling is the non-vacuous global closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.