primitiveLedgerPosting_forces_rcl
plain-language theorem explainer
Primitive ledger-posting semantics plus continuity in the second argument force any two-variable combiner P to equal the canonical RCL combiner 2uv+2u+2v. Researchers deriving the Recognition Composition Law from ledger axioms rather than analytic input would cite this. The proof is a short composition: primitive posting yields completed ledger-linear response, which the existing factorization gate converts into RCL uniqueness.
Claim. Let $P:\mathbb{R}\to\mathbb{R}\to\mathbb{R}$. Suppose $P$ is symmetric, obeys the zero boundary $P(u,0)=2u$ and the unit diagonal $P(1,1)=6$, and is additive under free defect-ledger posting in its second argument. If $v\mapsto P(u,v)$ is continuous for every fixed $u$, then $P(u,v)=2uv+2u+2v$ for all real $u,v$.
background
This module isolates the T4-to-T5 bridge as a ledger-derived algebraic condition rather than an analytic input. The free recognition ledger already supplies unconditional additivity of defect costs. The remaining question is when a two-variable combiner $P$ inherits that additivity as a linear response in its second argument, so the d'Alembert factorization gate can fire.
Primitive ledger-posting semantics package four axioms on $P$: symmetry $P(u,v)=P(v,u)$; zero boundary $P(u,0)=2u$; unit diagonal $P(1,1)=6$; and right-posted additivity, meaning that for any weight $w$ and free defect ledgers $\Gamma,\Delta$, the excess $P(u,\mathrm{cost}(w,\Gamma+\Delta))-P(u,0)$ splits as the sum of the excesses for $\Gamma$ and $\Delta$. This surface talks directly to free defect ledgers, closer to the Phase-2 ledger than the discrete natural-number posting surface.
The target is the canonical RCL combiner $\mathrm{rclCombiner}(u,v)=2uv+2u+2v$, the unique polynomial forced by the Recognition Composition Law once the factorization gate is open. Upstream, ledger-linear response already forces that polynomial through the gate theorem; the missing step is promoting primitive posting plus continuity to full ledger-linear response.
proof idea
Two-line term composition. First apply ledgerLinearResponse_from_primitiveLedgerPosting, which (via free-ledger combiner semantics extracted from the primitive axioms plus continuity) produces a full LedgerLinearResponse witness for $P$. Then feed that witness into ledgerLinearResponse_forces_rcl, which opens the factorization gate and rewrites $P$ as rclCombiner by the existing gate-forces-RCL theorem. No new algebra is done at this layer.
why it matters
Phase 3 of the foundation asks that the T4-to-T5 step be derived from the recognition ledger rather than assumed. This theorem closes the continuity route from the most ledger-native posting surface (primitive free-defect posting) all the way to the canonical RCL polynomial. That polynomial is exactly the two-variable form of the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$, which sits at the T5 J-uniqueness landmark in the forcing chain.
A sibling doc-comment records the parallel order-regularity route, where monotonicity replaces continuity as the regularity gate. Together the two routes show that either analytic or order hypotheses, once paired with primitive ledger posting, discharge the factorization gate. No downstream consumers are wired yet in the graph; the declaration is a terminal bridge lemma ready for the unified forcing chain to import.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.