ledgerShadow_eq_false_iff
plain-language theorem explainer
The Boolean shadow of a defect ledger is false exactly when the ledger is empty. Anyone identifying the T0 floor with a truncation of the extensive recognition ledger cites this kernel fact. The proof unfolds the if-then definition and splits on whether the ledger is zero.
Claim. For any index type $I$ and any defect ledger $\Gamma : I \to_0 \mathbb{N}$, the Boolean shadow of $\Gamma$ equals $\mathsf{false}$ if and only if $\Gamma = 0$.
background
In Recognition Science the T0 floor is the two-state recognition cost forced by a distinction: the observable quotient is Boolean, and cost is the indicator that something nonzero has been recognized. Separately, the extensive recognition ledger is the free commutative monoid $\mathrm{DefectLedger}, I = I \to_0 \mathbb{N}$ of finitely supported multiplicities of primitive distinctions, with additive cost given by weighted total multiplicity.
This module supplies the missing truncation that makes the T0 floor the shadow of that ledger. The shadow map sends a ledger to $\mathsf{false}$ on the empty ledger and $\mathsf{true}$ as soon as any recognition has been posted. The present lemma is the exact characterization of the false fiber of that map.
Upstream, $\mathrm{DefectLedger}$ is the free commutative monoid on $I$; the shadow is defined by a single case split on emptiness. Downstream packaging uses this fiber fact when proving the monoid homomorphism and cost-kernel properties of the bridge.
proof idea
Term-level case analysis on the definition. Unfold the shadow (if $\Gamma = 0$ then false else true). Split on whether $\Gamma = 0$; in each branch simp discharges the biconditional against the corresponding branch of the definition. No external lemmas are required beyond definitional unfolding and Boolean equality simplification.
why it matters
Closes part of the Phase-2 audit gap: T0 must be the Boolean truncation of an extensive cost object, not an ad-hoc indicator on an unrelated carrier. The parent theorem ledger_floor_t0_bridge packages the full bridge (monoid homomorphism onto the T0 join, cost truncation to ${0,1}$, surjectivity, and kernel identification). This lemma is the false-fiber half of that kernel story: shadow false exactly on the zero ledger, so two ledgers share the empty shadow precisely when both have zero extensive cost.
In the forcing chain this anchors T0 as the genuine shadow of the ledger rather than a chosen Boolean. It does not itself force $\phi$, the eight-tick octave, or $D=3$; those sit later (T5–T8). It is the elementary kernel step that lets the extensive ledger project cleanly onto the T0 floor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.