LedgerT0IdentificationCertificate
plain-language theorem explainer
Packages the Phase-2 claim that the T0 floor is the two-state shadow of the extensive recognition ledger, specialised to one primitive distinction under unit weight. Auditors of the T-1-to-T8 chain cite it as the certificate type whose three fields demand a surjective cost-and-join homomorphism, rank-1 Boolean cost truncation, and genuine quotient surjectivity. The structure itself carries no proof; the companion theorem fills the fields from the bridge lemmas.
Claim. A Phase-2 identification certificate is a proposition asserting three facts, for every carrier $K$ with a distinction witness $h:\exists x\,y\in K,\,x\neq y$: (i) the truncation map from the unit-indexed extensive ledger (weight $1$) is a surjective cost-and-join homomorphism onto the distinction-generated T0 floor; (ii) on a single multiplicity $n\in\mathbb{N}$, the forced-quotient recognition cost of the truncated ledger equals the Boolean recognition cost of the Boolean truncation of $n$; (iii) that truncation map is surjective, so the T0 floor is a genuine quotient (shadow) of the ledger.
background
The module closes a Phase-2 audit gap: before it, DistinctionToT4 built the T0 floor as recognition-work cost on the two-state forced quotient of a distinction $h$, with Boolean indicator cost, while RecognitionLedgerFloor built an extensive defect ledger $I\to_0\mathbb{N}$ with additive cost, never identified with that floor.
The explicit truncation is ledgerToFloor h $\Gamma$ := (forcedQuotientBoolEquiv h).symm (ledgerShadow $\Gamma$), where the shadow is false exactly on the zero ledger and true otherwise. The sibling structure LedgerFloorT0Bridge asserts that this lift is a monoid homomorphism onto the T0 join (empty to empty, addition to Boolean OR), a cost truncation clamping extensive cost to ${0,1}$, and surjective.
Upstream, forcedQuotientRecognitionCost is the recognition-work cost on the distinction quotient, defined by transporting Boolean recognition cost along the forced-quotient/Bool equivalence. The certificate specialises the bridge to index type Unit and constant weight $1$.
proof idea
No proof body: this is a bare structure ... : Prop packaging three named fields. Each field is a quantified proposition (bridge instance, rank-1 cost identity, surjectivity). Inhabitation is deferred to the companion theorem ledger_t0_identification_certificate, which fills the fields by applying ledger_floor_t0_bridge (with one_pos), rank1_cost_is_boolean_truncation, and ledgerToFloor_surjective.
why it matters
This is the audit-facing certificate type for Phase 2 of the strict T-1-to-T8 forcing chain: it turns T0 from a chosen Boolean indicator into the shadow of an extensive cost object. The sole downstream consumer is ledger_t0_identification_certificate, whose doc-comment states that the Phase-2 ledger-to-T0 identification is a theorem and constructs an instance by discharging all three fields.
In the Recognition framework this sits at the base of the forcing chain (T0), before J-uniqueness (T5), phi as self-similar fixed point (T6), the eight-tick octave (T7), and $D=3$ (T8). Without the certificate, the extensive ledger and the distinction floor remain formally disconnected worlds. Packaging the three obligations as a single Prop makes the audit checklist machine-checkable rather than narrative.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.