rclCombiner_primitiveLedgerPostingSemantics
plain-language theorem explainer
The canonical RCL combiner P(u,v)=2uv+2u+2v satisfies primitive free-ledger posting semantics: symmetry, zero boundary, unit diagonal, and additivity when the second argument is a free defect-ledger cost. Anyone deriving the T4-to-T5 factorization bridge from the recognition ledger rather than assuming it analytically would cite this. The proof reuses the existing factorization-gate fields and reduces both additivity obligations to unconditional free-ledger cost additivity plus a ring identity.
Claim. The bilinear combiner $P(u,v)=2uv+2u+2v$ obeys primitive ledger-posting semantics: $P$ is symmetric, $P(u,0)=2u$ for all real $u$, $P(1,1)=6$, free defect-ledger costs add, and $P$ is additive in its second argument whenever that argument is the cost of a free defect ledger (right ledger-posted additivity).
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 factorization gate forces the RCL polynomial.
The canonical RCL combiner is $P(u,v)=2uv+2u+2v$, the polynomial form of the Recognition Composition Law right-hand side. Primitive ledger-posting semantics is the structure closest to the Phase-2 free ledger: the second coordinate is fed directly by costs of actual free defect ledgers, and additive posting of those ledgers is the operation the combiner sees. It sits upstream of the discrete rank-one natural-number surface.
Upstream, free-ledger cost is unconditionally additive: the cost of a sum equals the sum of the costs, with no independence restriction. The same combiner is already known to satisfy the full factorization associativity gate (symmetry, zero boundary, unit diagonal, and the remaining gate fields).
proof idea
Four of the five structure fields are immediate. Symmetry, zero boundary, and unit diagonal are projected from the existing theorem that the RCL combiner satisfies the factorization gate. Free-ledger additivity is exactly the unconditional ledger-cost additivity theorem applied to the weight and the two defect ledgers.
The remaining field, right ledger-posted additivity, rewrites the ledger cost of a sum via that same additivity theorem, unfolds the combiner definition $P(u,v)=2uv+2u+2v$, and closes by ring arithmetic: the excess $P(u,c)-P(u,0)$ is linear in the cost $c$, so it splits over sums of free ledgers.
why it matters
This declaration certifies that the canonical RCL polynomial already lives on the primitive free-ledger surface, before any passage to the rank-one natural-number discrete surface. In the module program, that is the algebraic condition needed so ledger-linear response yields the right-affine field of the d'Alembert factorization gate; with symmetry, boundary, and unit diagonal, the gate theorem then forces the RCL polynomial and thereby feeds T5 J-uniqueness, $J(x)=(x+x^{-1})/2-1$.
No downstream consumers are wired yet in the dependency graph. Sibling lemmas (free-ledger combiner semantics from primitive posting; discrete posting from primitive posting) are the natural next steps toward closing the T4-to-T5 bridge from the ledger floor rather than assuming factorization analytically. The RCL identity $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$ is the composition law whose polynomial skeleton this instance installs on the ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.