T1_FromDistinction
plain-language theorem explainer
Packages the T1 recognition-work axioms on the observable quotient forced by a distinction witness ∃x≠y in K. Inconsistent quotient configurations cost strictly positive work, zero-cost configurations are consistent, and the marked inconsistent Boolean lift is positive-cost. Downstream spine theorems cite this as the T1 floor after T0 transport. It is a Prop-structure (interface), not a proved theorem.
Claim. Given a type $K$ and a distinction witness $h:\exists x,y\in K,\, x\neq y$, the predicate $\mathrm{T1}$ on the forced observable quotient asserts three properties of the transported recognition-work cost $C$: (i) every inconsistent configuration $\Gamma$ satisfies $C(\Gamma)>0$; (ii) $C(\Gamma)=0$ implies $\Gamma$ is consistent; (iii) the marked inconsistent Boolean state (the image of $\mathsf{true}$ under the inverse quotient–Bool equivalence) has strictly positive cost.
background
This module closes Phase 1 of the T−1→T8 forcing path from a raw distinction witness rather than from a global Boolean chain. Given $h:\exists x,y\in K,,x\neq y$, the upstream construction builds the forced observable quotient $\mathrm{ForcedQuotient},h:=\mathrm{Quotient}(\mathrm{forcedObservableSetoid},h)$ and proves it equivalent to $\mathsf{Bool}$. Configuration space and recognition-work cost are then transported across that equivalence, yielding a T0 surface native to the distinction.
A configuration space supplies empty configuration, binary join, a consistency predicate, and an independence relation, with join a commutative monoid. Recognition cost $C$ is the work functional on those configurations. T1 is the classical cost–logic link: inconsistency is expensive, and free configurations are consistent. Here those axioms are stated on the forced quotient, not on bare $\mathsf{Bool}$.
proof idea
No proof body: this is a Prop-valued structure (definitional interface). Its three fields name the T1 obligations on $\mathrm{ForcedQuotient},h$ relative to $\mathrm{forcedQuotientRecognitionCost}$. Inhabitants are built downstream by distinction_T0_to_T1, which maps T0's contradiction_expensive to inconsistent_positive and the forward direction of T0's logic_emergent to zero_cost_consistent, with the marked-state positivity coming from the same T0 package.
why it matters
Places T1 on the distinction-generated floor so later spine steps never fall back to unthreaded global Bool facts. distinction_forces_T1 obtains an instance from any distinction via T0; distinction_T1_to_T2 consumes it to force T2 (state dichotomy) on the same quotient; DistinctionToT0_Spine records the completed early slice T−1 through T3. This is the T1 rung of the forcing chain (toward T5 J-uniqueness, T6 $\varphi$, T7 eight-tick, T8 $D=3$), routed through the transported recognition-work surface of Phase 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.