rationalLedgerPosting_forces_rcl
plain-language theorem explainer
Any two-variable real combiner that obeys rational completed ledger posting equals the canonical RCL polynomial $2uv+2u+2v$ pointwise. Cite this when closing the ledger-to-factorization bridge: rational affine response plus continuity already pins the Recognition Composition Law combiner. The proof is a one-line composition of the rational-posting/linear-response equivalence with the existing linear-response forcing theorem.
Claim. If $P:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ satisfies rational completed ledger posting (symmetry, zero boundary $P(u,0)=2u$, unit diagonal $P(1,1)=6$, continuity in the second argument, affine response on rational second arguments, and free-ledger additivity), then $P(u,v)=2uv+2u+2v$ for all real $u,v$.
background
This module builds the Phase 3 bridge from the recognition ledger to d'Alembert factorization (T4 to T5). The free ledger already gives unconditional additivity; the remaining algebraic input is a two-variable combiner with ledger-linear response in its second argument. With symmetry, the boundary law, and the unit diagonal, the factorization gate forces the RCL polynomial.
Rational completed ledger posting is the analytic-completion package: on the countable positive-ratio completion of the free ledger, costs already obey the affine response law on rationals, and the response is continuous in the completed real coordinate. Explicit fields include $P(u,v)=P(v,u)$, $P(u,0)=2u$, $P(1,1)=6$, right-continuity, and $P(u,q)-P(u,0)=q,(P(u,1)-P(u,0))$ for $q\in\mathbb{Q}$.
The canonical RCL combiner is $rclCombiner(u,v)=2uv+2u+2v$, the bilinear form appearing in the Recognition Composition Law. Upstream, ledger-linear response already forces this polynomial through the gate theorem; rational posting is equivalent to ledger-linear response by dense-rational completion plus continuity.
proof idea
One-line term proof. Apply the forward direction of rationalLedgerPosting_iff_ledgerLinearResponse to turn the rational-posting hypothesis into LedgerLinearResponse P, then feed that into ledgerLinearResponse_forces_rcl, which rewrites through the factorization gate and identifies $P$ with rclCombiner. No new algebra is done here; the work sits in those two lemmas.
why it matters
This is the forcing half of the equivalence that rational completed ledger posting is exactly the canonical RCL combiner. Downstream, rationalLedgerPosting_iff_rcl uses it as the left-to-right constructor, pairing it with the reverse path through linear response.
In the framework, it discharges the remaining algebraic condition of the T4-to-T5 bridge: once the ledger supplies rational affine response and continuity, the Recognition Composition Law polynomial is forced rather than assumed. That polynomial is the two-variable form behind T5 J-uniqueness ($J(x)=(x+x^{-1})/2-1$) and the RCL identity $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. Closing this direction lets the ledger, not an external analytic ansatz, select the cost that later forces $\varphi$, the eight-tick octave, and $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.