t2_corollary_of_t1
plain-language theorem explainer
If the Meta-Principle holds on the Boolean recognition-cost floor (zero-cost states are consistent), then discreteness is forced: the floor splits into exactly two distinct states, zero cost selects consistency, and positive cost selects the marked state. Cited by anyone chaining T1 into T2–T4 in the unified forcing chain. The proof builds the T2 structure by Bool case analysis plus the T1 zero-cost consistency field.
Claim. Assume the Meta-Principle on the Boolean floor: every zero-cost configuration is consistent (and inconsistent configurations have positive recognition-work cost). Then discreteness is forced: every floor state $\Gamma$ is either $\mathrm{false}$ or $\mathrm{true}$, these two states are distinct, zero recognition cost selects only $\mathrm{false}$ (consistency), and positive cost selects only $\mathrm{true}$ (the marked inconsistent state).
background
The Unified Forcing Chain module aims to show that T0–T8 are inevitabilities from the cost foundation (Recognition Composition Law, normalization, calibration), starting from an absolute floor. The local chain step here sits between T1 and T2.
T1 (Meta-Principle forced) is a structure on Boolean floor configurations: inconsistent states have strictly positive recognition-work cost, and any zero-cost state is consistent. The cost is the Boolean recognition cost from the T-1→T0 bridge (boolRecognitionCost), which assigns work to floor configurations before the analytic $J$-cost layer appears.
T2 (discreteness forced) packages four facts on that same Boolean floor: exhaustive dichotomy into the two Bool values, distinctness of those values, zero cost selects only the consistent state false, and positive cost selects only the marked state true. In this pre-analytic sense, discreteness means the floor has already separated consistency from inconsistency into two discrete labels.
proof idea
Construct a T2_Discreteness_Forced witness from a T1_MP_Forced hypothesis h.
state_dichotomy: introduce $\Gamma:\mathrm{Bool}$ and case-split; each branch is reflexivity (false = falseortrue = true).states_distinct: closed bydecide(false ≠ true).zero_cost_selects_consistency: applyh.zero_cost_consistentdirectly to the zero-cost hypothesis.positive_cost_selects_marked: case on $\Gamma$. Onfalse, the Boolean cost is definitionally $0$, so positivity contradicts bylinarith. Ontrue, the goal is reflexivity.
No external lemmas beyond the T1 field and Bool/cost definitional facts; the Boolean floor is exposed explicitly rather than left implicit in the cases.
why it matters
This is the T1→T2 bridge certificate in the complete inevitability chain: T-1 absolute floor → T0 logic → T1 MP → T2 discreteness → T3 ledger → … → T8. The module claim is that every level is forced from cost, not merely compatible; T2 here is discreteness before analytic $J$, as two-state separation of zero-cost consistency from positive-cost marking.
Downstream audit equalities pin the standalone holders to the routed corollary chain: t2_holds_eq_corollary equates t2_holds with this corollary applied to the T1 surface from T0; t3_holds_eq_corollary and t4_holds_eq_corollary thread the same T2 witness into ledger and recognition forcing. Without this bridge, later steps would hide the Boolean floor inside ad hoc case splits instead of a named T1→T2 implication.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.