primitiveLedgerPosting_monotone_forces_rcl
plain-language theorem explainer
Primitive free-ledger posting plus global monotonicity in the second slot forces any two-argument combiner to equal the canonical RCL polynomial $2uv+2u+2v$. Foundation workers bridging T4 ledger additivity to the T5 factorization gate cite this. The proof is a two-step term composition: monotone primitive posting yields ledger-linear response, which the existing gate theorem converts into RCL identity.
Claim. Let $P:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ satisfy primitive ledger-posting semantics (symmetry, boundary $P(u,0)=2u$, unit diagonal $P(1,1)=6$, and additive response when free defect ledgers are posted into the second argument). If for every fixed $u$ the map $v\mapsto P(u,v)$ is monotone, then $P(u,v)=2uv+2u+2v$ for all real $u,v$.
background
Phase 3 of the ledger-to-factorization bridge asks that the T4-to-T5 step be derived from the recognition ledger rather than assumed analytically. The free ledger already supplies unconditional additivity of defect costs. What remains is an algebraic condition on a two-variable combiner $P$ so that the d'Alembert factorization gate fires and forces the Recognition Composition Law polynomial.
Primitive ledger-posting semantics is the ledger-native surface: the second coordinate is fed by actual free-defect ledger costs, posting is additive, and $P$ is symmetric with boundary $P(u,0)=2u$ and unit diagonal $P(1,1)=6$. The canonical target is the RCL combiner $\mathrm{rclCombiner}(u,v)=2uv+2u+2v$, which satisfies the full factorization gate.
Ledger-linear response is the completed real condition that turns the gate on. Upstream, primitive posting plus a global monotone response already produces that linear-response package; a separate theorem then routes linear response through the gate to RCL identity. No continuity or completeness hypotheses appear: only free-ledger additivity and order regularity.
proof idea
Pure term composition of two prior results. First apply ledgerLinearResponse_from_primitiveLedgerPosting_monotone to the given primitive-posting package and the global-monotone hypothesis; that yields a full LedgerLinearResponse record (symmetry, boundary, unit diagonal, and real-linear response in the second argument). Then feed that record into ledgerLinearResponse_forces_rcl, which builds the factorization gate from linear response and rewrites through gate_forces_rcl to obtain pointwise equality with rclCombiner. No new algebra is done at this site.
why it matters
This closes one order-regular route from free-ledger posting to the canonical RCL combiner, the algebraic heart of the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$ and the T5 J-uniqueness landmark. It isolates the precise remaining condition named in the module brief: free-ledger additivity plus monotone response, with no analytic continuity input.
Honesty note from the upstream monotone-to-linear-response lemma: global monotonicity is vacuous against the unrestricted real target, because RCL response slopes $2(u+1)$ go negative for $u<-1$. The result is non-vacuous on the physical cost cone $u\ge -1$, and is kept as a special case and proof component of the directional (monotone-or-antitone per slice) route. No downstream consumers are recorded yet; the declaration stands as a named bridge lemma inside the Phase-3 ledger-to-factorization file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.