Foundation Tminus1 Forced From Distinction Forced Bool Representative Left Inv

The Boolean coordinate round trip

A distinction is the simplest possible fact: two things are not the same. Given any such pair, one can ask whether the two sides can be safely labeled, say false and true, without losing information. The theorem forcedBoolRepresentative_left_inv answers that question in the affirmative. It states that if you take a side, label it, and then look up which side that label names, you get the side you started with. The round trip from side to label and back is the identity.

The statement is a precise algebraic property. The framework builds a ledger, a discrete record of events, from a distinction witness, a proof that two objects differ. It then forms a quotient, a compressed view where objects are identified when they behave the same way, and shows this quotient is equivalent to the two-element Boolean type. The theorem in question is the left inverse half of that equivalence: the map from Boolean labels back to quotient classes, followed by the map from classes to labels, returns the original class. Its companion theorem supplies the right inverse, so the two maps are genuine inverses and the equivalence is exact.

The result is proved in a machine-checked library of formal theorems, meaning no step of the argument is left to informal judgment. It is part of a larger construction: from a single distinction, the framework derives a marked pair, a Boolean projection, an observable equivalence relation, and a two-class quotient, all without assuming any extra structure. The theorem establishes that this derived Boolean coordinate system is coherent: labels do not collide or vanish.

What the theorem does not claim is equally important. It does not assert that any particular distinction exists; it takes a distinction as a given premise. It does not say that the Boolean labeling is unique in an absolute sense, only that any two such labelings are related by a Boolean automorphism, a relabeling of true and false. It does not claim that the framework's full recognition chain, the sequence of results leading to the golden ratio and three spatial dimensions, follows from this theorem alone. It is one rung, not the whole ladder.

The practical upshot is that the framework's foundational floor is not an extra assumption. Once a distinction is supplied, the Boolean/observable structure is forced, not chosen. This matters because it means the simplest possible fact, that two things differ, already carries a complete two-valued coordinate system within it.

/-- Every quotient class is equal to the representative of its Boolean value. -/
theorem forcedBoolRepresentative_left_inv
    {K : Type*} (h : ∃ x y : K, x ≠ y)
    (q : Quotient (forcedObservableSetoid h)) :
    forcedBoolRepresentative h (forcedQuotientToBool h q) = q := by
  refine Quotient.inductionOn q ?_
  intro z
  by_cases hz : forcedBoolProjection h z = false
  · simp [forcedQuotientToBool, forcedBoolRepresentative, hz]
    exact Quotient.sound (by
      change forcedBoolProjection h (markedPairOfDistinction h).base =
        forcedBoolProjection h z
      simp [hz])
  · have hztrue : forcedBoolProjection h z = true := by
      cases hp : forcedBoolProjection h z
      · exact False.elim (hz hp)
      · rfl
    simp [forcedQuotientToBool, forcedBoolRepresentative, hztrue]
    exact Quotient.sound (by
      change forcedBoolProjection h (markedPairOfDistinction h).alt =
        forcedBoolProjection h z
      simp [hztrue])

/-- 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 supplied distinction forces a two-class observable Boolean floor. -/
theorem booleanObservableFloor_forced_from_distinction
    {K : Type*} (h : ∃ x y : K, x ≠ y) :
    Nonempty (Quotient (forcedObservableSetoid h) ≃ Bool) :=
  ⟨forcedQuotientEquivBool h⟩

/-- Every quotient class is equal to the representative of its Boolean value. -/
theorem forcedBoolRepresentative_left_inv
    {K : Type*} (h : ∃ x y : K, x ≠ y)
    (q : Quotient (forcedObservableSetoid h)) :
    forcedBoolRepresentative h (forcedQuotientToBool h q) = q := by
  refine Quotient.inductionOn q ?_
  intro z
  by_cases hz : forcedBoolProjection h z = false
  · simp [forcedQuotientToBool, forcedBoolRepresentative, hz]
    exact Quotient.sound (by
      change forcedBoolProjection h (markedPairOfDistinction h).base =
        forcedBoolProjection h z
      simp [hz])
  · have hztrue : forcedBoolProjection h z = true := by
      cases hp : forcedBoolProjection h z
      · exact False.elim (hz hp)
      · rfl
    simp [forcedQuotientToBool, forcedBoolRepresentative, hztrue]
    exact Quotient.sound (by
      change forcedBoolProjection h (markedPairOfDistinction h).alt =
        forcedBoolProjection h z
      simp [hztrue])

What this page does not claim

This theorem alone does not force the golden ratio or the three spatial dimensions of the broader framework. The theorem does not prove that any distinction exists; it only works from a supplied distinction witness. The Boolean coordinates are unique only up to a relabeling of true and false, not in an absolute sense.

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: