rationalLedgerPosting_iff_ledgerLinearResponse
plain-language theorem explainer
Rational ledger posting (affine response on rationals plus continuity) is equivalent to full ledger-linear response on the reals. Anyone closing the T4-to-T5 ledger-to-factorization bridge cites this biconditional. Forward direction reuses the dense-rational completion theorem; reverse specializes the real affine law to continuity and rational points.
Claim. For a combiner $P:\mathbb{R}\to\mathbb{R}\to\mathbb{R}$, the following are equivalent: (i) $P$ satisfies rational ledger posting semantics (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); (ii) $P$ has full ledger-linear response $P(u,v)=(P(u,1)-P(u,0))\,v+P(u,0)$ for all real $v$, with the same shared fields.
background
Phase 3 of the foundation chain asks that the T4-to-T5 bridge be derived from the recognition ledger rather than assumed analytically. This module isolates the algebraic condition: if a two-variable combiner has ledger-linear response in its second argument, the rightAffine field of the d'Alembert factorization gate follows, and with symmetry, boundary law, and unit diagonal the gate forces the RCL polynomial.
Ledger-linear response means the second argument is governed by response to one unit of posted ledger mass: $P(u,v)=(P(u,1)-P(u,0))v+P(u,0)$, pinned to free-ledger additivity. Rational ledger posting is the analytic-completion input: the same shared fields, but only affine response on rational second arguments plus continuity in the completed real coordinate.
The upstream theorem ledgerLinearResponse_from_rationalLedgerPosting states that rational posting plus continuity completes the response from the dense rational ledger-ratio surface to all real costs.
proof idea
Biconditional by constructor.
Forward: one-line application of ledgerLinearResponse_from_rationalLedgerPosting, the dense-rational completion theorem.
Reverse: from full LedgerLinearResponse, build a RationalLedgerPostingSemantics record. Shared fields (symmetry, zero boundary, unit diagonal, free-ledger additivity) copy directly. Continuity of $v\mapsto P(u,v)$ follows by rewriting via rightResponse as an affine map $(P(u,1)-P(u,0))v+P(u,0)$ and composing continuous primitives. Rational affinity is rightResponse at $v=q\in\mathbb{Q}$, simplified by ring.
why it matters
This equivalence is the semantic hinge between the countable rational completion of free-ledger posting and the full real linear-response package that feeds the factorization gate. Downstream, factorizationGate_of_rationalLedgerPosting routes through the forward direction into factorizationGate_of_ledgerLinearResponse. The forcing theorems rationalLedgerPosting_forces_rcl and rationalLedgerPosting_iff_rcl likewise reduce to the linear-response RCL theorems via this iff. The free-ledger combiner equivalence freeLedgerCombinerSemantics_iff_rationalLedgerPosting uses the reverse direction.
In the forcing chain this closes the remaining algebraic condition on the T4-to-T5 bridge: ledger posting semantics become interchangeable with the linear response that yields the Recognition Composition Law (RCL) and thence T5 J-uniqueness. No open scaffold remains here; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.