dist_claim_self_distinguishes
plain-language theorem explainer
The theorem shows that for any type K the proposition asserting existence of distinct elements differs from its negation. Researchers on self-bootstrap arguments in Recognition Science cite it to confirm the meta-language already encodes non-trivial propositional distinctions. The proof is a direct term application of the general lemma that no proposition equals its negation.
Claim. For any type $K$, the proposition asserting the existence of distinct elements satisfies $P ≠ ¬P$ where $P$ is the statement $∃ x y : K, x ≠ y$.
background
The module records the Lean-checkable meta-level facts for the self-bootstrap argument under Route A of the absolute-floor program. It establishes that the formal language distinguishes propositions and that the claim of object-level distinguishability differs from its denial, without deriving a non-singleton carrier from nothing. The key upstream result is the theorem that any proposition P satisfies P ≠ ¬P in classical logic, which is instantiated here on the existential claim over K.
proof idea
The proof is a one-line term wrapper that applies the lemma prop_ne_not directly to the proposition ∃ x y : K, x ≠ y.
why it matters
This declaration supplies the claim_not_its_negation field in the selfBootstrapCert theorem that assembles the full self-bootstrap certificate. It completes the meta-level portion of the distinguishability argument in the Foundation module. Within Recognition Science it anchors the absolute-floor program by verifying that the formal system already distinguishes the relevant propositions at the meta-level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.