T1_To_T2_Bridge
plain-language theorem explainer
Bridge certificate from T1 (modus ponens / zero-cost consistency) to T2 (two-state discreteness). It packages the Boolean absolute-floor witness from the T−1→T0 edge with T1's cost dichotomy so that every floor state is either consistent (`false`) or marked (`true`). Anyone assembling the complete T0–T8 forcing chain cites this structure. It is a pure Prop bundle: no proof body, only field obligations discharged by the companion existence theorem.
Claim. Given a $T_{-1}\to T_0$ bridge (Boolean absolute floor with recognition-work cost) and a $T_1$ certificate (inconsistent states have positive cost; zero-cost states are consistent), a $T_1\to T_2$ bridge is a record consisting of: an absolute-floor witness on $\mathrm{Bool}$; the dichotomy $\forall\Gamma,\,\Gamma=\mathsf{false}\lor\Gamma=\mathsf{true}$; distinctness $\mathsf{false}\neq\mathsf{true}$; consistency exactly at $\mathsf{false}$; positive cost selecting $\mathsf{true}$; and a $T_2$ discreteness certificate built from those facts.
background
The Unified Forcing Chain module aims to show every level T−1 through T8 is forced from the cost foundation (Recognition Composition Law plus normalization and calibration). T−1 supplies an absolute floor: a meta-language distinction plus a nontrivial universe of discourse. The T−1→T0 bridge extracts a Boolean absolute-floor witness, a normalized two-point floor, a configuration interface, and a unit-normalized recognition-work cost on Bool.
T1 (MP forced) is the cost corollary that inconsistent floor states have strictly positive recognition-work cost and zero-cost states are consistent. T2 (discreteness forced) means, before the analytic $J$ layer, that the floor has separated zero-cost consistency from positive-cost inconsistency into exactly two Boolean states.
A configuration space (from CostFromDistinction) carries an empty config, a join, a consistency predicate, and independence. On the Boolean floor, consistency is identified with false and the marked inconsistent state with true. T1 alone does not expose that two-state geometry; the bridge must surface the floor witness rather than bury it in case analysis.
proof idea
This declaration is a structure (Prop bundle), not a proved theorem. It names the obligations a $T_1\to T_2$ bridge must carry: the Boolean absolute-floor witness, dichotomy and distinctness of false/true, the identification of consistency with false, positive-cost selection of true, and the resulting $T_2$ discreteness record.
The companion theorem t1_to_t2_bridge_holds fills the fields by projection: floor_used from the T−1→T0 bridge's bool_floor; dichotomy and distinctness from that bridge's floor-config lemmas; consistency and positive-cost fields from T1 plus the Boolean cost; and t2 assembled from those pieces. No new analytic work occurs here.
why it matters
In the forcing chain, T2 is the first discreteness step: continuous structure cannot stabilize once cost separates consistency from inconsistency on a two-point floor. This bridge is the explicit edge that makes that step non-vacuous by recording the Boolean floor from T−1→T0 alongside T1.
Downstream, CompleteForcingChain and CompleteForcingChainT8 include this bridge (or its twin in TMinus1ToT8Bridge) as a required field between T1 and T2. The existence theorem t1_to_t2_bridge_holds is the discharge site. Without this certificate, the chain would hide the floor inside tactic cases/decide, breaking the audit requirement that every forcing edge expose its hypotheses.
Framework landmark: T2 in the T0–T8 sequence (discreteness before ledger, unique $J$, $\varphi$, eight-tick, and $D=3$). It does not yet touch T5 J-uniqueness or the RCL analytic layer; those sit further up the chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.