t1_to_t2_bridge_holds
plain-language theorem explainer
Given the T-1→T0 Boolean-floor bridge and T1 (modus ponens / zero-cost consistency), the T1→T2 bridge certificate is inhabited: the floor is exhausted by two distinct states, consistency is exactly the unmarked state, and positive cost selects the marked state. Anyone assembling the complete T0–T8 forcing chain cites this edge. The proof fills the bridge fields by transporting dichotomy and cost–consistency facts from the Boolean floor, then packages the T2 discreteness payload.
Claim. If $B_{01}$ is a T-1$\to$T0 bridge certificate (Boolean absolute floor with recognition-work cost and consistency interface) and $H_1$ asserts T1 (zero-cost floor states are consistent; inconsistent states have positive cost), then the T1$\to$T2 bridge holds: the floor used is $B_{01}$'s Boolean floor; every floor state is $\mathsf{false}$ or $\mathsf{true}$ and these are distinct; consistency is exactly $\mathsf{false}$; positive cost selects the marked state; and the T2 discreteness payload follows.
background
The Unified Forcing Chain module aims to show every landmark T-1 through T8 is forced from the cost foundation (Recognition Composition Law plus normalization and calibration), not merely compatible with it. T-1 is the absolute floor: a meta-language Boolean distinction in a non-singleton universe. T0 says logic (consistency is cheap) emerges from cost minimization. T1 is the meta-principle that nothing of infinite cost is selected: inconsistent recognition-work states cannot be zero-cost.
A configuration space (from CostFromDistinction) carries an empty config, a join, a consistency predicate, and independence. The T-1→T0 bridge packages a Boolean absolute-floor witness, a normalized two-point floor, a Bool floor config, and a unit-normalized recognition-work cost. Its doc-comment stresses this is the non-vacuous edge: the Boolean distinction carries concrete recognition-work cost with dichotomy and independent additivity, reaching the LogicFromCost T0 payload through that interface.
T2 is discreteness: continuous structure cannot stabilize under cost. The T1→T2 bridge exists because T1 alone only relates zero/positive cost to consistency; discreteness also needs the explicit two-state Boolean floor (consistent = false, marked = true) rather than hiding cases inside decide.
proof idea
Structure construction, not a deep algebraic argument. Set floor_used to the Boolean floor from the T-1→T0 bridge. Copy floor_dichotomy and floor_states_distinct from the bridge's floor config (false_true_distinct).
consistency_is_false is the forward direction of the floor config's consistency_iff_false. For positive_cost_selects_marked: positive cost implies inconsistency via floor_positive_iff_inconsistent; case-split on dichotomy; the consistent case contradicts, so the state is marked.
The nested t2 payload reuses the same dichotomy and distinctness. Its zero_cost_selects_consistency composes T1's zero_cost_consistent with consistency_iff_false. Its positive_cost_selects_marked repeats the same inconsistency-plus-dichotomy case split.
why it matters
This is the certified T1→T2 edge in the complete inevitability chain. Downstream, t2_holds is literally one application of this bridge; t3_holds and t4_holds thread the resulting T2 into ledger and recognition forcing; complete_forcing_chain and the TMinus1ToT8 twin complete_forcing_chain_t8 both invoke it when assembling the full stack.
In primer terms it discharges the T2 step ("Discreteness ← Cost (continuous can't stabilize)") on the pre-analytic Boolean floor, before analytic J-cost, φ-forcing (T6), the eight-tick octave (T7), and D=3 (T8). The module's stronger claim is that every level is forced with no gaps; this lemma makes the Boolean-floor witness explicit so T2 is not smuggled in by case analysis on Bool.
No scaffolding remains here: claim status is proved. The open work sits later in the chain (unique J, φ, dimension), not at this bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.