rclCombiner_directional
plain-language theorem explainer
For each fixed first cost u, the canonical RCL combiner is monotone in posted mass v when u ≥ −1 and antitone when u ≤ −1. Anyone closing the ledger-to-factorization bridge via the directional order route cites this as the non-vacuity witness that the forced combiner itself satisfies the directional hypothesis. The proof is a two-branch real inequality: case on the sign of u+1 and finish with nlinarith.
Claim. Let $C(u,v) := 2uv + 2u + 2v$ be the canonical RCL combiner on $\mathbb{R}$. Then for every fixed $u \in \mathbb{R}$, the partial map $v \mapsto C(u,v)$ is either monotone or antitone: monotone whenever $u \ge -1$, and antitone whenever $u \le -1$.
background
This module builds the Phase-3 bridge from the recognition ledger to d'Alembert factorization (the T4-to-T5 step). The free ledger already gives unconditional additivity; the remaining algebraic demand is that a two-variable combiner have ledger-linear response in its second argument, so that the gate's rightAffine field follows and, with symmetry, boundary law, and unit diagonal, forces the RCL polynomial.
The canonical combiner is $C(u,v) = 2uv + 2u + 2v$, the bilinear form appearing on the right-hand side of the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. Ledger posting semantics ask how cost responds when defect mass $v$ is posted against a fixed first cost $u$. Global monotonicity and global non-negativity of that response hold only on the physical cone $u \ge 0$; the directional route weakens the order hypothesis to "monotone or antitone in $v$ for each fixed $u$".
proof idea
Term-mode proof by cases on the sign of $u+1$. Fix $u$. If $u+1 \ge 0$, prove monotonicity: for $a \le b$, unfold $C$ and apply nlinarith to the non-negative product $(u+1)(b-a)$. If $u+1 < 0$, prove antitonicity the same way, using the non-negative product $-(u+1)\cdot(b-a)$. No external lemmas beyond basic ordered-field facts.
why it matters
This is the non-vacuity witness for the directional order route into RCL. The doc-comment states it discharges the directional hypothesis of the directional forcing theorem, so that route is a genuine closure rather than an empty implication. Global-monotone and global-nonneg routes only live on the physical cost cone $u \ge 0$; here the forced combiner itself is directionally monotone for every real $u$, including the non-physical half-line.
Downstream it sits under the ledger-to-factorization forcing chain that recovers the canonical RCL combiner from primitive ledger posting (used by the nonneg forcing theorem in this module, and intended for the directional sibling). That combiner is exactly the algebraic content of T5 J-uniqueness in the forcing chain: once right-affineness is ledger-derived, the existing factorization gate yields the RCL polynomial and thereby $J(x)=\cosh(\log x)-1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.