ledgerCost_add
plain-language theorem explainer
Unconditional additivity of the weighted recognition cost on the free defect ledger: cost of a sum equals the sum of costs, with no independence side-condition. Anyone citing ledger posting, order-faithfulness, or the factorization gate toward RCL needs this fact. The public name is a one-line re-export of the foundation lemma.
Claim. For any index type $I$, weight $w:I\to\mathbb{R}$, and free defect ledgers $\Gamma,\Delta$ (finitely supported $I\to\mathbb{N}$), the weighted recognition cost satisfies $\mathrm{cost}_w(\Gamma+\Delta)=\mathrm{cost}_w(\Gamma)+\mathrm{cost}_w(\Delta)$.
background
The Ledger Floor module is the public aggregator for the extensive recognition ledger and its Boolean T0 shadow. The free ledger is the commutative monoid $\mathrm{DefectLedger},I=I\to_0\mathbb{N}$ of finitely supported multiplicity assignments on primitive distinctions. The weighted cost sums $w(i)$ against those multiplicities; it is the ledger-level avatar of the J-cost / defect functional used elsewhere in the stack (observer events, multiplicative recognizers, PRC ratio orbits).
Module framing stresses that additivity here is unconditional: no auxiliary "independence" relation is required to split cost across a sum of ledgers. That is the contrast with gerrymandered independence hypotheses that would otherwise smuggle structure into the cost law. The T0 Boolean floor is later recovered as a truncation (two-state shadow) of this extensive ledger when weights are strictly positive on witnessed distinctions.
proof idea
One-line public abbrev: it aliases the already-proved foundation statement RecognitionLedgerFloor.ledgerCost_add (explicit universe/args via @). No local argument is replayed; the mathematical content and proof live in the foundation module this aggregator re-exports.
why it matters
This is the citation handle the core-theory PDF and downstream factorization layer use for free-ledger linearity. In LedgerToFactorization it is the algebraic engine behind ledgerCost_le_add_right (order-faithfulness: non-negative weights never decrease cost when defect mass is added), which supplies the order shadow for the non-negativity route into the factorization associativity gate. The same additivity is named explicitly in the directional forcing path: primitive ledger posting plus per-slice monotone/antitone regularity forces the canonical RCL combiner, with additivity coming from this lemma.
That lands on Phase-3 obligations linking ledger-linear response to the Recognition Composition Law polynomial, and on specialization theorems that turn primitive posting into discrete rank-one posting. Framework-wise it is the extensive-cost half of the ledger-to-T0 identification story (T0 Boolean floor as quotient shadow), not a substitute for J-uniqueness (T5) or the phi fixed point (T6).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.