MP
plain-language theorem explainer
MP defines the proposition that Nothing cannot recognize itself. Researchers building derivations from recognition axioms cite this as the base constraint T1 that blocks self-referential collapse at the empty type. The definition is a direct negation of an existential claim over the Recognize structure instantiated at Empty, serving as the entry point for the forcing chain.
Claim. Let $Nothing$ denote the empty type and let $Recognize(A,B)$ be the structure with fields recognizer of type $A$ and recognized of type $B$. Then MP is the proposition $¬∃ r : Recognize(Nothing, Nothing), ⊤$.
background
The Recognition module defines Nothing as the empty type Empty and Recognize as the minimal structure pairing a recognizer with a recognized object. This establishes the local setting for T1: Nothing cannot recognize itself. The definition prevents any recognition relation from holding when both arguments are empty, blocking foundational self-reference.
proof idea
The declaration is a one-line definition that directly encodes the negated existential over Recognize Nothing Nothing. No lemmas or tactics are applied; it is a direct construction of the Prop.
why it matters
MP anchors T1 in the Recognition Science framework and feeds theorems including unity_is_unique_existent, prelogical_boolean_fragment, and ml_derivation_complete. It supplies the initial constraint for the T0-T8 forcing chain and the J-cost minimization that yields phi and D=3. Downstream results in Astrophysics and Foundation modules rely on it to derive mass-to-light ratios and Boolean fragments from non-trivial recognition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.