rclCombiner_rationalLedgerPostingSemantics
plain-language theorem explainer
The canonical RCL combiner $P(u,v)=2uv+2u+2v$ satisfies rational ledger posting semantics: symmetry, zero boundary, unit diagonal, right-continuity, rational affine response, and free-ledger additivity. 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 gate fields for the algebraic axioms and discharges continuity, rational affinity, and additivity by direct calculation plus unconditional ledger-cost additivity.
Claim. The canonical RCL combiner $P(u,v)=2uv+2u+2v$ satisfies rational ledger posting semantics: $P$ is symmetric; $P(u,0)=2u$ for all $u$; $P(1,1)=6$; for each fixed $u$, $v\mapsto P(u,v)$ is continuous; for all real $u$ and rational $q$, $P(u,q)-P(u,0)=q\,(P(u,1)-P(u,0))$; and free ledger costs are unconditionally additive under independent defect sums.
background
This module isolates the remaining algebraic condition in the Phase 3 T4-to-T5 bridge: derive the d'Alembert factorization gate from the recognition ledger rather than take it as analytic input. The free ledger already has unconditional additivity of cost. If a two-variable combiner has the matching ledger-linear response in its second argument, the rightAffine field of the factorization gate follows; with symmetry, boundary law, and unit diagonal, the gate theorem 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)$. Rational ledger posting semantics is the analytic-completion input on the countable positive-ratio completion of the free ledger: rational ledger costs already obey the affine response law, and the response is continuous in the completed real coordinate.
Upstream, the same combiner is already known to satisfy the full factorization associativity gate (symmetry, zero boundary, unit diagonal, and the remaining gate fields). Free-ledger cost additivity is unconditional: the cost of a sum of defect ledgers equals the sum of the costs, with no independence restriction.
proof idea
Instance construction for the six fields of rational ledger posting semantics. Symmetry, zero boundary, and unit diagonal are taken directly from the existing gate theorem for the canonical combiner. Right-continuity: unfold the bilinear definition and apply the continuity tactic. Right rational affinity: unfold, then norm_num and ring to check the affine identity on $\mathbb{Q}$. Free-ledger additivity: apply the unconditional ledger-cost additivity theorem from the recognition ledger floor (cost of $\Gamma+\Delta$ equals sum of costs).
why it matters
Places the canonical RCL combiner inside the rational completed posting semantics that the ledger-to-factorization bridge needs. Module goal: if a combiner has ledger-linear response in the second argument, then together with symmetry, boundary law, and unit diagonal the gate forces the RCL polynomial (the T5 J-uniqueness input). This theorem certifies that the standard RCL polynomial itself meets the rational-completion side of that bridge: affine response on rationals plus continuity, plus free-ledger additivity already proved unconditionally.
No downstream consumers are wired yet in the graph; the natural parent is the completed ledger-linear response equivalence (rational posting plus continuity), whose forward direction is algebraic and whose reverse is dense-rational completion. Framework landmark: feeds the T4-to-T5 step that derives J-uniqueness from ledger structure rather than assuming the analytic gate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.