Foundation Tminus1 Forced From Distinction Forced Boolean Coordinates Unique Up

The Boolean floor

A Boolean coordinate system is a way of assigning one of two labels, commonly written false and true, to every element of a collection. The theorem forcedBooleanCoordinates_unique_up_to_bool_aut states a precise uniqueness result: given any witness that two distinct elements exist, the two-valued coordinate system built from that witness is unique up to a Boolean automorphism, meaning the only freedom is a global swap of the two labels.

The construction starts with a distinction witness, a proof that there exist two different elements in the underlying type. From that witness the framework builds a marked pair, a projection onto the two Boolean values, an equivalence relation identifying elements with the same projection, and finally a quotient that is equivalent to the Boolean type. The uniqueness theorem then shows that any two such coordinate systems are related by a single invertible map on the Boolean type, which must be either the identity or the swap. This is the strongest possible statement: the labels themselves are arbitrary, but the partition into two classes is forced.

In Recognition Science, this result establishes the Boolean observable floor, the minimal two-valued layer of observation, as a consequence of distinction rather than an assumption. The framework's library, a machine-checked collection of formal theorems, proves that if no object-level distinction exists, no object-level forcing occurs; but once a distinction is given, the two-valued floor is not an extra measure. The theorem also supplies a legacy raw floor required by an existing certificate structure, preserving the strong thesis that the entire T−1 floor interface is forced by the supplied witness.

The theorem does not claim that the two labels have any intrinsic meaning, nor that the choice of which element is marked as base or alternate is canonical. It does not assert that the Boolean floor is the only observable structure, only that it is the unique two-valued one. The uniqueness is up to automorphism, so the framework does not privilege any particular assignment of false and true to the two classes.

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

/-- Extract the marked pair carried by a distinction witness. -/
noncomputable def markedPairOfDistinction
    {K : Type*} (h : ∃ x y : K, x ≠ y) : MarkedPair K where
  base := Classical.choose h
  alt := Classical.choose (Classical.choose_spec h)
  distinct := Classical.choose_spec (Classical.choose_spec h)

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

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

What this page does not claim

The theorem does not assign intrinsic meaning to the labels false and true. It does not claim the Boolean floor is the only observable structure, only the unique two-valued one. It does not assert that the choice of which element is marked as base or alternate is canonical.

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: