Foundation Tminus1 Forced From Distinction Raw Floor Forced From Distinction

The forced floor

In mathematics, a distinction is simply the fact that two objects are not the same. The Recognition Science framework begins with this primitive idea: a witness that there exist two distinct elements, written as ∃ x y, x ≠ y. The declaration rawFloor_forced_from_distinction is a theorem in the framework's machine-checked library of formal theorems. It states that from any such witness, one can construct a marked pair, a Boolean projection, an observable equivalence relation, and a two-class quotient, all without adding any new assumptions. The name "raw floor" refers to the minimal structural layer this construction establishes.

The theorem itself is deliberately modest. Its statement is simply that if there exist two distinct elements, then there exist two distinct elements. This is a tautology in classical logic, but the framework treats it as a load-bearing principle. The declaration proves that the entire Boolean and observable floor is forced by the given distinction, rather than being an external admissibility package. The framework's library shows that from the witness, one can construct a marked pair, a Boolean projection, the observable equivalence relation generated by that projection, the two-class quotient, and uniqueness of Boolean coordinates up to Boolean automorphism. Each of these constructions is a separate theorem in the same module, and each depends on the original distinction witness.

The key consequence is that the framework does not assume a structure; it derives it. If there is no object-level distinction, there is no object-level forcing. But once the distinction is given, the Boolean and observable floor is not an extra measure. This is the non-half-measure version of the T−1 repair, meaning it does not rely on an external admissibility package. The framework's library also proves that the Boolean structure is unique up to a Boolean automorphism, which means the coordinates are essentially canonical. The distinction witness is the sole input, and everything else follows.

What the declaration does not claim is equally important. It does not claim that a distinction can be created from nothing. The theorem requires a witness as input; it does not prove that such a witness must exist. It does not claim that the constructed Boolean structure is the only possible structure, only that it is unique up to automorphism given the construction. It does not claim anything about the physical world; it is a purely formal result about types and quotients. The framework's library also shows that the construction works for the Boolean type itself, but this is a special case, not a general statement about all types.

/-- The supplied distinction forces the raw floor expected by the legacy
certificate interface. -/
theorem rawFloor_forced_from_distinction
    {K : Type*} (h : ∃ x y : K, x ≠ y) :
    ∃ x y : K, x ≠ y :=
  h

/-- The distinction witness gives two representatives not identified by the
observable relation it generates. -/
theorem forcedObservableFloor
    {K : Type*} (h : ∃ x y : K, x ≠ y) :
    ObservableFloorWitness K (forcedObservableSetoid h).r := by
  refine ⟨(markedPairOfDistinction h).base, (markedPairOfDistinction h).alt, ?_⟩
  intro hrel
  simp [forcedObservableSetoid] at hrel

/-- The Boolean projection forced by a chosen distinction witness. -/
noncomputable def forcedBoolProjection
    {K : Type*} (h : ∃ x y : K, x ≠ y) : K → Bool :=
  boolProjection (markedPairOfDistinction h)

/-- The observable equivalence relation forced by a distinction: two
representatives are equivalent exactly when the forced Boolean projection gives
the same value on them. -/
noncomputable def forcedObservableSetoid
    {K : Type*} (h : ∃ x y : K, x ≠ y) : Setoid K where
  r x y := forcedBoolProjection h x = forcedBoolProjection h y
  iseqv := by
    constructor
    · intro x
      rfl
    · intro x y hxy
      exact hxy.symm
    · intro x y z hxy hyz
      exact hxy.trans hyz

/-- The observable quotient generated by a distinction is equivalent to Bool. -/
noncomputable def forcedQuotientEquivBool
    {K : Type*} (h : ∃ x y : K, x ≠ y) :
    Quotient (forcedObservableSetoid h) ≃ Bool where
  toFun := forcedQuotientToBool h
  invFun := forcedBoolRepresentative h
  left_inv := forcedBoolRepresentative_left_inv h
  right_inv := forcedQuotientToBool_representative h

/-- Boolean coordinates forced by the same distinction are unique up to Boolean
automorphism. -/
theorem forcedBooleanCoordinates_unique_up_to_bool_aut
    {K : Type*} {h : ∃ x y : K, x ≠ y}
    (c₁ c₂ : ForcedBooleanCoordinates h) :
    c₂.coord = c₁.coord.trans (forcedBooleanCoordinateChange c₁ c₂) := by
  ext q
  simp [forcedBooleanCoordinateChange]

/-- Boolean coordinates forced by the same distinction are unique up to Boolean
automorphism. -/
theorem forcedBooleanCoordinates_unique_up_to_bool_aut
    {K : Type*} {h : ∃ x y : K, x ≠ y}
    (c₁ c₂ : ForcedBooleanCoordinates h) :
    c₂.coord = c₁.coord.trans (forcedBooleanCoordinateChange c₁ c₂) := by
  ext q
  simp [forcedBooleanCoordinateChange]

What this page does not claim

The theorem does not prove that a distinction witness must exist; it only shows what follows if one is given. The construction does not claim to be the only possible Boolean structure, only unique up to automorphism. The result is purely formal and makes no statement about physical reality.

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/TMinus1ForcedFromDistinction.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: