Foundation Distinction To T4 Distinction Forces T0

The distinction floor

A distinction is the simplest possible fact: two things are not the same. The Recognition Science declaration distinction_forces_T0 proves that this fact alone forces a two-valued configuration space. Given any type K with two distinct elements, the theorem constructs a quotient of K whose states are exactly the two Boolean values, true and false. The construction is not an assumption about the world; it is a theorem in the framework's machine-checked library of formal theorems.

The declaration then proves that this two-valued space satisfies T0, the weakest separation axiom in topology. T0 says that for any two distinct points, at least one has a neighborhood not containing the other. The framework's library shows this property follows from the forced quotient, and then chains further theorems: T0 forces T1, T1 forces T2, T0 and T2 together force T3, and T2 with T3 forces T4. The single theorem distinction_forces_T0_to_T4 bundles the whole spine, so one distinction yields the first four separation axioms.

In plain terms, the framework models a ledger, a discrete record of events, and a recognition, the act of telling two entries apart. The theorem says that the cost of recognition, the work required to distinguish two states, is forced by the distinction itself. The quotient's two states are the empty configuration and its complement, and the recognition cost on each state is transported from the Boolean cost function, so the framework's cost structure survives the quotient.

The theorem does not claim that physical space is two-dimensional, that T4 is the end of the forcing chain, or that the quotient is the only possible configuration space. It establishes a floor: the minimal structure that any distinction forces. The value of the result is that the framework's early spine does not depend on a global Boolean assumption; it is generated by the distinction witness itself.

/-- 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

/-- 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 transported cost is literally the Boolean recognition cost under the
forced quotient coordinate. -/
theorem forcedQuotientRecognitionCost_transport
    {K : Type*} (h : ∃ x y : K, x ≠ y) (Γ : ForcedQuotient h) :
    (forcedQuotientRecognitionCost h).C Γ =
      UnifiedForcingChain.TMinus1ToT0.boolRecognitionCost.C
        (forcedQuotientBoolEquiv h Γ) :=
  rfl

What this page does not claim

The theorem does not claim physical space is two-dimensional. The theorem does not claim T4 is the end of the forcing chain. The quotient is not claimed to be the only possible configuration space.

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: