ledgerToFloor
plain-language theorem explainer
Explicit truncation map from an extensive defect ledger to the two-state T0 floor forced by a distinction witness. Anyone citing the Phase-2 ledger-to-T0 identification uses this carrier map. Defined by transporting the Boolean ledger shadow through the inverse of the forced quotient-to-Bool equivalence; a one-line composition, not a proved property.
Claim. Given a distinction witness $h:\exists x,y\in K,\,x\neq y$ and a defect ledger $\Gamma$ (finitely supported multiplicities on an index type $I$), the lift to the distinction-generated observable quotient is $\mathrm{ledgerToFloor}_h(\Gamma):=\Phi_h^{-1}(\mathrm{shadow}(\Gamma))$, where $\mathrm{shadow}(\Gamma)$ is $\mathsf{false}$ if $\Gamma=0$ and $\mathsf{true}$ otherwise, and $\Phi_h$ is the canonical equivalence between that quotient and $\mathsf{Bool}$.
background
This module closes a Phase-2 gap in the strict T-1-to-T8 audit: before it, two constructions sat side by side with no formal link. DistinctionToT4 builds the T0 floor as recognition-work cost on the observable quotient forced by a distinction $h:\exists x,y,,x\neq y$; that quotient is two-state ($\simeq\mathsf{Bool}$) with Boolean indicator cost. RecognitionLedgerFloor builds the extensive ledger $\mathrm{DefectLedger},I=I\to_0\mathbb{N}$ (free commutative monoid of finitely supported multiplicities) with additive weighted cost, but never identifies it with the T0 floor.
The Boolean shadow of a ledger is the two-state truncation of extensive $\mathbb{N}$-valued multiplicity: $\mathsf{false}$ on the empty ledger, $\mathsf{true}$ as soon as any recognition has been posted. The forced quotient is the observable quotient generated by the distinction witness; the forced quotient-to-Bool map is the coordinate equivalence transporting that quotient to $\mathsf{Bool}$.
The present definition is the lift of that shadow into the distinction-generated quotient, so the target is the T0 floor itself, not an unrelated carrier.
proof idea
One-line definitional composition. Evaluate the Boolean shadow of the input ledger, then apply the inverse of the forced quotient-to-Bool equivalence. No tactic proof and no intermediate lemmas: the body is exactly that transport. Noncomputable only because the underlying equivalence is.
why it matters
This is the explicit truncation map that makes the T0 floor the two-state shadow of the extensive recognition ledger, discharging the colleague-checklist item that T0 must be the shadow of an extensive cost object rather than a chosen Boolean indicator.
It is the carrier of the structure LedgerFloorT0Bridge, which packages monoid-homomorphism onto the T0 join, cost truncation (floor cost equals the clamp of extensive ledger cost to ${0,1}$), surjectivity, and kernel identification. Downstream results that apply it include the universal bridge theorem for every distinction and strictly positive weight, surjectivity of the shadow lift, the rank-1 identity that floor cost is Boolean recognition cost of truncated multiplicity, and the audit certificate packaging the full Phase-2 identification under unit weight on a single primitive distinction.
Sits at the T0 end of the forcing chain (T0-T8): once the floor is the ledger shadow, later steps (J-uniqueness, $\varphi$, eight-tick octave, $D=3$) rest on a cost object rather than an ad hoc bit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.