Foundation Self Bootstrap Distinguishability Dist Claim Self Distinguishes

The self-distinguishing claim

In classical logic, a proposition is never equal to its own negation. The Recognition Science declaration dist_claim_self_distinguishes applies this general fact to a specific statement: the claim that a carrier has at least two distinct elements. The declaration proves, as a theorem, that this claim is not equal to the denial of that claim. In plain terms, the statement "there exist two different things" is itself different from the statement "it is not the case that there exist two different things." This is a meta-level fact: it is about the formal language in which the claim is expressed, not about any particular collection of objects.

The declaration is part of a larger argument called the self-bootstrap route, which aims to show that the framework's formal language already contains distinctions. The theorem bool_distinguishable establishes that the two Boolean values, false and true, are distinct. A further theorem, distinguishability_lifted_from_bool, shows that any carrier supporting a Boolean predicate taking both truth values inherits an object-level distinction: if a predicate returns true for one element and false for another, those two elements must be different. The self-distinguishing claim then works at the level of propositions themselves, showing that the formal language distinguishes the claim of object-level distinguishability from its own denial.

The declaration does not derive an object-level non-singleton carrier from nothing. The documentation states this plainly: it does not pretend to derive such a carrier. The theorem distinguishability_forced_given_object_witness makes the condition explicit: if a carrier already has at least two distinct elements, then it has at least two distinct elements. This is a tautology, not a derivation. The self-bootstrap certificate, SelfBootstrapCert, records the two meta-level facts the route actually proves: the meta-language distinguishes propositions, and the claim about object-level distinguishability is not its own negation. The route closes at the meta-language floor, not below it.

What this means for the framework is modest but exact. The formal language in which Recognition Science is written already contains distinctions at the level of propositions. The claim that some carrier has two distinct elements is itself distinct from the denial of that claim. This is a theorem about logic, not a theorem about the physical world. It does not establish that any particular carrier, such as the real numbers or the framework's cost function, has two distinct elements. It does not establish that the universe contains distinct objects. It establishes only that the formal language can distinguish a claim from its denial, which is a property of the logic itself.

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

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

/-- 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 an object-level non-singleton carrier from nothing. The declaration does not establish that any particular carrier, such as the real numbers or the framework's cost function, has two distinct elements. The declaration does not establish that the universe contains distinct objects.

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: