Foundation Distinction To T4 Distinction Forces T1

What a distinction forces

A distinction is the fact that two things are not the same. In the Recognition Science framework, this fact is a starting point: the framework asks what must be true about any system that can tell two things apart. The theorem distinction_forces_T1 is a machine-checked result in the framework's library of formal theorems. It states that from a witness to a distinction, a certain structure called T1 follows. This T1 structure is a set of properties about a cost function, a rule that assigns a number to each possible state of a system.

The framework builds this from a quotient, a mathematical construction that treats things as equivalent when they cannot be told apart. Given a distinction, the framework forms a quotient of the original space of states, and proves this quotient is equivalent to the two-element set Bool, the set containing true and false. This is the simplest possible configuration space: two states, which the framework identifies with the two outcomes of a distinction. The cost function on this quotient is then transported from the Boolean configuration space, and the T1 properties are proved to hold for it.

The T1 properties are about how the cost function behaves. One property says that an inconsistent state, one that contradicts the distinction, has positive cost. Another says that a state with zero cost must be consistent. A third says that the marked inconsistent state, the one that is definitely false, also has positive cost. These are not assumptions; they are conclusions that follow from the distinction alone, given the framework's definition of cost and its forcing chain.

The theorem is part of a larger spine. The same module proves that a distinction forces T0, T1, T2, T3, and T4 in sequence, each building on the previous. This is the first phase of a closure from a distinction to the framework's full structure of eight ticks and three dimensions. The theorem does not claim that any particular physical system has a distinction; it says that if one exists, then this structure follows. It does not claim that the cost function is unique, only that the T1 properties hold for the cost constructed on the quotient. It does not claim that the quotient is the only possible configuration space, only that it is the one forced by the distinction under the framework's rules.

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

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

/-- T0 on the forced quotient forces T1 on the forced quotient. -/
theorem distinction_T0_to_T1
    {K : Type*} {h : ∃ x y : K, x ≠ y}
    (h0 : T0_FromDistinction h) :
    T1_FromDistinction h where
  inconsistent_positive := h0.contradiction_expensive
  zero_cost_consistent := fun Γ hzero => (h0.logic_emergent Γ).mp hzero
  marked_inconsistent_positive := by
    exact h0.contradiction_expensive ((forcedQuotientBoolEquiv h).symm true) (by
      change forcedQuotientBoolEquiv h ((forcedQuotientBoolEquiv h).symm true) ≠ false
      simp [forcedQuotientBoolEquiv])

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

What this page does not claim

The theorem does not claim that any particular physical system contains a distinction. The theorem does not claim that the cost function on the quotient is the only possible one. The theorem does not claim that the quotient is 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: