mp_implies_recognition_meaningful
plain-language theorem explainer
Under the Meta-Principle, recognition between any two inhabited types is non-vacuous: a Recognize witness exists. Conservation-necessity arguments cite this as the positive half of MP (something can recognize). The proof is a pure inhabitant construction from Inhabited defaults plus reflexivity; the MP hypothesis is carried but unused in the term.
Claim. Assume the Meta-Principle ("nothing cannot recognize itself"). Then for all inhabited types $A$ and $B$ there exists a recognition structure $r$ from $A$ to $B$ (with recognizer and recognizee drawn from the inhabitants) such that the recognizer equals itself, i.e. recognition is well-formed and non-empty.
background
This module derives non-trivial conservation from the Meta-Principle alone, so that recognition_requires_distinguishability need not be an axiom. The chain is: MP makes recognition possible; recognition needs distinction; distinction in a discrete event system needs non-zero flow; hence MP forces non-trivial conservation.
The Meta-Principle is the negative claim that empty self-recognition is impossible. The present theorem extracts the dual positive claim: once types are inhabited (non-empty), a Recognize A B structure can be assembled. Downstream siblings package discrete event systems, event evolution, flow on edges, and distinguishability of flows.
Local setting is Verification/Necessity: close the conservation gap documented in the module header by replacing an axiom with a proved implication from MP.
proof idea
Term-mode, four steps. Introduce the two types and discard their Inhabited instances as anonymous. Build a Recognize A B pair by taking default for both the recognizer and the recognizee (available precisely because the types are inhabited). Close the residual equality r.recognizer = r.recognizer by rfl. The hypothesis hMP is never applied; it only records that the result sits under MP in the necessity chain.
why it matters
First bullet in the module's conservation-necessity status string: the status def lists this theorem as proven and treats it as the opening move of the core argument. Parent consumer is conservation_necessity_status, which advertises the full chain (recognition events, non-trivial systems have events, MP forces non-trivial flow) as complete without holes.
Framework role: it converts MP from a pure prohibition into an existence principle, which is exactly step 1 of the module argument ("MP implies recognition is possible"). That step is what lets later lemmas force distinguishability and non-zero flow, discharging the old LedgerNecessity axiom. No T5–T8 landmark is invoked here; the result is purely foundational bookkeeping under MP.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.