Foundation Self Bootstrap Distinguishability Bool Distinguishable

The smallest distinction

In mathematics, a distinction is the ability to tell two things apart. The Boolean type is the two-element set whose members are usually called false and true. The theorem bool_distinguishable states, in the framework's machine-checked library of formal theorems, that these two elements are not equal: false ≠ true. This is not a deep fact about physics; it is a definitional property of the Boolean type itself, verified by direct computation. The declaration records that the formal language in which the framework is written already contains at least one object-level distinction.

The same file proves a slightly more general statement. If any type K carries a Boolean predicate P that takes both values, meaning there is some x with P x = true and some y with P y = false, then K must have at least two distinct elements. This is the theorem distinguishability_lifted_from_bool. It shows that the existence of a two-valued predicate on a carrier is enough to force a distinction within that carrier. The proof is constructive: it takes the two witnesses and shows they cannot be equal, because equality would force a single element to have both Boolean values.

The file also proves a meta-level fact about propositions themselves. In classical logic, a proposition P is never equal to its own negation ¬P. This is the theorem prop_ne_not. Consequently, the claim that a carrier has at least two distinct elements is itself distinct from the denial of that claim. This is packaged as the theorem dist_claim_self_distinguishes, which states that the proposition "there exist x y with x ≠ y" is not equal to its negation.

In Recognition Science, this file is labeled Route A for the absolute-floor program. The program asks how the framework gets any distinction at all, given that its starting point is a ledger, a discrete record of events. The honest answer recorded here is that the framework does not derive an object-level non-singleton carrier from nothing. Instead, it proves meta-level facts: the formal language already distinguishes propositions, and the proposition asserting object-level distinguishability is distinct from its own denial. The certificate structure SelfBootstrapCert packages these two facts, and the theorem selfBootstrapCert shows the certificate is theorem-backed.

What this does not claim is important. The theorem distinguishability_forced_given_object_witness takes as a hypothesis the existence of two distinct elements in the carrier and returns that same existence as a conclusion. It does not manufacture the witness. The file explicitly says it does not pretend to derive an object-level non-singleton carrier from nothing. The self-bootstrap route closes at the meta-language floor, not below it. The object-level non-singleton condition remains named as a hypothesis, not derived as a theorem.

/-- The two-element type carries a definitional distinction. -/
theorem bool_distinguishable : (false : Bool) ≠ true := by
  decide

/-- Any carrier supporting a Boolean predicate with both truth values
inherits an object-level distinction. -/
theorem distinguishability_lifted_from_bool
    {K : Type*} (P : K → Bool)
    (hpos : ∃ x : K, P x = true) (hneg : ∃ x : K, P x = false) :
    ∃ x y : K, x ≠ y := by
  obtain ⟨x, hx⟩ := hpos
  obtain ⟨y, hy⟩ := hneg
  refine ⟨x, y, ?_⟩
  intro hxy
  have hfalse : P x = false := by
    simpa [hxy] using hy
  cases hx.symm.trans hfalse

/-- A proposition is never equal to its negation in classical logic. -/
theorem prop_ne_not (P : Prop) : P ≠ ¬ P := by
  intro h
  by_cases hp : P
  · have hnp : ¬ P := by
      rw [h] at hp
      exact hp
    exact hnp hp
  · have hp' : P := by
      rw [h.symm] at hp
      exact hp
    exact hp hp'

/-- The claim that a carrier admits a non-trivial distinction is itself
distinguishable from the denial of that claim. -/
theorem dist_claim_self_distinguishes (K : Type*) :
    (∃ x y : K, x ≠ y) ≠ (¬ ∃ x y : K, x ≠ y) :=
  prop_ne_not (∃ x y : K, x ≠ y)

/-- Route A, honest form: object-level distinguishability is never weaker
than the meta-level fact that the formal language already distinguishes
`Prop` values. The object-level non-singleton condition is still named. -/
theorem distinguishability_forced_given_object_witness
    (K : Type*) (_h_meta_dist : ∃ P Q : Prop, P ≠ Q)
    (h_at_least_two_in_carrier : ∃ x y : K, x ≠ y) :
    ∃ x y : K, x ≠ y :=
  h_at_least_two_in_carrier

What this page does not claim

The declaration does not derive the existence of a non-singleton carrier from nothing. The theorem distinguishability_forced_given_object_witness does not manufacture a witness; it only returns a supplied hypothesis. The file does not prove that any particular physical system has two distinct states; it only proves facts about the formal language.

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