ledger_t0_identification_certificate
plain-language theorem explainer
Public re-export of the Phase-2 certificate that the T0 Boolean floor is a genuine cost-and-join quotient (shadow) of the free extensive recognition ledger. Cite it when the core-theory PDF needs a single packaged witness that the floor is non-vacuous truncation of DefectLedger, not an independent axiom. The body is a one-line abbrev pointing at the Foundation bridge theorem that assembles the three component facts.
Claim. The packaged Phase-2 identification certificate: for any distinction witness, the T0 Boolean floor is a genuine quotient (shadow) of the extensive recognition ledger $I \to_0 \mathbb{N}$, via a surjective cost-and-join map, with rank-1 ledger cost equal to Boolean truncation of multiplicity.
background
The LedgerFloor module is the public aggregator for the Boolean shadow of the extensive recognition ledger. The ledger itself is the free commutative monoid $\mathrm{DefectLedger}, I = I \to_0 \mathbb{N}$ of finitely supported multiplicities of primitive distinctions, equipped with a weighted recognition cost that is unconditionally additive.
The T0 floor is the two-state Boolean recognition layer obtained by truncating multiplicity: presence versus absence of each distinction. The module documents that this floor is non-vacuous precisely when some distinction has positive weight, and that two independent copies of one defect cost twice the weight, so multiplicity is represented rather than collapsed.
Upstream, the Foundation bridge defines a structure LedgerT0IdentificationCertificate whose three fields package the bridge map, the rank-1 cost-as-truncation identity, and surjectivity of the ledger-to-floor map. The doc there states: "The Phase-2 ledger-to-T0 identification is a theorem."
proof idea
One-line abbrev: the public name is definitionally equal to Foundation.LedgerFloorT0.ledger_t0_identification_certificate. No local proof work occurs here.
The upstream theorem constructs an inhabitant of the certificate structure by supplying three component lemmas: ledger_floor_t0_bridge (with constant positive weight one) as the bridge, rank1_cost_is_boolean_truncation as the rank-1 cost identity, and ledgerToFloor_surjective as the quotient/surjectivity witness.
why it matters
This is the named public citation target for Phase-2 of the ledger-floor story: the core-theory PDF cites it to assert that the T0 Boolean floor is a genuine shadow of the extensive ledger, not a free-standing postulate. The module lists it among the primary export points alongside DefectLedger, ledgerCost, and ledger_floor_t0_bridge.
In the Recognition forcing chain it sits under the T0 Boolean recognition cost and the forced-quotient layer (DistinctionToT4, TMinus1ForcedFromDistinction, TMinus1ToT0). It does not itself force $\phi$, the eight-tick octave, or $D=3$; those are later T5–T8 steps. Its role is to close the identification that the Boolean floor is the truncation quotient of the free additive ledger, so downstream arguments may treat T0 as derived shadow rather than independent data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.