booleanTruncation
plain-language theorem explainer
Maps a natural-number multiplicity to a Boolean: zero becomes false and any positive count becomes true. Downstream T0-bridge results cite it as the rank-one shadow that recovers the two-state floor from the free defect ledger. The body is a one-line decidable inequality test.
Claim. Define the Boolean truncation of a natural number $n$ by $\mathrm{trunc}(n) = \mathsf{false}$ if $n = 0$ and $\mathrm{trunc}(n) = \mathsf{true}$ if $n \ge 1$. Equivalently, $\mathrm{trunc}(n)$ is the truth value of the predicate $n \neq 0$.
background
The Recognition Ledger Floor module answers the T-1/T0 audit gaps by taking the free commutative monoid of defect multiplicities, $\mathrm{DefectLedger}, I := I \to_0 \mathbb{N}$, with additive cost under a strictly positive weight. Multiplicity is first-class: two independent copies of the same primitive distinction cost twice the weight, so the Boolean floor is no longer forced by excluding $(true,true)$ from independence.
The two-state T0 floor is recovered as a truncation of this extensive ledger under unit weight on a single generator. Boolean truncation is exactly that map on generator counts: it collapses every positive multiplicity to the single marked Boolean state and leaves zero unmarked. Sibling lemmas record that addition of counts induces Boolean OR after truncation, and that the map is constantly true on $\mathbb{N}_{>0}$.
proof idea
Definitional one-liner: evaluate the decidable proposition $n \neq 0$ and return the resulting Boolean. No lemmas are applied; decide discharges the Prop-to-Bool conversion.
why it matters
This is the concrete link between the free additive ledger and the classical T0 two-state floor. The bridge theorems use it directly: on a single primitive distinction the ledger shadow equals Boolean truncation of the multiplicity; under unit weight the transported T0 cost is Boolean recognition cost composed with this truncation; and the shadow lift is surjective onto the floor, so every floor state is genuinely a ledger shadow.
Those facts assemble into the Phase-2 identification certificate that exhibits T0 as the surjective two-state truncation of the extensive recognition ledger (specialised to Unit and weight 1). In the forcing chain this closes the cokernel/multiplicity side of the T0 audit without reimposing an external setoid: the Boolean floor is derived, not postulated. Locally it also feeds the OR-compatibility and positivity simp lemmas that make the truncation algebra usable in later proofs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.