ledgerCost_add
plain-language theorem explainer
The recognition cost of a free defect ledger is strictly additive: cost of Γ+Δ equals cost of Γ plus cost of Δ, for any weight and any pair of finitely supported multiplicity maps. Anyone working the cokernel gap or the ledger-to-RCL bridge cites this. The proof is a short Finsupp sum-index argument after unfolding the weighted sum.
Claim. For any index type $I$, any weight $w:I\to\mathbb{R}$, and any two defect ledgers $\Gamma,\Delta$ (finitely supported maps $I\to\mathbb{N}$), the weighted ledger cost satisfies $\mathrm{cost}_w(\Gamma+\Delta)=\mathrm{cost}_w(\Gamma)+\mathrm{cost}_w(\Delta)$.
background
The Recognition Ledger Floor module answers the T-1/T0 audit's two real gaps: the kernel gap (observable equivalence should be the kernel of cost) and the cokernel gap (independent defects must accumulate with multiplicity). The carrier is the free commutative monoid on primitive distinctions, DefectLedger I := I →₀ ℕ, i.e. finitely supported multiplicity maps.
Ledger cost under a per-distinction weight $w$ is the total weighted multiplicity: sum over the support of $n_i\cdot w(i)$. Because the monoid operation is pointwise addition of multiplicities, additivity of cost is the natural algebraic property that closes the cokernel gap: two independent copies of the same defect cost $2w(i)$, with no restricted independence relation needed.
Upstream cost notions (J-cost on ratios, observer-event cost, multiplicative-recognizer derived cost) all specialize or motivate the weight $w$; this lemma is the free-monoid floor beneath those specializations.
proof idea
Unfold the definition of ledger cost to a Finsupp sum of $n\mapsto n\cdot w(i)$. Apply Finsupp.sum_add_index': the zero-coefficient branch is immediate by simp, and the two-coefficient branch reduces by push_cast and ring to the identity $(a+b)\cdot w(i)=a\cdot w(i)+b\cdot w(i)$. No positivity or independence hypothesis is used.
why it matters
Unconditional additivity is the module's answer to audit Loophole 9 (cokernel gap): independent defects accumulate additively with multiplicity, so the Boolean two-state floor is merely the $n\in{0,1}$ truncation rather than a forced restriction of independence. Downstream, ledgerCost_le_add_right is the direct order consequence (additivity plus non-negativity), and that order shadow feeds the non-negativity route to the factorization gate.
In LedgerToFactorization, primitive ledger posting plus directional regularity forces the canonical RCL combiner; the docs explicitly credit additivity to this lemma. That lands on the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$, the algebraic identity behind T5 J-uniqueness in the forcing chain. The lemma is therefore a foundation brick between the free ledger floor and the RCL/factorization bridge, not a cosmetic rewrite.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.