two_independent_same_defects
plain-language theorem explainer
Two independent unit copies of one defect cost twice the weight, not once: multiplicity is genuinely represented on the free recognition ledger. Cite this when arguing that the extensive ledger needs no gerrymandered independence relation to avoid a 1=2 collapse. The local declaration is a one-line public re-export of the proved additivity identity in the foundation module.
Claim. For any weight $w$ on the index of primitive distinctions and any distinction $i$, the recognition ledger cost of two independent unit postings of $i$ equals $2\,w(i)$: $\mathrm{cost}_w(\mathbf{1}_i+\mathbf{1}_i)=2\,w(i)$.
background
The Ledger Floor module is the public aggregator for the Boolean shadow of the extensive recognition ledger. The carrier is the free commutative monoid of finitely supported natural multiplicities on a type $I$ of primitive distinctions (the defect ledger $I\to_0\mathbb{N}$). Recognition cost is the weighted sum of those multiplicities; additivity of cost is unconditional.
The foundation theorem this abbrev exposes is the cokernel fix: on that free carrier, posting the same defect twice really costs twice. The module doc lists this among the public citation targets precisely so that multiplicity is not collapsed by an independence side-condition. Upstream cost notions (J-cost of recognition events, multiplicative-recognizer derived cost, rung-coarsened multiset cost) all sit behind the same extensive-ledger reading of weight.
proof idea
Locally this is a one-line abbrev re-export of the foundation theorem. The underlying proof is a short algebraic reduction: rewrite by unconditional additivity of ledger cost and the single-support evaluation, then finish by ring arithmetic after a cast. No independence hypothesis is introduced or discharged.
why it matters
This is the multiplicity witness the core-theory PDF cites for the ledger floor: two independent copies cost $2wi$, not $wi$, so the free ledger needs no restriction of independence to avoid $1=2$. Downstream, recognition multiplicity of a $k$-face cell is defined as unit-weight ledger cost of the cell ledger and is proved equal to the face count $k$ by generalizing exactly this identity (additivity plus single-support evaluation), with no reference to the closure map. It also underwrites the T0 bridge package: the Boolean floor is a genuine cost-and-join shadow (quotient) of the extensive ledger rather than a vacuous two-state toy. In the forcing chain this sits under the T-1/T0 Boolean recognition cost that the module identifies as the public core slice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.