t1_corollary_of_t0
plain-language theorem explainer
T1 (the Meta-Principle: inconsistent floor states cannot be zero-cost) is not an independent axiom; it is a direct corollary of T0's cost/consistency split. Anyone citing the T0→T1 bridge or the unified forcing chain uses this. The proof is a short term constructor that repackages T0's positive-cost and zero-cost fields into the T1 witness bundle.
Claim. If logic is forced at the Boolean floor (consistent configurations have recognition cost $0$, and every inconsistent configuration has strictly positive cost), then the Meta-Principle is forced: every inconsistent Boolean floor state has positive cost, every zero-cost state is consistent, and the marked inconsistent state $\mathsf{true}$ has positive cost.
background
The Unified Forcing Chain module aims to show that T0–T8 are inevitabilities from the cost foundation (Recognition Composition Law, normalization, calibration), not optional siblings. T-1 supplies an absolute floor; T0 then forces classical logic as the zero/positive split of recognition work on that floor.
T0_Logic_Forced packages three facts: a recognition-work cost certificate on Bool, cheap consistency (C(false) = 0), and expensive contradiction (every inconsistent Boolean state has positive cost). The Meta-Principle surface T1_MP_Forced asks for the dual reading: inconsistent states are never zero-cost, zero-cost states are consistent, and a marked inconsistent witness is positive.
In the chain diagram, T0 is "Logic ← cost minimization (consistency is cheap)" and T1 is "MP ← cost (nothing has infinite cost)". This declaration makes the second arrow a pure corollary of the first.
proof idea
Term-mode structure construction from a T0 hypothesis h.
inconsistent_positiveis taken verbatim fromh.contradiction_expensive.zero_cost_consistentapplies the forward direction ofh.logic_emergentat each Boolean configuration: zero cost implies consistency.marked_inconsistent_positivespecializes the expensive-contradiction field attrue, discharging the inconsistency side-condition byBool.noConfusionafter rewritingtrue = false.
No external lemmas beyond the T0 field projections and Boolean absurdity are required.
why it matters
This is the hinge that demotes T1 from an independent forcing step to a corollary of T0. Downstream, T0_To_T1_Bridge and t0_to_t1_bridge_holds record that the bundled T1 witness is definitionally t1_corollary_of_t0 h0 (equality field t1_eq_corollary := rfl). Audit equalities such as t1_holds_eq_routed and the later T2/T3 corollary routing (t2_holds_eq_corollary, t3_holds_eq_corollary) depend on this identification.
In the primer chain, T0 forces logic from cost; T1 is the Meta-Principle reading of that same split. Closing T0→T1 without a fresh axiom keeps the "Complete Inevitability Chain" claim honest: every level after the absolute floor is forced by cost structure rather than postulated. The same bridge is mirrored in TMinus1ToT1Bridge for the T-1→T0→T1 path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.