MetaPrinciple
plain-language theorem explainer
MetaPrinciple states that the existence of a binary relation R on type X together with a self-recognizing element x forces X to be nonempty. Researchers deriving the ledger and phi from recognition cite it as the initial constructive step. The proof extracts the witness x directly from the existential hypothesis in a single term.
Claim. If there exists a binary 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 module presents the claim that recognition requires a substrate. Its module documentation states: 'Nothing cannot recognize itself.' Formally this means empty recognition is impossible, so the existence of a self-recognizing element entails that the type cannot be empty. The module treats the statement as a theorem rather than an axiom and positions it as the root of the derivation: MP yields the ledger by double-entry necessity, the ledger yields phi by self-similar closure, and phi yields the constants.
proof idea
The proof is a one-line term-mode wrapper. It introduces the existential hypothesis and returns the Nonempty constructor applied to the witness x extracted from the pair (R, x).
why it matters
This theorem is the direct parent of recognition_implies_existence and recognition_structure_nonempty. It supplies the base step of the chain MP → Ledger → phi described in the module documentation. The result anchors the Recognition Science framework before the forcing chain T0-T8 and the Recognition Composition Law are invoked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.