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; the Boolean T0 floor is that unit-weight truncation of the extensive ledger. Public aggregator alias of the Foundation theorem of the same name. Citation target for anyone identifying the T0 two-state shadow with ledger multiplicity. The body is a one-line re-export of the proved Foundation result.
Claim. Under the constant unit weight $w\equiv 1$, the ledger cost of $n$ copies of a single primitive distinction $i$ equals the generator count: $\mathrm{ledgerCost}(1,\, n\cdot e_i)=n$. Equivalently, the Boolean two-state T0 floor is the unit-weight truncation of the extensive recognition ledger (clamp of multiplicity to $\{0,1\}$).
background
The LedgerFloor module is the public aggregator for the ledger-floor layer cited by the core-theory PDF: the free additive recognition ledger $\mathrm{DefectLedger},I=I\to_0\mathbb{N}$ (finitely supported multiplicity of primitive distinctions), its weighted recognition cost, and the identification of the T0 Boolean floor as the two-state shadow of that extensive ledger.
Recognition cost on the ledger is additive without any independence side-condition. Under a general weight $w:I\to\mathbb{R}$, cost of a Finsupp is the weighted sum of multiplicities. The unit-weight specialization $w\equiv 1$ makes cost equal raw generator count, which is exactly the Boolean truncation story: zero multiplicity is false, any positive multiplicity is true.
Upstream cost notions (J-cost on recognition events, derived cost of multiplicative recognizers, rung-coarsen multiset cost) supply the broader recognition-cost language; this declaration specializes to the ledger's unit-weight case.
proof idea
Public one-line abbrev that re-exports Foundation.RecognitionLedgerFloor.boolean_floor_is_truncation. The underlying theorem is itself a short calculation: rewrite the single-support ledger cost via ledgerCost_single, then close by ring, yielding $\mathrm{ledgerCost}(1,\mathrm{single},i,n)=n$. No extra hypotheses.
why it matters
Pins the slogan that the Boolean T0 floor is the unit-weight truncation of the extensive ledger. Downstream, unit_cost_is_generator_count is a direct one-line application of this fact, and the bundled bridge ledger_floor_t0_bridge / certificate ledger_t0_identification_certificate package the stronger claim that the truncation map is a surjective cost-and-join homomorphism from the ledger onto the distinction-generated T0 floor.
In the forcing chain this sits at the T0 Boolean recognition layer: the two-state shadow of extensive multiplicity, before the higher T-steps (J-uniqueness, phi, eight-tick, D=3). It closes the Phase-2 identification that T0 is a genuine quotient (shadow) of the free ledger rather than an independent primitive.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.