unit_cost_is_generator_count
plain-language theorem explainer
Under unit weight, the recognition cost of n copies of one primitive distinction equals the integer n itself. Anyone wiring the free ledger into a cost-function abstraction, or specializing primitive postings to discrete rank-one ledgers, cites this identity. The proof is a one-line term reusing the Boolean-floor truncation lemma.
Claim. For any primitive distinction index $i$ and any $n \in \mathbb{N}$, if the weight is identically $1$, then the ledger cost of the finitely supported configuration with multiplicity $n$ only at $i$ equals $n$ as a real: $\mathrm{cost}_{w \equiv 1}(n \cdot e_i) = n$.
background
The module constructs the free additive cost floor on the carrier of finitely supported maps $I \to \mathbb{N}$ (the free commutative monoid of multiset configurations of primitive distinctions). Recognition cost under a weight $w$ is the total weighted multiplicity: sum over support of $n_i \cdot w(i)$. This is the object that closes the T-1/T0 audit cokernel gap: independent defects accumulate with multiplicity, so one need not gerrymander the independence relation to dodge $1=2$.
Under unit weight $w \equiv 1$, cost collapses to raw generator count. The Boolean two-state floor of T0 is the $n \in {0,1}$ truncation of the same object. Upstream, the unit-weight single-support identity is already recorded as the Boolean-floor truncation lemma, whose statement matches this theorem exactly.
proof idea
One-line term-mode wrapper. The goal is definitionally identical to the Boolean-floor truncation lemma, so the proof is just that lemma applied at $i$ and $n$. The underlying computation (inside the named lemma) rewrites the single-support ledger cost and closes by ring arithmetic: multiplicity $n$ at one index under weight $1$ contributes $n \cdot 1 = n$.
why it matters
This is the unit-weight specialization that makes generator count the literal cost of a pure rank-one ledger entry. Downstream it feeds the specialization of primitive ledger posting semantics to the natural-number rank-one surface (discrete posting from primitive posting). In the Recognition framework it underwrites assembly of the free ledger into the existing cost-from-distinction abstraction with the universal independence relation, closing audit Loopholes 8 and 9: multiplicity is represented, so universal independence stays consistent with additivity. It also anchors the Boolean T0 floor as the ${0,1}$ shadow of the unrestricted free-monoid floor rather than a separate primitive.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.