T2_Discreteness_Forced
plain-language theorem explainer
T2 packages two-state discreteness of the Boolean recognition floor: every state is false or true, the states are distinct, zero cost selects only consistency (false), and positive cost selects only the marked state (true). Anyone assembling the public T−1..T8 forcing spine cites this record as the T2 slot. It is a Prop-structure (definitional interface), not a proved theorem.
Claim. The discreteness claim on the Boolean floor: every state $\Gamma\in\{\mathrm{false},\mathrm{true}\}$ is one of the two Booleans; $\mathrm{false}\neq\mathrm{true}$; the recognition-work cost $C$ satisfies $C(\Gamma)=0\Rightarrow\Gamma=\mathrm{false}$ and $0<C(\Gamma)\Rightarrow\Gamma=\mathrm{true}$, where $C$ is the concrete Boolean cost ($0$ on false, $1$ on true).
background
The module is the public T−1 through T8 forcing spine. T−1 is the absolute distinguishability floor; T0 the Boolean recognition-work split; T1 the cost-form Meta-Principle; T2 is two-state discreteness of that floor, before any analytic $J$ layer.
The cost in play is the concrete Boolean recognition-work cost: $C(\Gamma)=0$ if $\Gamma=\mathrm{false}$ and $1$ otherwise. Upstream, a normalized two-point recognition floor is the abstract version of this Boolean floor: one empty/consistent point, one marked inconsistent point, a unit-normalized cost, and an equivalence to Bool as canonical representative. Uniqueness results identify any such normalized floor (with mark true) with this cost pointwise.
In the unified chain wording, discreteness means the floor has already separated zero-cost consistency from positive-cost inconsistency into the two Boolean states.
proof idea
No proof body: this is a Prop-valued structure that bundles four fields. state_dichotomy is the exhaustive Boolean case split; states_distinct is false ≠ true; the two cost-selection fields are the implications from the Boolean cost $C$ (zero only on false, positive only on true). Downstream bridge theorems inhabit the structure by supplying those four facts from earlier floor and cost lemmas, rather than deriving them inside this declaration.
why it matters
T2 is the named discreteness step on the public forcing spine (primer landmark T2 in the T0–T8 chain). It is a required field of CompleteForcingChainT8 and of the unified CompleteForcingChain, and it is the hypothesis type for the bridges T1_To_T2_Bridge, T0_T2_To_T3_Bridge, and T2_T3_To_T4_Bridge.
Those bridges use it concretely: t0_t2_to_t3_bridge_holds re-exports state_dichotomy as the floor split into ledger additivity; t2_t3_to_t4_bridge_holds takes states_distinct as the witness that a distinction exists on the floor before balanced ledger recognition. Without this interface, the spine cannot pass from Meta-Principle cost form to additive ledger bookkeeping and recognition witnesses. It deliberately stops short of T5 $J$-uniqueness and later $\varphi$, eight-tick, and $D=3$ steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.