RationalLedgerPostingSemantics
plain-language theorem explainer
A two-argument combiner P satisfies rational ledger posting when it is symmetric, hits the zero-boundary and unit-diagonal normalizations, is continuous in its second slot, is affine on rational second arguments, and preserves free-ledger cost additivity. Anyone deriving the T4-to-T5 bridge from ledger data rather than analytic fiat cites this package. It is a Prop structure bundling those six fields; no proof body.
Claim. A map $P:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ has rational ledger posting semantics when: $P(u,v)=P(v,u)$; $P(u,0)=2u$; $P(1,1)=6$; $v\mapsto P(u,v)$ is continuous for each $u$; for every real $u$ and rational $q$, $P(u,q)-P(u,0)=q\,(P(u,1)-P(u,0))$; and free defect-ledger cost is additive under ledger sum for every index type and weight.
background
Module setting is the ledger-to-factorization bridge: Phase 3 wants the T4-to-T5 step forced from recognition-ledger structure instead of assumed as analytic input. The free ledger already has unconditional additivity of ledger cost. The remaining algebraic condition is that a two-variable combiner respond linearly in its second argument on ledger data; with symmetry, the boundary law, and the unit diagonal, the existing d'Alembert factorization gate then forces the Recognition Composition Law (RCL) polynomial.
Rational posting is the analytic-completion input on the countable positive-ratio completion of that free ledger: costs already obey the affine response law on rationals, and the response is continuous in the completed real coordinate. Upstream cost notions (J-cost on recognition events, multiplicative-recognizer derived cost, PRC quotient cost, rung-coarsen multiset cost) supply the ambient meaning of "cost" that ledgerCost aggregates. DefectLedger is the free ledger carrier whose sum is the additivity domain.
proof idea
Definitional Prop structure: six named fields, empty proof body. Instantiation means exhibiting symmetry, zero-boundary $P(u,0)=2u$, unit diagonal $P(1,1)=6$, right-continuity, rational right-affineness, and free-ledger cost additivity. Downstream lemmas treat the structure as a hypothesis package and project fields (e.g. ledgerLinearResponse_from_rationalLedgerPosting copies symmetry, zeroBoundary, and completes the dense-rational affine law by continuity).
why it matters
This is the completed semantic bridge from free-ledger posting to the factorization gate. Downstream, factorizationGate_of_rationalLedgerPosting feeds it into FactorizationAssociativityGate; rationalLedgerPosting_forces_rcl and rationalLedgerPosting_iff_rcl identify it with the canonical RCL combiner $P(u,v)=\mathrm{rclCombiner}(u,v)$. Equivalence theorems (rationalLedgerPosting_iff_ledgerLinearResponse, freeLedgerCombinerSemantics_iff_rationalLedgerPosting) show it is the same completed T5 bridge as free-ledger combiner semantics and full ledger-linear response.
In the forcing chain this is the ledger-native route into T5 J-uniqueness and the RCL identity $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. It closes the Phase-3 gap: RCL is no longer an external analytic assumption but the unique continuous rational-affine symmetric combiner compatible with free-ledger additivity and the normalizations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.