booleanTruncation_zero
plain-language theorem explainer
The Boolean truncation of multiplicity zero is false. Anyone bridging the free defect ledger to the T0 two-state floor cites this base identity when matching single-generator shadows. The proof is a one-line simp unfolding of the truncation definition.
Claim. Under the Boolean shadow that sends a natural multiplicity $n$ to $\mathrm{false}$ exactly when $n=0$ (and to $\mathrm{true}$ for every positive count), one has $\mathrm{trunc}(0)=\mathrm{false}$.
background
The Recognition Ledger Floor module supplies the free additive cost carrier that closes the T-1/T0 audit gaps: the kernel gap (observable equivalence derived from cost) and the cokernel gap (independent defects accumulate with multiplicity). The carrier is the free commutative monoid DefectLedger I := I →₀ ℕ with cost ledgerCost w for a strictly positive weight.
Boolean truncation is the shadow of a natural generator count onto two states: zero maps to false, any positive multiplicity to true. It is the n ∈ {0,1} cut that recovers the classical T0 Boolean floor from the free ledger under unit weight.
Upstream, the definition is simply decide (n ≠ 0). This lemma records the zero case of that decision.
proof idea
One-line wrapper: simp [booleanTruncation] unfolds the definition decide (n ≠ 0) at n = 0, which reduces to false by the decision procedure for natural inequality.
why it matters
Feeds ledgerShadow_single in the T0 bridge: on a single primitive distinction the ledger shadow equals the Boolean truncation of the multiplicity, and the zero case of that proof rewrites through this identity after Finsupp.single_zero and ledgerShadow_zero.
In the module narrative, the two-state Boolean floor of T0 is exactly the truncation of the free ledger under unit weight (boolean_floor_is_truncation). Pinning trunc(0) = false is the base case that keeps the shadow honest at the empty ledger, so the free monoid genuinely specializes to the classical two-state floor rather than inventing a third state or collapsing zero into true.
No open scaffolding: status is proved with zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.