ledgerLinearResponse_from_primitiveLedgerPosting_directional
plain-language theorem explainer
Primitive ledger-posting semantics plus per-slice directional regularity (each fixed first-cost slice is monotone or antitone in posted mass) forces the completed ledger-linear response law. Anyone bridging the free recognition ledger to the d'Alembert factorization gate cites this as the non-vacuous order-theoretic route. The proof builds the centered response, gets Cauchy additivity from primitive posting, then applies the monotone or antitone additive-implies-linear lemmas slicewise.
Claim. If $P:\mathbb{R}\to\mathbb{R}\to\mathbb{R}$ satisfies primitive ledger-posting semantics (symmetry, zero boundary $P(u,0)=2u$, unit diagonal $P(1,1)=6$, and additive response to free defect-ledger postings) and, for every fixed first cost $u$, the map $v\mapsto P(u,v)$ is either monotone or antitone, then $P$ has ledger-linear response: $P(u,v)=(P(u,1)-P(u,0))\cdot v+P(u,0)$ for all $u,v$, together with free-ledger additivity.
background
This module is the Ledger-to-Factorization bridge. Phase 3 asks that the T4-to-T5 step be derived from the recognition ledger rather than assumed as analytic input. The free ledger already proves unconditional additivity; 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 packages symmetry, zero boundary $P(u,0)=2u$, unit diagonal $P(1,1)=6$, and the law that posting free defect ledgers additively is the operation seen by the combiner. Ledger-linear response strengthens this by requiring the closed form $P(u,v)=(P(u,1)-P(u,0))v+P(u,0)$ plus free-ledger additivity.
Upstream, primitive posting forces ordinary real additivity of the centered right response. The lemmas that monotone (resp. antitone) additive real maps are linear replace continuity in the Cauchy step by order regularity; the antitone branch is needed because the RCL slope $2(u+1)$ is negative for $u<-1$.
proof idea
Refine the ledger-linear-response structure, copying symmetry, zero boundary, unit diagonal, and free-ledger additivity straight from the primitive hypothesis. For the right-response field, fix $u$ and set $\mathrm{response}(t):=P(u,t)-P(u,0)$. Additivity of this response is exactly the upstream theorem that primitive posting forces right-posted real additivity. Case-split on the directional hypothesis at $u$: if the slice is monotone (resp. antitone), subtracting the constant $P(u,0)$ preserves monotonicity (resp. antitonicity), so the corresponding additive-implies-linear lemma yields $\mathrm{response}(x)=\mathrm{response}(1)\cdot x$. Specialize at $x=v$ and rearrange by linear arithmetic to the affine form $P(u,v)=(P(u,1)-P(u,0))v+P(u,0)$.
why it matters
This is the genuine non-vacuous order replacement for the analytic continuity gate on the T4-to-T5 bridge. Global monotonicity is vacuous for the target RCL combiner (response slope $2(u+1)$ changes sign at $u=-1$), but per-slice directional regularity is satisfied by the canonical combiner, so the forcing hypothesis is consistent with its conclusion.
Downstream, the directional factorization-gate theorem feeds this result into the full gate, and the directional RCL-forcing theorem concludes $P$ equals the RCL combiner. That lands on the Recognition Composition Law and forcing-chain step T5 (J-uniqueness via $J(x)=(x+x^{-1})/2-1$). The module's stated goal is exactly this isolation: ledger structure plus a mild order hypothesis, not continuum analysis, forces the RCL polynomial.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.