empty_has_no_self_recognition
plain-language theorem explainer
Emptiness of a type X precludes any binary relation R on X together with an element x satisfying R x x. Researchers formalizing the Recognition Science meta-principle cite this result to establish that recognition structures demand non-empty domains before any ledger or self-similar closure can arise. The proof is a direct term-mode contradiction that applies the eliminator of the emptiness hypothesis to the witness x.
Claim. If a type $X$ is empty, then there does not exist a binary relation $R : X → X → Prop$ and an element $x ∈ X$ such that $R(x,x)$.
background
The module formalizes the meta-principle that nothing cannot recognize itself: recognition requires a recognizer, so empty recognition is impossible. This statement opens the derivation chain MP → Ledger (double-entry necessity) → φ (self-similar closure) → constants. The theorem uses only the standard IsEmpty eliminator and does not invoke the sibling definitions RecognitionStructure or MinimalLedger.
proof idea
The term proof introduces the existential witness consisting of a relation R and element x with R x x, then applies the eliminator h.elim x supplied by the IsEmpty hypothesis to obtain a contradiction.
why it matters
The result supplies the formal content of the meta-principle in the RRF foundation module and is the first step toward the ledger and phi-ladder constructions. It directly supports the module claim that MP is a theorem rather than an axiom. No downstream uses are recorded yet; the open question it leaves is how non-empty recognition structures are populated to reach the eight-tick octave and D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.