T2_Discreteness_Forced
plain-language theorem explainer
T2 packages discreteness as a four-field Prop on the Boolean absolute floor: every floor state is false or true, the two states differ, zero recognition cost forces the consistent state false, and positive cost forces the marked inconsistent state true. Anyone citing the T−1..T8 inevitability chain or the T1→T2 / T2→T3 bridges needs this interface. It is a definitional Prop bundle, not a proved theorem; witnesses are supplied by the T1 Meta-Principle bridge.
Claim. Discreteness at the absolute floor is the conjunction of: (i) every Boolean floor configuration $\Gamma$ equals $\mathsf{false}$ or $\mathsf{true}$; (ii) $\mathsf{false}\neq\mathsf{true}$; (iii) if the Boolean recognition cost of $\Gamma$ is zero, then $\Gamma=\mathsf{false}$ (consistency); (iv) if that cost is strictly positive, then $\Gamma=\mathsf{true}$ (marked inconsistency). This is the pre-analytic meaning of discreteness, before the $J$-cost layer.
background
The Unified Forcing Chain module aims to show T−1 through T8 as forced from the cost foundation (Recognition Composition Law, normalization, calibration), not merely compatible. In that ladder, T2 is the discreteness step: after T0 (logic from cost minimization) and T1 (Meta-Principle: nothing has infinite cost), the floor must split into two stable states rather than a continuum.
The ambient floor is Boolean. Recognition cost on that floor is the Boolean recognition cost carried from the T−1→T0 bridge: zero on the consistent state, positive on the marked inconsistent state. Doc-comment meaning: before analytic $J$ appears, discreteness means exactly that zero-cost consistency and positive-cost inconsistency have been separated into those two Boolean states.
Upstream cost notions (observer $J$-cost, multiplicative-recognizer derived cost, rung-coarsen sums) sit at higher layers; T2 only needs the Boolean floor cost and the dichotomy of Bool.
proof idea
No proof body: this is a Prop-valued structure (four fields). It records what “discreteness is forced” means as a claim interface. Concrete instances are built downstream from the T1 floor Meta-Principle via the T1→T2 bridge (floor witness, dichotomy, distinctness, consistency-is-false, and the matching cost-selection rules). Later bridges project fields such as state_dichotomy rather than re-proving them.
why it matters
T2 is the discreteness rung in the complete inevitability chain (module claim: every level T−1..T8 forced from cost). Downstream, CompleteForcingChain / CompleteForcingChainT8 carry a t2 field of this type; T1_To_T2_Bridge is the intended producer; T0_T2_To_T3_Bridge and t0_t2_to_t3_bridge_holds consume state_dichotomy as the floor split into the ledger step; T2_T3_To_T4_Bridge uses T2 to supply a concrete distinction pair and balanced zero-cost consistency toward recognition.
In primer terms this is the T2 landmark before T3 ledger symmetry $J(x)=J(1/x)$, T5 $J$-uniqueness, T6 $\varphi$, T7 eight-tick, and T8 $D=3$. It does not yet introduce analytic $J$; it only freezes the two-point cost-marked floor that later steps refine.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.