freeLedgerCombinerSemantics_iff_rationalLedgerPosting
plain-language theorem explainer
Free-ledger combiner semantics and rational completed ledger posting are equivalent for any two-variable real combiner. Anyone working the T4-to-T5 ledger bridge can treat free-ledger additivity-plus-continuity and rational affine completion as the same completed semantic package. The proof is a pure iff chain: both sides are already equivalent to completed ledger-linear response, so they match each other by composition.
Claim. For any $P:\mathbb{R}\to\mathbb{R}\to\mathbb{R}$, free-ledger combiner semantics on $P$ (symmetry, zero boundary $P(u,0)=2u$, unit diagonal $P(1,1)=6$, right-posted additivity, right continuity, and free-ledger additivity) hold if and only if rational ledger posting semantics on $P$ hold (the same boundary and continuity data, with affine response on rational second arguments).
background
This module isolates the remaining algebraic condition in the Phase 3 T4-to-T5 bridge: derive the factorization combiner from the recognition ledger rather than assume it analytically. The free ledger already gives unconditional additivity; a two-variable combiner with matching ledger-linear response in its second argument yields the rightAffine field of the d'Alembert factorization gate, which with symmetry, boundary law, and unit diagonal forces the RCL polynomial.
Free-ledger combiner semantics records a weaker response law than full ledger-linear response: additive posting in the second coordinate plus a continuity gate, leaving Cauchy linearization as a theorem. Rational ledger posting is the analytic-completion input on the countable positive-ratio completion: costs already obey the affine response on rationals, continuous in the completed real coordinate.
Two upstream equivalences pin the picture: free-ledger semantics is exactly completed ledger-linear response, and rational posting plus continuity is exactly the same completed linear response (forward algebraic, reverse by dense-rational completion).
proof idea
Term-mode constructor on the biconditional. Left-to-right: apply free-ledger $\Rightarrow$ ledger-linear response, then ledger-linear response $\Rightarrow$ rational posting. Right-to-left: reverse the same two arrows. No new analysis; pure composition of freeLedgerCombinerSemantics_iff_ledgerLinearResponse and rationalLedgerPosting_iff_ledgerLinearResponse.
why it matters
Closes the identification that free-ledger posting and rational completed posting are the same completed T5 semantic bridge. In the forcing chain this sits at the ledger side of T5 J-uniqueness and the Recognition Composition Law: once either semantic package is established, the d'Alembert gate can force the RCL combiner polynomial without choosing a preferred completion language.
No downstream consumers are wired yet (used_by is empty), so the lemma is presently a consolidation node inside LedgerToFactorization. It lets later gate theorems cite whichever presentation is convenient (free additivity or rational affine response) without re-proving continuity or linearization. It does not itself force $J$ or $\phi$; it only equates two completed ledger interfaces that feed that forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.