LedgerFloorT0Bridge
plain-language theorem explainer
The T0 floor is the Boolean truncation of the extensive recognition ledger: a Prop bundle asserting that the shadow map from defect ledgers to the distinction-forced two-state quotient is a monoid homomorphism, that floor cost is the clamp of extensive ledger cost to {0,1}, and that floor identity is the cost-kernel. Anyone citing the Phase-2 T0 identification or the T-1-to-T8 audit certificate needs this interface. It is a definitional structure; the inhabiting theorem supplies the proofs fieldwise.
Claim. Fix a distinction witness $h:\exists x,y\in K,\,x\neq y$ and weights $w:I\to\mathbb{R}$. The structure asserts that the shadow map $\mathrm{ledgerToFloor}_h$ from the extensive defect ledger $\mathrm{DefectLedger}\,I=I\to_0\mathbb{N}$ onto the forced T0 quotient satisfies: (i) empty ledger maps to the empty configuration; (ii) addition projects to the floor join (Boolean OR); (iii) T0 recognition cost of the shadow equals $0$ if ledger cost is zero and $1$ otherwise; (iv) consistency of the shadow iff ledger cost vanishes; (v) two ledgers share a shadow iff they agree on whether extensive cost is zero.
background
The module closes a Phase-2 gap in the strict T-1-to-T8 audit: before it, the distinction-generated T0 floor and the extensive recognition ledger sat side by side with no formal link. DistinctionToT4 builds the T0 floor as recognition-work cost on the observable quotient ForcedQuotient h forced by a distinction $h:\exists x,y:K,,x\neq y$; that quotient is two-state ($\simeq\mathrm{Bool}$) with Boolean indicator cost. RecognitionLedgerFloor builds the extensive ledger $\mathrm{DefectLedger},I=I\to_0\mathbb{N}$ with additive cost $\mathrm{ledgerCost},w$, but never identifies it with T0.
A configuration space (from CostFromDistinction) is an abstract carrier with empty configuration, binary join, consistency predicate, and independence. The forced quotient inherits that structure. The explicit truncation is
$$\mathrm{ledgerToFloor}_h,\Gamma:=(\mathrm{forcedQuotientBoolEquiv},h)^{-1}(\mathrm{ledgerShadow},\Gamma),$$
where $\mathrm{ledgerShadow},\Gamma$ is false exactly when $\Gamma=0$ and true otherwise. The structure packages the homomorphism, cost-truncation, and kernel claims that make the floor a genuine shadow of the ledger.
proof idea
No proof body: this is a Prop-valued structure (five fields). Inhabitation is deferred to ledger_floor_t0_bridge, which, given strictly positive weights $w$, fills each field by unfolding ledgerToFloor and rewriting with the sibling lemmas ledgerShadow_zero, the additivity and single-support facts for ledgerShadow, and the cost identities that clamp extensive cost to ${0,1}$. Surjectivity of the shadow (every floor state is hit) is stated separately as ledgerToFloor_surjective and is not one of the five structure fields, though the module doc treats it as part of the same identification.
why it matters
This is the interface that turns T0 from a chosen Boolean indicator into the shadow of an extensive cost object, the Phase-2 item on the colleague T-1-to-T8 checklist. Downstream, ledger_floor_t0_bridge proves the structure for every distinction witness and every strictly positive weight; LedgerT0IdentificationCertificate packages the specialised unit-weight, single-primitive case for the audit; and LedgerFloor.LedgerFloorT0Bridge re-exports the abbrev.
In the forcing chain, T0 is the base of UnifiedForcingChain: once the floor is the truncated ledger rather than an ad hoc Bool, later steps (J-uniqueness at T5, $\varphi$ at T6, eight-tick octave at T7, $D=3$ at T8) rest on a cost object that already knows extensive multiplicity. The kernel field says floor identity is exactly the truncated cost kernel, so no extra structure is smuggled in at the Boolean level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.