mp_holds
plain-language theorem explainer
The theorem asserts that the metaphysical primitive MP holds inside the RRF namespace. Researchers deriving physics from recognition relations would cite the re-export when they need the base Recognition module available under the RRF prefix. The proof is a direct term-level alias of the original theorem proved by case analysis on the empty recognizer.
Claim. The metaphysical primitive holds: it is impossible for the empty type to recognize itself, i.e., $¬∃ r : Recognize(∅,∅), ⊤$.
background
The module re-exports core Recognition definitions to bridge the existing Recognition module with the RRF framework. MP is defined as the proposition that nothing cannot recognize itself, where Nothing is the empty type and Recognize is the minimal recognizer-recognized pairing. The upstream definition states MP : Prop := ¬ ∃ _ : Recognize Nothing Nothing, True.
proof idea
One-line term wrapper that applies the upstream theorem Recognition.mp_holds from IndisputableMonolith.Recognition.
why it matters
The re-export places MP inside RRF.Core.Recognition so that downstream results such as nothing_cannot_recognize_itself can reference the manuscript phrasing 'Nonexistence cannot recognize itself.' MP anchors the Recognition Science chain at the starting point before J-uniqueness and the phi-ladder are introduced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.