T1_To_T2_Bridge
plain-language theorem explainer
Certificate packaging the step from forced Meta-Principle (T1) plus the Boolean absolute-floor bridge into two-state discreteness (T2). Anyone assembling the public T−1…T8 spine cites it to expose the floor witness rather than hide it in case analysis. As a Prop structure it only records the required fields; the companion inhabitance theorem fills them from the T−1→T0 bridge.
Claim. Given a bridge $b_{01}$ from the absolute distinguishability floor to the Boolean T0 recognition-work interface and a forced cost-form Meta-Principle $h_1$ at T1, the T1-to-T2 bridge is the proposition that: an absolute Boolean floor witness is present; every $\Gamma:\mathrm{Bool}$ is $\mathrm{false}$ or $\mathrm{true}$; $\mathrm{false}\neq\mathrm{true}$; every consistent configuration equals $\mathrm{false}$; every state of positive Boolean recognition cost equals $\mathrm{true}$; and the T2 discreteness record holds (dichotomy, distinctness, zero-cost selects consistency, positive cost selects the marked state).
background
This module is the public theory-only 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 two-state discreteness of that floor. The spine stops before private operator and measurement layers.
The Boolean recognition cost is the concrete two-point cost $C(\mathrm{false})=0$, $C(\mathrm{true})=1$. An absolute-floor witness on a type $K$ asserts bare distinguishability (some unequal propositions) and a nontrivial specification. The T−1→T0 bridge already packages a Boolean floor witness, floor configuration, floor cost, a recognition-work certificate, and zero cost on the consistent state.
T2 discreteness itself is the record that every Boolean state is false or true, the two states differ, zero cost selects consistency (false), and positive cost selects the marked state (true). Upstream uniqueness says any normalized Boolean two-point floor with marked state true is canonically this floor.
proof idea
No proof body: the declaration is a Prop-valued structure (definitional certificate). Fields name the Boolean absolute-floor witness, exhaustive dichotomy and distinctness of false/true, the consistency→false and positive-cost→true selection rules, and an embedded T2 discreteness record.
Inhabitation is deferred to the sibling theorem t1_to_t2_bridge_holds, which fills the fields from the T−1→T0 bridge (floor witness, floor dichotomy, false≠true, consistency-zero) and from the forced Meta-Principle / Boolean cost, then assembles the T2 record. The structure exists so those witnesses are explicit fields rather than hidden cases/decide steps.
why it matters
Closes the T1→T2 arrow on the public forcing spine. Downstream, CompleteForcingChainT8 and the unified CompleteForcingChain both carry this bridge as a named link between forced Meta-Principle and two-state discreteness; the unified copy’s doc states the point: T1 alone only separates zero-cost consistency from positive cost, so T2 needs the Boolean floor from T−1→T0 exposed explicitly.
In the primer landmarks this is the discreteness step before T3 ledger bookkeeping, T4 recognition witness, T5 J-uniqueness ($J(x)=(x+x^{-1})/2-1$), T6 φ, T7 eight-tick, and T8 $D=3$. The honesty note on the full T8 chain warns that later T5 uniqueness does not consume the floor bridge substantively; this certificate still keeps the early spine auditable and non-hidden.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.