recognition_implies_existence
plain-language theorem explainer
If a type admits a binary relation with at least one self-loop, then the type is nonempty. Recognition Science derivations cite this to extract a substrate from the meta-principle before building the ledger and phi-ladder. The proof is a direct one-line application of the MetaPrinciple theorem to the supplied hypothesis.
Claim. If there exists a relation $R : X → X → Prop$ and an element $x ∈ X$ such that $R(x,x)$, then the type $X$ is nonempty.
background
The Meta-Principle asserts that recognition requires a substrate: nothing cannot recognize itself. This module treats the principle as a derived theorem rather than an axiom, with the implication that an existential self-recognizing pair forces the carrier type to be inhabited. The local setting begins the chain MP → Ledger → φ → constants in RRF units.
proof idea
The proof is a one-line wrapper that applies the MetaPrinciple theorem to the hypothesis h.
why it matters
This result supplies the constructive half of the Meta-Principle, directly supporting the module claim that the principle is a theorem. It precedes the ledger construction and self-similarity forcing of phi in sibling declarations, consistent with the T0–T8 forcing chain and the Recognition Composition Law. No open scaffolding remains at this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.