distinguishability_lifted_from_bool
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.