boolean_floor_is_truncation
plain-language theorem explainer
Under unit weight, the recognition cost of n copies of one primitive distinction equals the natural number n itself. Anyone identifying the Boolean T0 floor as a truncation of the free additive ledger cites this identity. The proof is a one-line rewrite through the single-defect cost formula, then ring normalization of n·1 = n.
Claim. For any primitive distinction index $i$ and multiplicity $n \in \mathbb{N}$, the ledger cost of the finitely supported spike sending $i$ to $n$ (and all other indices to zero), evaluated at the constant unit weight $w \equiv 1$, equals $n$ as a real: $\mathrm{cost}_{w\equiv 1}(\delta_i^{\oplus n}) = n$.
background
The module closes two genuine gaps from the T-1/T0 audit (the Anil critique): the kernel gap (observable equivalence must be the kernel of cost, not an external setoid) and the cokernel gap (independent defects must accumulate additively with multiplicity). The carrier is the free commutative monoid of finitely supported multiplicity maps on a type $I$ of primitive distinctions, $\mathrm{DefectLedger}, I := I \to_0 \mathbb{N}$.
Recognition cost under a weight $w$ is the total weighted multiplicity: $\mathrm{ledgerCost}, w, \Gamma = \sum_i n_i \cdot w(i)$. The upstream single-defect lemma states that a pure spike of multiplicity $n$ at $i$ costs exactly $n \cdot w(i)$. The Boolean two-state floor of T0 is the $n \in {0,1}$ truncation of this object under unit weight; the present identity is the unrestricted unit-weight case for arbitrary $n$.
proof idea
One-line term proof. Rewrite by the single-defect cost lemma, which specializes the left-hand side to $(n:\mathbb{R})\cdot w(i)$ at the constant weight $w\equiv 1$, hence to $n\cdot 1$. Then ring normalizes $n\cdot 1 = n$. No induction, case split, or positivity hypothesis is required.
why it matters
This is the explicit unit-weight specialization that makes the Boolean T0 floor the truncation of the free ledger, as the module doc states. Downstream, unit_cost_is_generator_count is literally this statement (one-line application), and the LedgerFloor package re-exports the result as the Boolean shadow of the ledger. It discharges the cokernel gap: multiplicity is represented on the nose, so two independent copies of the same defect cost $2$ rather than collapsing under a Boolean clamp. In the forcing chain this sits at T0, the two-state recognition floor, before J-uniqueness (T5) and the self-similar fixed point $\varphi$ (T6).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.