ledgerShadow_zero

A defect ledger on an index type $I$ is a finitely supported map $I\to_0\mathbb{N}$: the free commutative monoid of multiplicities of primitive distinctions. Its extensive recognition cost is the weighted sum of those multiplicities.

The Boolean shadow of a ledger is the two-state truncation: $\mathsf{false}$ exactly on the empty ledger, $\mathsf{true}$ as soon as any recognition has been posted. Upstream, this is defined by a single if-then-else on equality with zero.

This module closes the Phase-2 gap between two previously disconnected constructions: the T0 floor (Boolean recognition cost on the two-state observable quotient forced by a distinction) and the extensive ledger. The shadow map is the explicit truncation that makes the floor the two-state image of the ledger.

One-line wrapper. Unfold the definition of the Boolean shadow (the if-then-else on $\Gamma=0$), then discharge the positive branch by reflexivity of equality at the zero ledger. No further lemmas are required.

This is the monoid-unit clause of the ledger-to-floor bridge. The bundled theorem LedgerFloorT0Bridge (via ledger_floor_t0_bridge) uses it to prove that the lift of the empty ledger is the empty floor state, so the truncation is a monoid homomorphism onto the T0 join.

It is also the $n=0$ arm of the single-primitive identity: on a Finsupp singleton the shadow equals Boolean truncation of the multiplicity, and the zero-multiplicity case reduces exactly here. Surjectivity of the lift onto the T0 floor likewise hits the unmarked state by sending the empty ledger through this fact.

In the forcing chain this is scaffolding under T0: it turns the Boolean indicator from a chosen floor into the genuine shadow of an extensive cost object, as required by the strict T-1-to-T8 audit.