t2_holds
plain-language theorem explainer
Discreteness is forced on the pre-analytic Boolean floor: every floor state is one of two distinct Booleans, zero cost picks only consistency, and positive cost picks the marked inconsistent state. Citers of the T0–T8 inevitability chain need this as the T2 step before ledger and J uniqueness. The proof is a short term chain through the T-1→T0, T0→T1, and T1→T2 bridges.
Claim. Discreteness is forced on the pre-analytic floor: every Boolean floor state $\Gamma$ satisfies $\Gamma=\mathsf{false}\lor\Gamma=\mathsf{true}$; the two states are distinct; zero recognition cost selects only the consistent state; and positive cost selects only the marked inconsistent state.
background
The Unified Forcing Chain module shows that T0–T8 are forced from the cost foundation (Recognition Composition Law, normalization, calibration), starting from an absolute floor rather than assuming logic or discreteness.
T2 is the discreteness step. Before any analytic $J$ layer, discreteness means the floor has already separated zero-cost consistency from positive-cost inconsistency into two Boolean states. The structure packages four facts: exhaustive dichotomy on $\mathsf{Bool}$, distinctness of $\mathsf{false}$ and $\mathsf{true}$, zero cost selects only consistency, and positive cost selects only the marked inconsistent state.
Upstream, the canonical T-1→T0 bridge supplies the Boolean absolute floor, its config, recognition cost, and work constraint. From a forced T0 (logic from cost), the T0→T1 bridge yields MP (nothing has infinite cost). The T1→T2 bridge then packages the floor dichotomy and distinctness into the T2 surface used here.
proof idea
Term-mode chain, no tactics. Bind the canonical T-1→T0 bridge, push it through the local T0 extraction to obtain forced logic, then take the T1 field of the T0→T1 bridge. Feed that bridge and the forced T1 into the T1→T2 bridge and project its T2 field. The result is exactly the discreteness structure: dichotomy, distinctness, and the two cost-selection rules on the Boolean floor.
why it matters
This is the T2 link in the complete inevitability chain: after logic (T0) and MP (T1), discreteness is forced by cost before ledger symmetry (T3), recognition (T4), unique $J$ (T5), $\varphi$ (T6), the eight-tick octave (T7), and $D=3$ (T8).
Downstream, Gravity.MasterTheorem.T0_T8_holds_proven includes this theorem as the T2 conjunct of the full T0–T8 package. The sibling audit theorem equates the standalone statement with the corollary applied to the routed T1 surface (subsingleton uniqueness), so the chain has a single canonical T2 witness rather than parallel copies.
Without T2, later discrete-ledger and self-similarity steps would rest on an unforced continuum; this closes that gap on the pre-analytic floor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.