rationalLedgerPosting_iff_rcl
plain-language theorem explainer
Rational completed ledger posting for a two-argument combiner P is equivalent to P being identically the canonical RCL polynomial 2uv+2u+2v. Anyone sealing the T4-to-T5 ledger-to-factorization bridge cites this biconditional. The proof is a short constructor: one direction is the existing force lemma; the other routes through the two intermediate equivalences with ledger-linear response.
Claim. For any $P:\mathbb{R}\to\mathbb{R}\to\mathbb{R}$, the following are equivalent: (i) $P$ obeys rational completed ledger posting (symmetry, zero boundary $P(u,0)=2u$, unit diagonal $P(1,1)=6$, right-continuity, rational right-affine response, and free-ledger additivity); (ii) $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 read off 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 the matching ledger-linear response in its second argument, the d'Alembert factorization gate forces the RCL polynomial.
Rational completed ledger posting is the analytic-completion input 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. Its fields include symmetry, zero boundary $P(u,0)=2u$, unit diagonal $P(1,1)=6$, right-continuity, and rational right-affine response.
The canonical RCL combiner is the polynomial $rclCombiner(u,v)=2uv+2u+2v$, the unique target of the Recognition Composition Law after the T5 J-uniqueness step. Upstream, ledger-linear response is already known equivalent to this combiner, and rational posting is known equivalent to ledger-linear response.
proof idea
Tactic-mode constructor on the biconditional.
Forward direction is a one-line application of rationalLedgerPosting_forces_rcl, which itself reduces rational posting to ledger-linear response and then applies the existing force lemma to the RCL polynomial.
Reverse direction: assume $P$ equals the RCL combiner everywhere; feed that hypothesis into the reverse arm of ledgerLinearResponse_iff_rcl to obtain ledger-linear response, then into the reverse arm of rationalLedgerPosting_iff_ledgerLinearResponse to recover rational completed ledger posting. No new analysis is done here; the proof only composes the two intermediate equivalences with the one-way force lemma.
why it matters
This is the clean closed form of the Phase 3 semantic bridge: rational completed ledger posting is not merely sufficient for the RCL combiner, it is exactly that combiner. Together with the free-ledger additivity already proved upstream, it discharges the remaining algebraic obligation that lets the d'Alembert factorization gate force the RCL polynomial from ledger data rather than from an analytic ansatz.
In the forcing chain this sits at the T4-to-T5 interface. T5 uniquely forces $J(x)=(x+x^{-1})/2-1$, and the Recognition Composition Law is the two-variable identity $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$; the combiner $2uv+2u+2v$ is precisely the polynomial form of that identity in the cost coordinates. Closing the ledger side of the equivalence removes the last free analytic input before the gate theorem.
No downstream consumers are wired yet in the graph; the declaration is the terminal packaging of the rational-posting chain inside this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.