rclCombiner_postingNonneg
plain-language theorem explainer
On the physical cost cone, the canonical RCL combiner never falls when non-negative ledger mass is posted in the second slot. Anyone verifying that the ledger non-negativity forcing route is inhabited by the intended combiner cites this. The proof unfolds the combiner polynomial and closes by nonlinear arithmetic from product non-negativity.
Claim. Let $C$ be the canonical RCL combiner. For all real $u,v$ with $u \ge 0$ and $v \ge 0$, one has $C(u,0) \le C(u,v)$: posting non-negative second-slot mass never lowers the combined cost when the first cost is non-negative.
background
This module isolates the remaining algebraic condition in the Phase-3 bridge from the recognition ledger to d'Alembert factorization (T4 to T5). The free ledger already gives unconditional additivity; if a two-variable combiner has ledger-linear response in its second argument, the rightAffine field of the factorization gate follows, and with symmetry, boundary law, and unit diagonal the gate forces the RCL polynomial.
The Recognition Composition Law (RCL) is the functional identity $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$ that uniquely characterizes the J-cost $J(x)=(x+x^{-1})/2-1$ (forcing step T5). The canonical combiner is the two-variable polynomial realizing that identity on cost values. Recognition costs live on the cone $u \ge 0$ (J is non-negative), so ledger-native posting hypotheses are checked there rather than by analytic continuity.
proof idea
Tactic proof in three steps: introduce $u,v$ and the two non-negativity hypotheses; unfold the definition of the canonical RCL combiner; discharge the resulting polynomial inequality by nlinarith, feeding mul_nonneg on each hypothesis twice so the cross terms are known non-negative. No external lemmas beyond the combiner definition and basic real arithmetic.
why it matters
Feeds ledgerLinearResponse_from_primitiveLedgerPosting_monotone, which upgrades primitive ledger posting plus a global monotone response to full real ledger-linear response. The downstream doc warns that global monotonicity is vacuous for the target combiner off the physical cone (RCL slope $2(u+1)$ is negative for $u<-1$); this lemma shows the non-negativity route is nevertheless non-vacuous on $u\ge 0$ and is satisfied by the intended combiner, with regularity grounded in ledger cost non-negativity rather than continuity.
In the forcing chain this is a ledger-native witness that the T5 RCL polynomial is reachable from posting semantics, not only from analytic inputs. It is the special-case companion to the directional (monotone-or-antitone per slice) route that closes the order argument without vacuity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.