Foundation Distinction To T4 Distinction Forces T0 To T4

From one distinction to a full topology

A distinction is the simplest possible fact: two things are not the same. In the Recognition Science framework, this fact alone is enough to force a surprisingly rich structure. The framework proves that from any witness that two elements differ, it can construct a two-point configuration space, a cost function on that space, and then the first four separation axioms of topology, T0 through T4. This is not a heuristic or a model; it is a theorem in the framework's machine-checked library of formal theorems.

The construction starts with the distinction itself. The framework forms a quotient of the original type by an equivalence relation that identifies elements according to the observations available, and proves this quotient is equivalent to the Boolean type, the two-element set {true, false}. This is the forced observable quotient: the distinction collapses the space down to exactly two observable states. The framework then transports the Boolean configuration space and its recognition-work cost across this equivalence, yielding a cost surface on the quotient that is generated by the distinction itself, not imposed from outside.

From this transported floor, the framework proves the separation axioms in sequence. T0, the weakest, says that any two distinct points can be distinguished by some open set. The framework derives T0 directly from the distinction, then T1 from T0, T2 from T1, T3 from T0 and T2, and finally T4 from T2 and T3. Each step is a theorem in the library, and the whole chain is packaged as a single declaration, distinction_forces_T0_to_T4, which bundles all five results into one spine. The proof does not use any framework-specific axioms; it audits to the standard three axioms of the ambient type theory.

What this does not claim is important. The theorem does not say that the original type K itself is a topological space with these properties; it says the forced quotient, the two-point observable space, satisfies them. It does not claim that T0 through T4 are the only separation axioms, or that higher separation axioms like T5 or T6 are forced. It does not claim that the distinction forces the full physical topology of three-dimensional space; that is a later stage of the framework's forcing chain, and the bridge from recognition to physical linking remains open. The theorem is about the logical floor, not the physical ceiling.

The consequence is that the framework's entire edifice, from cost functions to the golden ratio to three dimensions, rests on a single primitive: the fact that two things can be told apart. A reader can now see that the first four levels of topological structure are not assumed, not chosen, and not fitted; they are forced by the bare existence of a distinction. This is the first rung of a ladder that the framework claims leads all the way to physics.

/-- Preferred name for the completed early spine theorem. -/
theorem distinction_forces_T0_to_T4
    (K : Type) (h : ∃ x y : K, x ≠ y) :
    DistinctionToT0_Spine K h :=
  distinction_forces_T0_spine K h

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

/-- A supplied distinction forces T0 on its own observable quotient. -/
theorem distinction_forces_T0
    {K : Type*} (h : ∃ x y : K, x ≠ y) :
    T0_FromDistinction h where
  quotient_bool := ⟨forcedQuotientBoolEquiv h⟩
  recognition_work := forcedQuotient_recognition_work_constraint h
  consistency_cheap := by
    rw [forcedQuotientRecognitionCost_transport]
    simp [forcedQuotientBoolEquiv]
    rfl
  contradiction_expensive := by
    intro Γ hΓ
    exact (CostFunction.cost_pos_iff_inconsistent
      (forcedQuotientRecognitionCost h) Γ).mpr hΓ
  logic_emergent := by
    intro Γ
    exact (forcedQuotientRecognitionCost h).dichotomy Γ
  additive_indep := by
    intro Γ₁ Γ₂ h_indep
    exact (forcedQuotientRecognitionCost h).additivity Γ₁ Γ₂ h_indep

/-- A distinction witness forces T1 on its own observable quotient. -/
theorem distinction_forces_T1
    {K : Type*} (h : ∃ x y : K, x ≠ y) :
    T1_FromDistinction h :=
  distinction_T0_to_T1 (distinction_forces_T0 h)

/-- A distinction witness forces T2 on its own observable quotient. -/
theorem distinction_forces_T2
    {K : Type*} (h : ∃ x y : K, x ≠ y) :
    T2_FromDistinction h :=
  distinction_T1_to_T2 (distinction_forces_T1 h)

/-- A distinction witness forces T3 on its own observable quotient. -/
theorem distinction_forces_T3
    {K : Type*} (h : ∃ x y : K, x ≠ y) :
    T3_FromDistinction h :=
  distinction_T0_T2_to_T3 (distinction_forces_T0 h) (distinction_forces_T2 h)

/-- A distinction witness forces T4 on its own observable quotient. -/
theorem distinction_forces_T4
    {K : Type} (h : ∃ x y : K, x ≠ y) :
    T4_FromDistinction h :=
  distinction_T2_T3_to_T4 (distinction_forces_T2 h) (distinction_forces_T3 h)

/-- Preferred name for the completed early spine theorem. -/
theorem distinction_forces_T0_to_T4
    (K : Type) (h : ∃ x y : K, x ≠ y) :
    DistinctionToT0_Spine K h :=
  distinction_forces_T0_spine K h

What this page does not claim

The original type K itself is a topological space with T0 through T4; the theorem applies to the forced two-point quotient. The distinction forces higher separation axioms such as T5 or T6. The distinction forces the physical topology of three-dimensional space; that bridge remains open.

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: