primitiveLedgerPosting_nonneg_forces_rcl

Phase 3 of the foundation asks that the T4-to-T5 bridge be derived from the recognition ledger rather than taken as an analytic input. This module isolates the remaining algebraic condition: free-ledger additivity is already unconditional; if a combiner has the matching ledger-linear response in its second argument, the d'Alembert factorization gate (with symmetry, boundary law, and unit diagonal) forces the RCL polynomial.

Primitive ledger-posting semantics is the Phase-2-close surface: the second coordinate is fed by actual free defect-ledger costs, and additive posting of ledgers is the operation the combiner sees. The four fields are symmetry, $P(u,0)=2u$, $P(1,1)=6$, and right-additivity of excess cost under $\Gamma+\Delta$. The canonical target is the RCL combiner $P(u,v)=2uv+2u+2v$, the polynomial form of the Recognition Composition Law.

The only order input here is global posting non-negativity: non-negative defect mass never lowers cost. That is the order shadow of ledger-cost non-negativity. Upstream, the same non-negativity hypothesis upgrades primitive posting to full real ledger-linear response; a separate gate theorem then forces equality with the RCL combiner.

Term-mode two-step composition, no local tactics. First apply the upstream lemma that primitive posting plus global non-negativity yields ledger-linear response (via the monotone route: non-negativity implies monotonicity in the posted coordinate, then monotone additive response is linear). Feed that LedgerLinearResponse witness into the gate theorem that any ledger-linear response forces $P$ equal to the RCL combiner pointwise. The body is exactly that composition.

Closes a fully ledger-internal route from primitive posting data to the canonical RCL combiner, which is the algebraic content of T5 (J-uniqueness / Recognition Composition Law) in the forcing chain. The module goal is precisely this T4-to-T5 bridge: free-ledger additivity plus linear response yields the rightAffine field of the factorization gate, and with symmetry, boundary, and unit diagonal the gate forces the RCL polynomial.

No downstream consumers are wired yet (used_by is empty); the declaration is a terminal packaging of the non-negativity route. Honesty note from the upstream non-negativity lemma: the global hypothesis $P(u,0)\le P(u,v)$ for all $u$ and $v\ge 0$ is vacuous for the target combiner when $u<-1$; it holds on the physical cost cone $u\ge 0$. The non-vacuous global closure is the directional-regularity sibling. Still, as a proved packaging theorem it records that the ledger-native order shadow of cost non-negativity is enough, on its stated domain, to force RCL.