tminus1_to_t0_bridge
plain-language theorem explainer
From any absolute-floor certificate, a Boolean distinction carries a unit-normalized recognition-work cost that forces the T0 logic interface (consistency cheap, contradiction expensive). Citers of the complete T-1 through T8 inevitability chain need this non-vacuous edge. The proof is a term-mode record: extract the Boolean witness, normalize to a two-point floor, and package the LogicFromCost fields via cost-positivity and additivity lemmas.
Claim. Given an absolute-floor certificate establishing meta-language proposition distinguishability and a non-singleton universe of discourse, there is a bridge to T0: the extracted Boolean floor witness yields a canonical normalized two-point recognition cost with dichotomy and independent additivity, and the T0 logic-from-cost payload (consistency is cheap, contradiction is expensive, logic emergent as zero-cost configurations) follows from that cost interface.
background
The Unified Forcing Chain module proves that T0 through T8 are forced from the cost foundation (Recognition Composition Law, normalization $F(1)=0$, calibration $F''(1)=1$). The chain bottoms out at T-1, the absolute floor: two preconditions of statability itself, namely meta-language proposition distinguishability and a non-singleton universe of discourse.
T0 asserts that classical logic emerges from cost minimization: consistency has zero cost, contradiction has positive cost, and the zero-cost configurations are exactly the consistent ones. The bridge structure packages the missing non-vacuous edge. As its doc-comment states, "the absolute floor supplies the Boolean distinction; that Boolean distinction carries a concrete recognition-work cost satisfying dichotomy and independent additivity; and the existing LogicFromCost T0 payload is then reached through this cost/consistency interface."
Upstream, the absolute-floor closure certificate provides the Boolean witness. Sibling constructions normalize that witness to a two-point floor and extract the Boolean configuration interface together with the unit-normalized recognition cost.
proof idea
Term-mode construction of the bridge record. The Boolean floor is the witness field of the absolute-floor closure certificate. The normalized floor is the canonical two-point floor normalization of that witness. Configuration and cost interfaces are the corresponding Boolean extractions from the same witness.
Recognition-work is the Boolean work-constraint theorem. Floor consistency on the empty configuration is definitional (rfl). Positivity of cost iff inconsistency is the general CostFromDistinction lemma specialized to the Boolean recognition cost. The embedded T0 payload reuses the normalized floor's recognition-work, zero-on-empty, positive-iff-inconsistent, and zero-iff-consistent fields, plus Boolean cost additivity for independent additivity.
why it matters
This is the non-vacuous T-1→T0 edge that older aggregates lacked. Downstream, t0_from_tminus1 projects the T0 field directly; complete_forcing_chain and complete_forcing_chain_t8 thread the bridge into the full inevitability chain from absolute floor through D=3. The T-1-to-T1 certificate also starts here before attaching the T0→T1 step.
In the framework landmarks, T0 is the first forced level after the absolute floor: logic from cost minimization rather than an assumed primitive. Closing this edge lets the chain claim every level T0–T8 is forced, not merely compatible, once the meta-language floor is granted. The module's stronger top-level claim ("Complete Inevitability Chain") depends on this bridge being theorem-backed rather than postulated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.