primitiveLedgerPosting_directional_forces_rcl
plain-language theorem explainer
Primitive ledger-posting semantics plus a per-slice monotone-or-antitone regularity condition force any two-variable combiner to equal the canonical RCL polynomial $2uv+2u+2v$. Anyone deriving the Recognition Composition Law from ledger axioms rather than analytic assumptions would cite this. The proof is a two-step term composition: directional posting yields ledger-linear response, which already forces the RCL combiner.
Claim. Let $P:\mathbb{R}\to\mathbb{R}\to\mathbb{R}$ satisfy primitive ledger-posting semantics: symmetry $P(u,v)=P(v,u)$, zero boundary $P(u,0)=2u$, unit diagonal $P(1,1)=6$, and additive response under free defect-ledger posting. If for every fixed $u$ the map $v\mapsto P(u,v)$ is monotone or antitone, then $P(u,v)=2uv+2u+2v$ for all real $u,v$.
background
Phase 3 of the foundation chain asks that the T4-to-T5 bridge be derived from the recognition ledger rather than assumed as an analytic input. The free ledger already proves unconditional additivity of cost under posting. The remaining algebraic condition is that a two-variable combiner have the corresponding ledger-linear response in its second argument; with symmetry, the boundary law, and the unit diagonal, the d'Alembert factorization gate then forces the RCL polynomial.
Primitive ledger-posting semantics packages those ledger-native axioms: symmetry, $P(u,0)=2u$, $P(1,1)=6$, and the identity that posting free defect ledgers additively is seen by the combiner as additive cost increments. The target is the canonical RCL combiner $2uv+2u+2v$, the bilinear form in the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$.
The directional hypothesis is mild: each fixed-$u$ slice is monotone or antitone in $v$. The canonical combiner itself satisfies this, so the forcing is non-vacuous.
proof idea
One-line term wrapper composing two prior results. First, ledgerLinearResponse_from_primitiveLedgerPosting_directional turns primitive posting semantics plus the per-slice monotone-or-antitone alternative into the intermediate ledger-linear-response structure (right-affine response in the second argument). That structure is then fed to ledgerLinearResponse_forces_rcl, which already proves every such combiner equals the RCL polynomial $2uv+2u+2v$. No fresh algebra is performed at this layer.
why it matters
This is the Phase-3 ledger-native forcing of the RCL combiner under directional regularity, closing the T4-to-T5 bridge from ledger axioms rather than analytic continuity. Downstream, satisfiesCompositionLaw_of_ledgerComposes applies it directly: if a cost $F$ composes through such a $P$, then $P$ is forced to the RCL combiner, so $F$ satisfies the Recognition Composition Law. That law is the functional equation whose unique solution under the forcing chain is the J-cost of T5, $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$).
A sibling non-negativity route (rclCombiner_postingNonneg) shows the intended combiner also meets the order-faithfulness hypothesis grounded in ledger-cost non-negativity, confirming both regularity paths are inhabited by the physical target.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.