rclCombiner_discreteLedgerPostingSemantics
plain-language theorem explainer
The canonical RCL combiner P(u,v)=2uv+2u+2v satisfies discrete free-ledger posting semantics: symmetry, zero boundary, unit diagonal, right-additivity on natural ledger costs, and free-ledger additivity. Anyone bridging the recognition ledger to the d'Alembert factorization gate cites this. The proof reuses the gate fields and closes the two ledger fields by ring arithmetic and the floor additivity lemma.
Claim. Let $P(u,v)=2uv+2u+2v$ be the canonical RCL combiner. Then $P$ obeys discrete ledger posting semantics: $P(u,v)=P(v,u)$; $P(u,0)=2u$; $P(1,1)=6$; for all real $u$ and naturals $m,n$, the excess $P(u,\cdot)-P(u,0)$ is additive on $m+n$; and $P$ inherits free-ledger cost additivity from the recognition ledger floor.
background
Phase 3 of the foundation asks that the T4-to-T5 bridge be derived from the recognition ledger rather than taken as an analytic input. This module isolates the algebraic condition: if a two-variable combiner has ledger-linear response in its second argument, together with symmetry, the boundary law, and the unit diagonal, the existing factorization gate forces the RCL polynomial.
The canonical combiner is $P(u,v)=2uv+2u+2v$, the bilinear form appearing in the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. Discrete posting semantics restrict the second coordinate to natural-number ledger costs (finite multiplicities before analytic completion). The five fields are symmetry, zero boundary $P(u,0)=2u$, unit diagonal $P(1,1)=6$, right-additivity of the posted excess on $\mathbb{N}$, and free-ledger additivity over arbitrary index sets.
Upstream, rclCombiner_satisfies_gate already shows $P$ meets the full factorization associativity gate, supplying the first three fields. Free-ledger additivity is the unconditional ledger-cost additivity proved on the recognition ledger floor.
proof idea
Structure construction, field by field. Symmetry, zero boundary, and unit diagonal are projected directly from rclCombiner_satisfies_gate. For right natural posted additivity, introduce $u,m,n$, unfold the combiner definition, then close by norm_num and ring: the excess $P(u,k)-P(u,0)$ is exactly $2uk$, which is additive in the natural argument. Free-ledger additivity is a one-line appeal to RecognitionLedgerFloor.ledgerCost_add.
why it matters
This is the discrete-surface certificate that the RCL combiner already carries free-ledger posting law before analytic completion of the second argument. In the module's forcing story, that certificate is the remaining algebraic input needed so that ledger-linear response yields the rightAffine field of the d'Alembert factorization gate, and thence the RCL polynomial itself (the T5 J-uniqueness landmark). It sits between the unconditional free-ledger additivity on the floor and the full gate theorem that forces $J(x)=\cosh(\log x)-1$. No downstream consumers are wired yet (used_by is empty); the natural parents are the discrete-to-rational and primitive-posting bridges in this same file, and ultimately the T4-to-T5 ledger-derived factorization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.