TMinus1_To_T0_Bridge
plain-language theorem explainer
The T-1→T0 bridge is a Prop-valued certificate that the absolute Boolean floor supplies a unit-normalized recognition-work cost, with zero cost exactly on consistent states, and thereby reaches the pre-analytic T0 logic surface. Anyone assembling the complete forcing chain from absolute floor through T0–T8 cites this edge. It is a structure packing named witnesses rather than a derived equality proof.
Claim. A T-1 to T0 bridge is a package of: an absolute-floor witness on $\mathrm{Bool}$; its canonical two-point normalization (empty/marked with unit cost on the marked state); the induced Boolean configuration and recognition-cost interfaces; a nonempty recognition-work constraint certificate; the identities $C(\mathrm{false})=0$ and $0<C(\Gamma)\Leftrightarrow\Gamma$ is inconsistent; and a T0 logic-forced record (logic as the zero/positive split of recognition work).
background
The Unified Forcing Chain module claims every level T-1 through T8 is forced from the cost foundation (Recognition Composition Law plus normalization and calibration), not merely compatible with it. T-1 is the absolute floor: a meta-language Prop distinction plus a non-singleton universe of discourse, packaged as an absolute-floor witness. T0 is the claim that logic is not pre-given but is the zero/positive split of recognition work on that floor.
A configuration space supplies empty configuration, join, consistency, and independence. Recognition-work cost on the Boolean floor is the minimal model: empty/consistent is false with cost 0; the unique marked inconsistent state is true with unit cost. Bare distinguishability does not name false/true or fix the unit scale; the canonical two-point normalization and the Boolean floor-config/cost certificates make that orientation and scale explicit.
Upstream, the absolute-floor witness forces bare distinguishability from meta-language Prop inequality and nontrivial specification. Cost-from-distinction supplies the configuration and cost interfaces that T0 consumes.
proof idea
No proof body: this is a Prop-structure definition whose fields are the bridge obligations. Downstream constructors (e.g. the theorem that builds a bridge from a T-1 absolute-floor certificate) fill the fields by extracting the Boolean absolute-floor witness, applying the Boolean floor-config and unit-normalized cost certificates from that witness, supplying the recognition-work constraint nonemptiness, discharging the zero-cost and positive-iff-inconsistent identities on the Boolean cost, and packaging the resulting T0 logic-forced record. The structure itself only names the interface; it does not re-prove cost uniqueness or RCL.
why it matters
This is the non-vacuous edge the module doc says was missing from older aggregates: absolute floor → Boolean distinction → concrete recognition-work cost (dichotomy and independent additivity) → LogicFromCost T0 payload. It is the first link in the complete inevitability chain (T-1 floor, T0 logic from cost minimization, then MP, discreteness, ledger, unique J, φ, eight-tick, D=3).
Parents include the T-1→T1 bridge certificate and its holding theorem, the compact TMinus1ToT1Cert, and the full CompleteForcingChainT8 record (which stores this bridge as tminus1_to_t0). Later bridges such as T0–T2→T3 also take a T-1→T0 bridge as a parameter for floor join and additivity facts. Framework landmark: T0 in the forcing chain, logic forced from cost rather than assumed. Note the honesty comment on the T8 aggregate: T5 uniqueness does not consume this floor bridge beyond re-export; the substantive floor-to-analytic-J gap remains a separate issue.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.