Foundation Distinction To T4 Distinction Forces T0 Spine

From one difference to a spine

In the Recognition Science framework, a distinction is the most basic possible fact: two things are not the same. The declaration distinction_forces_T0_spine is a machine-checked theorem that starts from just this fact and builds a tower of structure. It takes any collection K with two distinct elements, and from that one difference constructs a forced observable quotient, a two-valued configuration space, and a recognition-work cost on it. The theorem then proves that this constructed floor satisfies a sequence of separation properties, T0 through T4, in a single spine.

The spine is not a claim about physical space. It is a claim about a formal structure: given a distinction, the framework can build a Boolean algebra of observables and a cost function on it, and this algebra is provably equivalent to the simple two-element Boolean structure. The theorem distinction_forces_T0_spine bundles together the proofs that this constructed floor is T0, T1, T2, T3, and T4. Each step is a separate theorem: distinction_forces_T0, then distinction_forces_T1, and so on up to distinction_forces_T4. The spine is the packaged result that all five hold from the single starting distinction.

The construction works by taking the distinction witness, the proof that two elements differ, and using it to form a quotient of the original collection. This quotient is then shown to be equivalent to the Boolean type Bool, the two-element type with values true and false. The recognition-work cost on this quotient is transported from the Boolean cost, and the separation properties are proved for this transported floor. The key point is that the whole ladder is forced: no extra assumptions, no choices, just the one distinction and the framework's axioms.

What the declaration does not claim is just as important. It does not claim that physical space has four separation properties. It does not claim that the T4 spine is the same as the three-dimensional space of physics. The spine is a formal floor, a proof that a distinction is enough to generate a rich Boolean structure. The physical interpretation, the bridge from this formal spine to actual space, remains a separate open question. The theorem is a precise statement about the framework's internal logic, not a statement about the world.

/-- A distinction witness forces the T−1-to-T4 spine. -/
theorem distinction_forces_T0_spine
    (K : Type) (h : ∃ x y : K, x ≠ y) :
    DistinctionToT0_Spine K h where
  marked_pair := ⟨TMinus1ForcedFromDistinction.markedPairOfDistinction h⟩
  observable_floor := TMinus1ForcedFromDistinction.forcedObservableFloor h
  quotient_bool := ⟨forcedQuotientBoolEquiv h⟩
  t0 := distinction_forces_T0 h
  t1 := distinction_forces_T1 h
  t2 := distinction_forces_T2 h
  t3 := distinction_forces_T3 h
  t4 := distinction_forces_T4 h

/-- A distinction witness forces the T−1-to-T4 spine. -/
theorem distinction_forces_T0_spine
    (K : Type) (h : ∃ x y : K, x ≠ y) :
    DistinctionToT0_Spine K h where
  marked_pair := ⟨TMinus1ForcedFromDistinction.markedPairOfDistinction h⟩
  observable_floor := TMinus1ForcedFromDistinction.forcedObservableFloor h
  quotient_bool := ⟨forcedQuotientBoolEquiv h⟩
  t0 := distinction_forces_T0 h
  t1 := distinction_forces_T1 h
  t2 := distinction_forces_T2 h
  t3 := distinction_forces_T3 h
  t4 := distinction_forces_T4 h

/-- The forced quotient-to-Bool coordinate equivalence. -/
noncomputable def forcedQuotientBoolEquiv
    {K : Type*} (h : ∃ x y : K, x ≠ y) :
    ForcedQuotient h ≃ Bool :=
  forcedQuotientEquivBool h

What this page does not claim

The T4 spine is not a claim about physical space having four separation properties. The theorem does not establish the physical recognition-to-linking bridge; that remains open. The construction does not require any assumptions beyond the existence of two distinct elements.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/DistinctionToT4.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: