distinction_T0_to_T1
plain-language theorem explainer
Given a distinction witness on a type K, T0 on the forced observable quotient implies T1 on that same quotient: inconsistent states cost positively, zero-cost states are consistent, and the marked inconsistent Boolean state is expensive. Anyone closing the distinction-to-T4 spine cites this bridge. The proof fills the three T1 fields by transporting T0's contradiction-expensive and logic-emergent facts across the forced quotient–Bool equivalence.
Claim. Let $K$ be any type with a distinction witness $h:\exists x,y\in K.\, x\neq y$. If the forced observable quotient of $h$ satisfies the distinction-local T0 package (Boolean quotient, transported recognition-work surface, cheap consistency, expensive contradiction), then it satisfies the distinction-local T1 package: every inconsistent quotient configuration has positive recognition-work cost, every zero-cost configuration is consistent, and the marked inconsistent Boolean state is strictly expensive.
background
This module opens Phase 1 of the T−1→T8 closure from a raw distinction witness rather than from a global Boolean floor. Given $h:\exists x,y\in K.,x\neq y$, the upstream construction builds the forced observable quotient $\mathrm{ForcedQuotient},h$ and proves it equivalent to $\mathrm{Bool}$ via forcedQuotientBoolEquiv. Configuration space and recognition-work cost are transported across that equivalence, so the recognition-work surface lives on the quotient generated by the witness itself.
T0_FromDistinction packages the distinction-local T0 facts: the quotient is Boolean, carries a recognition-work constraint certificate, consistency is cheap, contradiction is expensive, and logic emerges (zero cost iff consistency). T1_FromDistinction is the next rung on that same quotient: inconsistent states cost positively, zero-cost states are consistent, and a marked inconsistent state is expensive. The present theorem is the pure implication T0⇒T1 on that transported floor.
proof idea
Structure-field construction, not a deep argument. The T1 field inconsistent_positive is definitionally the T0 field contradiction_expensive. The field zero_cost_consistent is the forward direction of T0's logic_emergent equivalence applied pointwise. For marked_inconsistent_positive, apply contradiction_expensive to the preimage of true under forcedQuotientBoolEquiv, then discharge the inconsistency side-condition by simplifying the equivalence so that the image is not false. No external lemmas beyond the in-module Bool equivalence and the T0 package fields.
why it matters
This is the T0→T1 step on the distinction-generated quotient, not on unthreaded global Bool. Downstream, distinction_forces_T1 is the one-line composition distinction_T0_to_T1 (distinction_forces_T0 h), so every later T2–T4 fact routed through the transported floor depends on this bridge. In the UnifiedForcingChain landmarks this is the local analogue of the early spine after T−1: once distinction forces a Boolean recognition-work surface (T0), inconsistency must be costly (T1). The module doc frames the whole file as Phase 1 of full T−1→T8 closure; without this implication the chain would still lean on global Bool facts the witness never justified.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.