MP_essential_for_physics
plain-language theorem explainer
Any state space with a non-constant observable forces a genuine recognition structure: inhabited Recognize(R₁,R₂) with at least one side non-empty. Verification and exclusivity arguments cite this to show the Meta Principle is not optional for non-trivial physics. The proof obtains recognition from the necessity lemma, then rules out double-Empty by the MP non-emptiness fact.
Claim. Let $S$ be a type of states. Suppose there exists an observable $o:S\to\mathbb{R}$ and states $s_1,s_2$ with $o(s_1)\neq o(s_2)$. Then there exist types $R_1,R_2$ such that $\mathrm{Recognize}(R_1,R_2)$ is inhabited and $R_1\neq\emptyset$ or $R_2\neq\emptyset$.
background
This module (Recognition Structure Necessity) shows that any framework extracting observables must carry a recognition structure: the ability to distinguish and identify states without an external referee. The strategy is three-step: observables imply distinguishable states; distinction requires comparison; comparison without external reference is self-recognition. The Meta Principle (MP) then forbids the trivial empty case.
An Observable on a state space $S$ is simply a map $S\to\mathbb{R}$ (a measurable extracted quantity). Non-constant observables therefore supply two states with unequal real values. Recognition is the primitive two-sided relation Recognize R₁ R₂ from the Recognition import: a structured act of identifying one side against the other.
Upstream in the same module, RS_recognition_is_necessary already converts a non-constant observable into inhabited recognition types, and recognition_must_be_nonempty (via MP) asserts that both carrier types of an inhabited recognition are nonempty. This theorem packages those facts into the physics-facing claim that MP is essential once observables exist.
proof idea
Tactic proof, short chain. From the hypothesis of a non-constant observable, apply RS_recognition_is_necessary to obtain types $R_1,R_2$ and a witness that Recognize R₁ R₂ is inhabited. Exhibit those types in the existential.
The first conjunct is that witness. For the second, apply recognition_must_be_nonempty to get Nonempty R₁ and Nonempty R₂. Argue by contradiction: if both $R_1=\mathsf{Empty}$ and $R_2=\mathsf{Empty}$, substitute $R_1=\mathsf{Empty}$ into Nonempty R₁ and discharge with not_nonempty_empty. (Only one side needs to be hit; the disjunction follows.)
why it matters
Closes the module's MP step: once observables exist, recognition cannot be the empty/trivial structure. The module doc states the Meta Principle "forbids trivial empty recognition, forcing non-trivial structure," with no axioms beyond MP. That is exactly the content here.
In the broader Recognition Science forcing picture, non-trivial recognition is the entry point to the T0–T8 chain (J-uniqueness, $\varphi$ as self-similar fixed point, eight-tick octave, $D=3$). Without this lemma, a skeptic could grant observables yet keep recognition vacuous. There are no recorded downstream uses yet; the result stands as a terminal verification fact in Verification.Necessity, available to exclusivity and framework-comparison arguments that need "physics implies MP-grade recognition."
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.