t0_to_t1_bridge_holds
plain-language theorem explainer
Given that logic is forced as the zero/positive split of recognition work on the Boolean floor, the Meta-Principle is packaged as a direct corollary rather than an independent sibling axiom. Anyone citing the T0–T1 step of the unified forcing chain needs this bridge certificate. The proof is a structure construction: apply the T0 corollary for the T1 witness and close the equality field by reflexivity.
Claim. If logic is forced (consistent Boolean floor states have zero recognition cost and inconsistent ones have positive cost), then there is a T0-to-T1 bridge certificate: the Meta-Principle is forced, and the bundled T1 witness equals the explicit corollary extracted from that T0 hypothesis.
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. T0 is the claim that logic itself is not pre-given: on the minimal Boolean floor, recognition work assigns cost zero to the consistent state and positive cost to every inconsistent state.
T1 is the Meta-Principle surface in this chain: nothing carries infinite cost in the sense that inconsistency is strictly expensive and zero-cost floor states are exactly the consistent ones. The bridge structure records that T1 is not an independent theorem sibling of T0. Its doc states that T1 is the direct corollary of the T0 cost/consistency split, and that the equality field forces the bundled witness to be definitionally the corollary payload for the supplied T0 hypothesis.
Upstream, t1_corollary_of_t0 already builds the Meta-Principle witness by copying the inconsistency-positive and zero-cost-consistent fields out of T0 (with a short case on the marked inconsistent Boolean).
proof idea
Term-mode structure construction, not a multi-step tactic proof. Instantiate the bridge certificate by setting the T1 field to t1_corollary_of_t0 applied to the given T0 hypothesis, then discharge the equality field with rfl. That records definitional identity between the packaged witness and the corollary, so later consumers cannot treat T1 as a fresh independent axiom.
why it matters
This is the explicit T0→T1 link in the complete inevitability chain. Downstream, t1_holds projects the bridge's T1 field; tminus1_to_t1_cert threads it into the public T-1–T1 certificate; and both complete_forcing_chain (this module) and complete_forcing_chain_t8 (TMinus1ToT8Bridge) call it immediately after the T-1→T0 bridge to obtain the Meta-Principle witness before discreteness, ledger, unique J, φ, eight-tick, and D=3.
In framework terms it closes the first cost-to-logic step after the absolute floor: T0 (logic from cost minimization) supplies T1 (MP: nothing has infinite cost) without a second axiom. That matches the module's stronger claim that every level is forced from the single RCL/normalization/calibration bundle once the floor is statable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.