distinction_T0_T2_to_T3
plain-language theorem explainer
Given a distinction witness on a type K, T0 and T2 on the forced observable quotient already imply T3 on that same quotient. Anyone threading the early forcing spine from a concrete inequality rather than global Bool cites this bridge. The proof is a short structure assembly: empty-cost and additive independence come from T0; monoid neutrality of empty join is ConfigSpace law.
Claim. Let $K$ be any type with a distinction witness $h:\exists x,y\in K.\, x\neq y$. If the forced observable quotient carries the T0 recognition-work surface (Boolean equivalence, transported cost, zero cost on the empty consistent state, additive independence) and the T2 dichotomy (exactly two distinct quotient states), then it carries T3: empty state cost zero, empty join left-neutral with cost neutrality, and independent joins additive.
background
This module closes Phase 1 of the T−1→T8 spine from a supplied distinction rather than from unthreaded global Bool. A witness $h:\exists x,y\in K.,x\neq y$ induces the forced observable quotient, proved equivalent to Bool. Configuration space and recognition-work cost are transported across that equivalence.
A configuration space supplies an empty entry emp, a binary join, consistency, and independence, with join a commutative monoid and emp the identity. T0 on the distinction quotient asserts Boolean equivalence, a recognition-work certificate, zero cost on the empty consistent state, and additive cost on independent joins. T2 asserts the two forced Boolean-coordinate states exhaust the quotient and are distinct. T3 packages the empty-cost, empty-join neutrality, and independent-join additivity laws on that same quotient floor.
proof idea
Structure construction for T3 on the forced quotient. The empty-balanced field is exactly T0's consistency_cheap (zero cost on empty). Empty-join left identity is ConfigSpace.emp_join applied to each quotient state. Empty-join cost neutrality rewrites by that same identity. Independent-join additivity is T0's additive_indep. The T2 hypothesis is accepted for the chain signature but unused in the body; all content comes from T0 plus ConfigSpace monoid laws.
why it matters
Fills the T0+T2⇒T3 step on the distinction-generated quotient, so the early forcing spine is threaded by the witness rather than by global Boolean facts. Downstream, distinction_forces_T3 is the one-line composition of the forced T0 and T2 packages through this bridge: a distinction alone yields T3 on its own quotient. That is the T3 rung of Phase 1 toward T4 and the full UnifiedForcingChain (T0–T8), including later J-uniqueness, φ, the eight-tick octave, and D=3. Without this transport, T3 would sit on an unlinked Bool floor and fail the module's closure mandate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.