ledgerToFloor_surjective
plain-language theorem explainer
Every T0 floor state is the shadow of some extensive defect ledger: the truncation map from finitely supported multiplicities to the forced two-state quotient is surjective. Anyone citing the Phase-2 ledger-to-T0 identification needs this to know the floor is a genuine quotient, not an ad-hoc Boolean. The proof case-splits on the Bool coordinate and hits false by the zero ledger and true by a unit single at a fixed index.
Claim. Fix a type $K$ with at least two distinct elements, and an index type $I$ with a chosen base index $i_0$. The truncation map sending a defect ledger $\Gamma : I \to_0 \mathbb{N}$ to the T0 floor state whose Boolean coordinate is false if $\Gamma = 0$ and true otherwise is surjective onto the forced two-state quotient of $K$.
background
The module identifies the T0 floor with the Boolean truncation of the extensive recognition ledger. DistinctionToT4 builds the T0 floor as recognition-work cost on the observable quotient ForcedQuotient forced by a distinction $h : \exists x,y : K,, x \neq y$; that quotient is two-state ($\simeq$ Bool) with cost the Boolean indicator. RecognitionLedgerFloor builds the extensive ledger DefectLedger $I = I \to_0 \mathbb{N}$ with additive cost, previously unconnected to T0.
The bridge map is ledgerToFloor $h,\Gamma :=$ (forcedQuotientBoolEquiv $h$).symm (ledgerShadow $\Gamma$), where ledgerShadow $\Gamma$ is false exactly when $\Gamma = 0$ and true otherwise. Upstream, forcedQuotientBoolEquiv is the forced quotient-to-Bool coordinate equivalence; ledgerShadow_zero says the zero ledger shadows to false; ledgerShadow_eq_true_iff says the shadow is true iff the ledger is nonzero.
proof idea
Take an arbitrary floor state $q$. Case-split on whether forcedQuotientBoolEquiv $h, q$ equals false.
If false: the preimage is the zero ledger. Unfold ledgerToFloor, rewrite by ledgerShadow_zero, and apply the symmetry equation of the Bool equivalence.
If not false: the coordinate must be true (Bool cases). The preimage is the unit single Finsupp.single $i_0, 1$. That single is nonzero (single_eq_zero and one_ne_zero). Rewrite by ledgerShadow_eq_true_iff, then again match via the equivalence symmetry equation.
why it matters
This is one of the four pillars of LedgerFloorT0Bridge: monoid homomorphism onto the T0 join, cost truncation, surjectivity, and kernel identification. Downstream, ledger_t0_identification_certificate packages it as floor_is_quotient_of_ledger, discharging the Phase-2 audit item that T0 must be "the shadow of an extensive cost object" rather than a chosen Boolean indicator. The LedgerFloor re-export surfaces the same fact at the package boundary.
In the forcing chain, T0 is the entry point before T5 J-uniqueness and the later phi, eight-tick, and $D=3$ steps. Surjectivity ensures nothing on the floor is unhit by the ledger, so the Boolean recognition cost is literally a quotient of extensive ledger cost, not an independent postulate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.