ledgerShadow
plain-language theorem explainer
The Boolean shadow of a defect ledger is false exactly on the empty ledger and true as soon as any recognition multiplicity is posted. It is the truncation of the free commutative monoid of finitely supported natural multiplicities down to a two-state floor. Anyone identifying the T0 recognition floor with an extensive ledger cites this map. The definition is a one-line case split on vanishing of the ledger.
Claim. For any index type $I$ and any defect ledger $\Gamma$ (a finitely supported map $I\to\mathbb{N}$), the ledger shadow is the Boolean value $\mathrm{shadow}(\Gamma)=\mathsf{false}$ if $\Gamma=0$ and $\mathsf{true}$ otherwise. Equivalently, it is the truncation of extensive multiplicity to the two-state floor: empty versus nonempty recognition.
background
A defect ledger is the free commutative monoid of finitely supported multiplicities of primitive distinctions: $\mathrm{DefectLedger},I=I\to_0\mathbb{N}$. Its extensive recognition cost is the weighted total multiplicity under a per-distinction weight. The empty ledger is the zero of that monoid.
Separately, the T0 floor arising from a distinction witness is a two-state observable quotient, equivalent to $\mathsf{Bool}$, whose recognition cost is a Boolean indicator. Before this module those two constructions sat side by side: an extensive $\mathbb{N}$-valued ledger and a Boolean T0 floor, with no formal truncation connecting them.
This definition supplies the missing shadow map. The module frames it as the Boolean truncation that makes the T0 floor the two-state shadow of the extensive ledger, closing the Phase-2 gap in the T-1-to-T8 audit (turning T0 from a chosen Boolean indicator into the shadow of an extensive cost object).
proof idea
Pure definition by case split: if the ledger equals zero, return false; otherwise return true. No lemmas are applied. Downstream simp lemmas (shadow of zero, false-iff-zero, true-iff-nonzero) are immediate unfoldings of this case split.
why it matters
This is the atomic truncation used by the whole LedgerFloorT0Bridge package. The lift ledgerToFloor is defined by transporting the shadow across the forced-quotient Boolean equivalence, so every monoid, cost, surjectivity, and kernel statement in the bundled bridge theorem factors through it.
Downstream, the shadow is shown to be a monoid homomorphism from ledger addition to Boolean OR, to agree with Boolean truncation of natural multiplicity on single generators, and to make the T0 recognition cost the clamp of extensive ledger cost to ${0,1}$. The Phase-2 identification theorem ledger_floor_t0_bridge packages those facts for every distinction witness and every strictly positive weight.
In the forcing chain this anchors T0: the two-state floor is no longer an ad hoc Boolean indicator but the genuine shadow of the extensive recognition ledger that later feeds cost uniqueness (T5 J-cost) and the rest of the chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.