freeLedgerCombinerSemantics_iff_rcl
plain-language theorem explainer
Free-ledger combiner semantics on a real bivariate map P is equivalent to P being identically the canonical RCL combiner 2uv+2u+2v. Anyone closing the T4-to-T5 ledger bridge cites this biconditional. The proof is a short constructor that routes both directions through the intermediate ledger-linear-response characterization.
Claim. For $P:\mathbb{R}\to\mathbb{R}\to\mathbb{R}$, the free-ledger combiner axioms (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 $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 derived from the recognition ledger rather than taken as an analytic input. This module isolates the remaining algebraic condition: a two-variable combiner whose second argument responds linearly to free-ledger postings should be forced to the Recognition Composition Law polynomial.
The free-ledger combiner package is intentionally weaker than full ledger-linear response. It records symmetry, the boundary law $P(u,0)=2u$, the unit diagonal $P(1,1)=6$, additive posting in the second coordinate, continuity in that coordinate, and free-ledger additivity, leaving Cauchy linearization as a theorem rather than a field.
The canonical target is the RCL combiner $\mathrm{rclCombiner}(u,v)=2uv+2u+2v$, the polynomial form of the composition identity $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$ that feeds J-uniqueness (T5).
proof idea
Bidirectional constructor through the intermediate ledger-linear-response layer.
Forward: free-ledger semantics implies ledger-linear response by freeLedgerCombinerSemantics_iff_ledgerLinearResponse, then ledgerLinearResponse_forces_rcl (which runs the existing d'Alembert factorization gate) yields pointwise equality with the RCL combiner.
Reverse: pointwise equality with the RCL combiner implies ledger-linear response by ledgerLinearResponse_iff_rcl, which is then converted back to free-ledger semantics by the converse half of freeLedgerCombinerSemantics_iff_ledgerLinearResponse.
why it matters
This is the clean Phase 3 closure statement for free-ledger combiners: the ledger posting package is not merely sufficient for the RCL polynomial, it is exactly equivalent to it. Together with the gate theorem that forces RCL from factorization data, it completes the algebraic half of the T4-to-T5 bridge from the recognition ledger floor to J-uniqueness.
The module doc frames the remaining obligation as proving ledger-linear response from free-ledger interpretation; this biconditional packages that obligation into a single citation target. No downstream dependents are recorded yet, so the result stands as a terminal characterization inside LedgerToFactorization rather than an intermediate lemma in a longer chain.
Framework landmarks: RCL itself, and the forcing step T5 (J-uniqueness) that the RCL polynomial unlocks once the factorization gate is satisfied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.