freeLedgerCombinerSemantics_iff_ledgerLinearResponse
plain-language theorem explainer
For a real two-argument combiner P, free-ledger posting semantics (additive second-argument posting plus continuity) is equivalent to completed ledger-linear response (affine law in the second argument). Anyone closing the T4-to-T5 ledger-to-factorization bridge cites this. One direction is the existing continuous-Cauchy linearization lemma; the converse rebuilds additivity and continuity from the affine response by algebra and elementary continuity of affine maps.
Claim. Let $P:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$. Then $P$ satisfies free-ledger combiner semantics (symmetry, zero boundary $P(u,0)=2u$, unit diagonal $P(1,1)=6$, additive posting in the second argument, continuity in that argument, and free-ledger cost additivity) if and only if it satisfies ledger-linear response (the same symmetry, boundary, diagonal, and free-ledger fields, together with the affine law $P(u,v)=(P(u,1)-P(u,0))\,v+P(u,0)$).
background
Module context is the Phase 3 ledger-to-factorization bridge: derive the T4-to-T5 gate from recognition-ledger structure rather than assume it analytically. A free ledger already gives unconditional cost additivity. The remaining algebraic condition is a two-variable combiner $P$ whose second argument responds linearly to posted ledger mass; with symmetry, boundary law, and unit diagonal, the d'Alembert factorization gate then forces the Recognition Composition Law (RCL) polynomial.
LedgerLinearResponse packages that completed bridge: $P(u,v)=(P(u,1)-P(u,0))v+P(u,0)$, plus free-ledger additivity. FreeLedgerCombinerSemantics is intentionally weaker: it records only additive posting
$P(u,v+w)-P(u,0)=(P(u,v)-P(u,0))+(P(u,w)-P(u,0))$
plus continuity in $v$, leaving Cauchy linearization as a theorem. Shared fields are symmetry $P(u,v)=P(v,u)$, zero boundary $P(u,0)=2u$, and unit diagonal $P(1,1)=6$.
Upstream, ledgerLinearResponse_from_free_ledger already proves that continuous additive posting yields the affine response over $\mathbb{R}$.
proof idea
Bidirectional constructor.
Forward: one-line application of ledgerLinearResponse_from_free_ledger, which linearizes continuous additive second-argument posting to the affine response law.
Converse: given ledger-linear response $h$, rebuild free-ledger semantics by copying symmetric, zeroBoundary, unitDiagonal, and free_ledger_additivity. For rightPostedAdditive, expand each term via $h$.rightResponse and cancel with ring. For rightContinuous, rewrite $v\mapsto P(u,v)$ as the affine map $v\mapsto (P(u,1)-P(u,0))v+P(u,0)$ by funext and $h$.rightResponse, then cite continuity of constant-multiple-of-identity plus constant.
why it matters
Closes the semantic gap between the weaker free-ledger posting package and the completed linear-response package that supplies the rightAffine field of the factorization gate. Downstream, freeLedgerCombinerSemantics_iff_rationalLedgerPosting identifies free-ledger semantics with rational completed ledger posting as "the same completed T5 semantic bridge," and freeLedgerCombinerSemantics_iff_rcl routes through this equivalence then ledgerLinearResponse_forces_rcl to conclude $P$ is exactly the canonical RCL combiner.
In the forcing chain this is the ledger-native path into T5 (J-uniqueness / RCL): once free-ledger semantics holds, RCL is forced, so the composition law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$ is no longer an analytic input. The module doc states the program explicitly: free-ledger additivity plus linear response yields rightAffine, and the existing gate theorem forces the RCL polynomial.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.