booleanTruncation_add_eq_or
plain-language theorem explainer
Boolean OR on the two-state T0 floor is induced by adding natural generator counts and truncating back to {0,1}. Anyone deriving the Boolean recognition floor from the free defect ledger would cite this. The proof is a short case split on vanishing summands, then simplification.
Claim. For all $m,n\in\mathbb{N}$, the Boolean truncation of $m+n$ equals the logical OR of the truncations of $m$ and of $n$. Equivalently, after collapsing positive generator counts to the true state of the T0 floor, $m+n$ is present if and only if at least one of $m$ or $n$ is present.
background
The module Recognition Ledger Floor closes two genuine gaps from the T-1/T0 audit: the kernel gap (observable equivalence must be the cost kernel, not an external setoid) and the cokernel gap (independent defects must accumulate with multiplicity). The carrier is the free commutative monoid of finitely supported multiplicity maps, with unconditional additive ledger cost under a strictly positive weight.
Boolean truncation is the map that sends generator count $0$ to the absent/false state and every positive count to the present/true state. Under unit weight, the classical two-state Boolean floor of T0 is exactly this truncation of the free ledger. The present lemma records how addition on counts projects to OR on that floor.
Upstream cost notions (J-cost on recognition events, multiset ratio costs, multiplicative-recognizer derived cost) supply the broader cost language; here only the discrete monoid floor is in play.
proof idea
Unfold Boolean truncation. Case on whether $m=0$. If so, substitute and simplify: the claim reduces to truncation of $n$ equaling false OR truncation of $n$. Otherwise case on whether $n=0$: truncation of $m$ equals truncation of $m$ OR false. In the remaining branch both summands are nonzero, so $m+n\neq 0$ by omega, and both sides simplify to true.
why it matters
This pins down that OR on the T0 Boolean floor is not a primitive logical gadget but the shadow of ordinary addition of generator counts after truncation to ${0,1}$. That is the discrete half of answering the cokernel/multiplicity critique: the free ledger adds with multiplicity, and the Boolean floor is what remains once multiplicity is collapsed to presence.
The module narrative ties the Boolean floor to unit-weight truncation of the free additive object (boolean_floor_is_truncation). Sibling results (ledgerCost_add, two_independent_same_defects, kernel setoid from cost) handle the continuous/weighted side; this lemma is the pure Boolean identity those stories rely on. Framework landmark: T0 two-state floor as derived truncation, not an ad-hoc base type. The dependency graph currently lists no downstream users, so it is infrastructure awaiting the floor-identification theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.