ledgerShadow_single
plain-language theorem explainer
On a single-support ledger entry Finsupp.single i₀ n, the Boolean shadow equals the Boolean truncation of the multiplicity n. Anyone identifying the T0 floor cost with clamped ledger cost on a rank-1 distinction cites this. The proof is a two-case split on n = 0, using the zero and nonzero characterizations of the shadow.
Claim. For any index type $I$, any $i_0 \in I$, and any $n \in \mathbb{N}$, the Boolean shadow of the finitely supported ledger that posts multiplicity $n$ only at $i_0$ equals the Boolean truncation of $n$: false when $n = 0$, true when $n > 0$.
background
This module identifies the T0 floor with the Boolean truncation of the extensive recognition ledger. The extensive ledger is DefectLedger I = I →₀ ℕ (finitely supported multiplicities). Its Boolean shadow is false exactly on the zero ledger and true as soon as any recognition is posted: ledgerShadow Γ := if Γ = 0 then false else true. The lift ledgerToFloor sends that shadow into the distinction-forced observable quotient ForcedQuotient h ≃ Bool.
Boolean truncation is the map ℕ → Bool that sends 0 to false and every positive natural to true. A single-support ledger Finsupp.single i₀ n is the free generator that posts multiplicity n at one primitive distinction and zero elsewhere. Upstream, ledgerShadow_zero and ledgerShadow_eq_true_iff give the two-sided characterization of the shadow on the zero and nonzero ledgers; those are the only facts needed here.
proof idea
Case split on whether n = 0.
If n = 0, substitute to get Finsupp.single i₀ 0 = 0, then rewrite by ledgerShadow_zero and booleanTruncation_zero.
If n ≠ 0, first show Finsupp.single i₀ n ≠ 0 via Finsupp.single_eq_zero, then apply ledgerShadow_eq_true_iff.mpr on the left and booleanTruncation_pos on the right. Both sides become true.
why it matters
This is the rank-1 specialization that makes the cost-truncation claim concrete. Downstream, rank1_cost_is_boolean_truncation uses it to prove that on a single primitive distinction with unit weight, the T0 floor cost is literally boolRecognitionCost ∘ booleanTruncation of the natural multiplicity.
That identity is one of the four legs of the bundled LedgerFloorT0Bridge theorem: the T0 floor is a surjective cost-and-join homomorphism from the extensive ledger, and on rank 1 the floor cost is exactly the two-state clamp of the ledger cost. The module closes the Phase 2 audit gap that previously left T0 as a chosen Boolean indicator rather than the shadow of an extensive cost object. In the forcing chain this sits at the T0 floor, before T5 J-uniqueness and the later phi and dimension forcings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.