T0_To_T1_Bridge
plain-language theorem explainer
The T0-to-T1 bridge certificate packages a Meta-Principle (T1) witness as a definitional corollary of logic-from-cost (T0), not as an independent sibling theorem. Anyone assembling the unified forcing chain cites it to lock the T0→T1 arrow. As a Prop structure it records both the forced T1 surface and an equality pinning that surface to the T0-corollary constructor for the supplied T0 hypothesis.
Claim. Given a hypothesis $h_0$ that logic is forced (consistent Boolean floor states have zero recognition-work cost; inconsistent ones have positive cost), the T0-to-T1 bridge is the proposition that there is a Meta-Principle witness $t_1$ with $t_1$ definitionally equal to the direct T0-corollary of $h_0$.
background
In the Unified Forcing Chain module, T-1 through T8 are claimed as forced inevitabilities from the cost foundation (Recognition Composition Law, normalization, calibration). T0 asserts that logic is not pre-given: at the Boolean floor it is the zero/positive split of recognition work. Consistent configurations cost zero; inconsistent ones cost positively. That is the foundation beneath the Meta-Principle.
T1 (Meta-Principle forced) says an inconsistent recognition-work state cannot be selected as a zero-cost state: inconsistent floor states have positive cost, and zero-cost states are consistent. The module's stronger claim is that T1 is not an independent axiom sibling of T0. Upstream, a corollary theorem builds a T1 witness by re-exporting T0's inconsistency-positive and zero-cost-consistent fields. This bridge structure is the certificate type that packages that dependency and forbids a parallel independent T1.
proof idea
This is a structure definition (Prop bundle), not a proved theorem body. It declares two fields: a T1 (Meta-Principle forced) witness, and a definitional equality requiring that witness to equal the T0-corollary constructor applied to the supplied T0 hypothesis. The companion inhabitant theorem simply sets the T1 field to that corollary and discharges the equality by reflexivity (rfl). No extra algebraic work is done here; the content lives in the corollary and in T0.
why it matters
This bridge is the T0→T1 link in the complete inevitability chain from absolute floor through dimensional forcing. Downstream it is a required field of the compact T-1-to-T1 certificate, of the full T-1-to-T8 forcing-chain record, and of this module's CompleteForcingChain. The equality field is the honesty mechanism: it records that the bundled T1 witness is definitionally the T0 corollary, so a parallel T1 proof cannot be smuggled in as if independent.
Framework landmarks: T0 (logic from cost minimization) and T1 (Meta-Principle from cost: nothing has infinite cost / inconsistent states are not zero-cost). The chain continues to T5 J-uniqueness, T6 phi, T7 eight-tick, T8 D=3, but this declaration only seals the first logic-to-MP step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.