T0_To_T1_Bridge
plain-language theorem explainer
Public re-export of the T0→T1 bridge certificate: given a forced Boolean recognition-work split (T0), T1 (the cost-form Meta-Principle) is packaged as its direct corollary, not a sibling axiom. Anyone assembling the T−1…T8 forcing spine cites this alias. The body is a one-line abbrev onto the structure in the T−1–T1 bridge module.
Claim. Abbreviation: the T0-to-T1 bridge is the structure that, given a proof $h_0$ that Boolean recognition logic is forced, packages a forced Meta-Principle witness $t_1$ together with the equality $t_1 = \mathrm{corollary\_of\_T0}(h_0)$, recording that T1 is definitionally the T0 corollary rather than an independent postulate.
background
This module is the public T−1 through T8 forcing spine. It stops before private operator and measurement layers. In that spine, T0 is the Boolean recognition-work split (logic forced from cost/consistency), and T1 is the cost-form Meta-Principle.
Upstream, the real object lives in the T−1–T1 bridge module and is mirrored in the unified forcing chain: a Prop-structure parameterized by a T0 witness $h_0$. Its fields are a T1 surface and an equality asserting that surface equals the packaged corollary of $h_0$. The unified-chain doc states the intent plainly: "T1 is not an independent theorem sibling of T0. It is the direct corollary of the T0 cost/consistency split: inconsistent floor states have positive cost, and zero-cost floor states are exactly consistent states."
The present declaration does not redefine that structure; it only exposes it under the public T−1…T8 namespace so later chain certificates can name one stable bridge type.
proof idea
One-line abbrev. No tactics, no new proof obligations. It aliases TMinus1ToT1Bridge.T0_To_T1_Bridge, so every field and every instance of the source structure is definitionally available here. Inhabitation is supplied elsewhere by t0_to_t1_bridge_holds, which sets the T1 field to t1_corollary_of_t0 h0 and discharges the equality by rfl.
why it matters
This alias is the named T0→T1 link inside the public forcing spine. Downstream, CompleteForcingChainT8 and the full CompleteForcingChain both carry a field t0_to_t1 : T0_To_T1_Bridge t0, and the compact TMinus1ToT1Cert does the same. The holding lemma t0_to_t1_bridge_holds is re-exported beside it so certificates can be filled without importing the private bridge module.
In the Recognition Science forcing chain (primer T0–T8), this is the first cost-logic step after the absolute distinguishability floor: T0 forces the Boolean split; T1 is forced as its corollary before discreteness (T2), ledger bookkeeping (T3), the recognition witness (T4), J-uniqueness (T5), φ (T6), the eight-tick octave (T7), and D = 3 (T8). The equality field is the honesty device: T1 must not be smuggled in as a fresh axiom once T0 is on the table.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.