ledgerCost_le_add_right
plain-language theorem explainer
For non-negative weights, free ledger cost never falls when defect mass is posted onto a ledger. Anyone routing the T4–T5 bridge through ledger-native non-negativity cites this order-faithfulness fact. The proof expands by unconditional additivity, then drops the non-negative summand by linear arithmetic.
Claim. Let $I$ be an index type and $w:I\to\mathbb{R}$ a family of non-negative weights. For defect ledgers $\Gamma,\Delta$ on $I$, the free ledger cost satisfies $C_w(\Gamma)\le C_w(\Gamma+\Delta)$.
background
The module isolates the remaining algebraic condition in the Phase-3 bridge from the recognition ledger to d'Alembert factorization (the T4-to-T5 step that forces the Recognition Composition Law). The free ledger already has unconditional additivity of cost under ledger sum. If a two-variable combiner has the matching ledger-linear response in its second argument, the rightAffine field of the factorization gate follows; with symmetry, boundary law, and unit diagonal, the gate forces the RCL polynomial.
Free ledger cost $C_w$ is the weighted sum of defect masses against weights $w$. Defect ledgers $\Gamma,\Delta$ are the floor-level posting objects. Two upstream facts pin the claim: cost is additive under ledger sum, and cost of any ledger is non-negative whenever every weight is non-negative.
proof idea
Rewrite the target inequality using additivity of free ledger cost, so the right-hand side becomes $C_w(\Gamma)+C_w(\Delta)$. Feed non-negativity of $C_w(\Delta)$ (under $w\ge 0$) into linear arithmetic to drop the second summand. Two tactic steps; no further structure is used.
why it matters
This is the ledger order-faithfulness anchor named in the doc-comment: posting non-negative defect mass never lowers free cost. Its order shadow is the non-negativity hypothesis on the non-negativity forcing route above, which the module uses to ground the T4-to-T5 bridge in ledger algebra rather than analytic continuity. That bridge is the path to T5 J-uniqueness (the RCL cost $J(x)=(x+x^{-1})/2-1$) via the d'Alembert factorization gate. A neighboring comment records that the canonical RCL combiner satisfies the corresponding posting non-negativity on the physical domain $u\ge 0$, with regularity input from cost non-negativity rather than continuity. No recorded downstream uses yet; the lemma is an internal anchor for that route.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.