booleanTruncation_pos
plain-language theorem explainer
Any positive natural-number multiplicity truncates to the Boolean value true. Bridging work from the free defect ledger down to the classical two-state T0 floor cites this as a simp fact. The proof is a one-line unfolding of the truncation definition against the positivity hypothesis.
Claim. If $n\in\mathbb{N}$ satisfies $n\neq 0$, then the Boolean truncation of $n$ equals $\mathsf{true}$: every positive generator count is sent to the occupied Boolean state.
background
The Recognition Ledger Floor module answers the two genuine gaps from the T-1/T0 audit (kernel of cost vs imposed setoid; additive multiplicity of independent defects). Its carrier is the free commutative monoid DefectLedger I := I →₀ ℕ of finitely supported generator counts, equipped with an additive cost under a strictly positive weight.
Boolean truncation is the shadow that collapses a natural-number multiplicity to a two-state bit: zero maps to false, and every positive count maps to true. The module records that the classical Boolean floor of T0 is exactly this {0,1} truncation of the free ledger under unit weight.
The present lemma is the positive half of that truncation identity; the zero half is the companion fact that truncation of zero is false.
proof idea
One-line term/tactic proof: simp unfolds the definition of Boolean truncation (which is decide (n ≠ 0)) and rewrites with the hypothesis n ≠ 0, yielding true.
why it matters
Downstream, ledgerShadow_single in the LedgerFloorT0Bridge uses this fact to identify the ledger shadow of a single primitive distinction with the Boolean truncation of its multiplicity. That bridge is how the free additive ledger (the object that closes the kernel and cokernel gaps of the Anil critique) recovers the classical two-state T0 floor rather than replacing it. In the forcing chain, T0 is the Boolean recognition floor; this lemma is a tiny but necessary piece of the truncation map that exhibits T0 as a shadow of the richer natural-number ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.