distinguishability_lifted_from_bool
A type K equipped with a predicate P to Bool that attains both true and false must contain at least two distinct elements. Researchers formalizing the self-bootstrap argument in Recognition Science cite this to obtain object-level distinction from a Boolean predicate without assuming a non-singleton carrier in advance. The proof extracts witnesses for each truth value and derives a contradiction from the assumption that they coincide via substitution and case analysis on Booleans.
claimLet $K$ be a type and $P : K → Bool$ a predicate. If there exists $x ∈ K$ with $P(x) = true$ and there exists $y ∈ K$ with $P(y) = false$, then there exist distinct $x', y' ∈ K$.
background
This theorem sits in the SelfBootstrapDistinguishability module, which records the Lean-checkable portion of the self-bootstrap argument for the absolute-floor program. The module establishes meta-level facts: the formal language distinguishes propositions, and the proposition asserting object-level distinguishability differs from its denial. It does not derive a non-singleton carrier from nothing but supplies the precise distinctions the argument requires.
proof idea
The tactic proof obtains witnesses x from the positive existential and y from the negative existential. It refines to the pair x, y and assumes for contradiction that x equals y. Substitution into the negative witness produces P x = false, which contradicts the positive witness by case analysis on the resulting Boolean equality.
why it matters in Recognition Science
The result supplies a foundational step in the self-bootstrap argument by showing that any carrier supporting a Boolean predicate with both truth values inherits object-level distinction. It fills the meta-level facts required by the absolute-floor program in Recognition Science. No downstream uses appear in the current graph, indicating it functions as a base lemma for later bootstrap constructions.
scope and limits
- Does not derive distinguishability from an empty carrier or a constant predicate.
- Does not invoke Recognition Science constants such as phi or the J-cost function.
- Does not address distinctions beyond object-level inequality of elements.
- Does not assume any specific structure on K beyond the existence of the predicate witnesses.
formal statement (Lean)
26theorem distinguishability_lifted_from_bool
27 {K : Type*} (P : K → Bool)
28 (hpos : ∃ x : K, P x = true) (hneg : ∃ x : K, P x = false) :
29 ∃ x y : K, x ≠ y := by
proof body
Tactic-mode proof.
30 obtain ⟨x, hx⟩ := hpos
31 obtain ⟨y, hy⟩ := hneg
32 refine ⟨x, y, ?_⟩
33 intro hxy
34 have hfalse : P x = false := by
35 simpa [hxy] using hy
36 cases hx.symm.trans hfalse
37
38/-- A proposition is never equal to its negation in classical logic. -/