ledgerShadow_eq_true_iff
plain-language theorem explainer
The Boolean shadow of a defect ledger is true exactly when the ledger is nonzero. Anyone identifying the T0 floor with the truncation of the extensive recognition ledger cites this equivalence. The proof unfolds the shadow definition and splits on whether the ledger vanishes.
Claim. For any index type $I$ and defect ledger $\Gamma : I \to_0 \mathbb{N}$, the Boolean shadow of $\Gamma$ equals $\mathsf{true}$ if and only if $\Gamma \neq 0$.
background
This module identifies the T0 floor with the Boolean truncation of the extensive recognition ledger. Before it, DistinctionToT4 built T0 as a two-state cost on the forced quotient of a distinction, while RecognitionLedgerFloor built the free commutative monoid DefectLedger I = I →₀ ℕ of finitely supported multiplicities, with no formal link between them.
The shadow map sends a ledger to false on the empty ledger and true as soon as any recognition has been posted: it is the truncation of ℕ-valued multiplicity to the two-state floor. The lift of that shadow through the forced-quotient Bool equivalence is the truncation map whose target is the distinction-generated observable quotient.
The local goal is to prove that this map is a monoid homomorphism onto the T0 join, a cost truncation to {0,1}, surjective onto the floor, and a cost-kernel identification.
proof idea
Unfold the definition of the shadow (the if-then-else on vanishing). Case-split on whether Γ equals zero. In each branch, simp with the case hypothesis closes the biconditional: the zero branch gives false ↔ false, the nonzero branch true ↔ true.
why it matters
This is the nonzero half of the shadow characterization that makes the T0 floor a genuine quotient of the extensive ledger. It is used by the bundled Phase-2 bridge ledger_floor_t0_bridge (the identification for every distinction witness and strictly positive weight), by ledgerShadow_single (shadow of a single primitive equals Boolean truncation of its multiplicity), and by ledgerToFloor_surjective (every floor state is hit, so nothing on the floor is unhit).
In the forcing chain this closes the audit gap that T0 was a chosen Boolean indicator rather than the shadow of an extensive cost object. It sits at the ledger-to-T0 interface before T5 J-uniqueness and the later phi-forcing steps; it does not itself force J, phi, or dimension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.