rclCombiner_freeLedgerSemantics
plain-language theorem explainer
The canonical RCL combiner $P(u,v)=2uv+2u+2v$ satisfies free-ledger combiner semantics: symmetry, zero boundary, unit diagonal, additive posting in the second argument, continuity, and free-ledger cost additivity. Anyone building the Phase 3 ledger-to-factorization bridge cites this as the model instance. The proof reuses the full factorization gate for three fields, then closes the rest by ring, continuity, and the free ledger's unconditional additivity.
Claim. The map $P(u,v)=2uv+2u+2v$ satisfies free-ledger combiner semantics: $P$ is symmetric, $P(u,0)=2u$, $P(1,1)=6$, posted increments add in the second argument ($P(u,v+w)-P(u,0)=(P(u,v)-P(u,0))+(P(u,w)-P(u,0))$), $v\mapsto P(u,v)$ is continuous for each $u$, and free-ledger cost is additive.
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: if a two-variable combiner has ledger-linear response in its second argument, then together with symmetry, the boundary law, and the unit diagonal, the existing d'Alembert factorization gate forces the RCL polynomial.
Free-ledger combiner semantics is the weaker intermediate structure. It records symmetry, $P(u,0)=2u$, $P(1,1)=6$, additive posting in the second coordinate, continuity in that coordinate, and free-ledger cost additivity. Unlike full ledger-linear response, it leaves Cauchy linearization as a theorem rather than a field of the structure.
The canonical RCL combiner is $P(u,v)=2uv+2u+2v$, the polynomial form of the Recognition Composition Law. It already satisfies the full factorization associativity gate; the free ledger independently supplies unconditional additivity of ledger cost.
proof idea
Instance construction for the six fields of free-ledger combiner semantics on the RCL combiner.
Symmetry, zero boundary, and unit diagonal are projected from the existing gate theorem that the RCL combiner satisfies full factorization associativity.
Right posted additivity: unfold the combiner definition and finish by ring on the polynomial identity.
Right continuity: unfold and apply the continuity tactic to the bilinear polynomial in the second variable.
Free-ledger additivity: invoke the free ledger's unconditional cost-additivity lemma (ledgerCost_add) on the posted increments.
why it matters
This is the model witness that the RCL polynomial carries free-ledger semantics, the weaker intermediate needed before full ledger-linear response. In the Phase 3 program, free-ledger additivity is already unconditional; the remaining obligation is to promote free-ledger semantics to ledger-linear response, from which the rightAffine field of the factorization gate follows and forces the RCL polynomial.
The declaration sits on the T4-to-T5 bridge: T5 is J-uniqueness with $J(x)=(x+x^{-1})/2-1$, and the RCL identity $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$ is the algebraic content of the combiner. Establishing that the canonical combiner is free-ledger-compatible keeps the ledger interpretation aligned with the forced factorization polynomial.
No downstream consumers are wired yet. The natural next step is the missing implication from free-ledger semantics to ledger-linear response, which would close the Phase 3 obligation named in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.