classical_observation_needs_recognition
plain-language theorem explainer
Any classical phase space with a non-constant position coordinate forces a nonempty recognition structure between some observer and observed types. Cite this when claiming that classical measurement already presupposes recognition, not only quantum or RS-native settings. The proof packages position as an Observable and applies the main observables-require-recognition theorem in one step.
Claim. Let $P$ be any type and let $\mathrm{position},\,\mathrm{momentum}:P\to\mathbb{R}$. If there exist $p_1,p_2\in P$ with $\mathrm{position}(p_1)\neq\mathrm{position}(p_2)$, then there exist types $O$ and $X$ such that the type of recognition events from $O$ to $X$ is nonempty.
background
The Recognition Necessity module shows that any framework extracting observables must carry a recognition structure: the ability to distinguish and identify states. Its three-step strategy is: (1) an observable is a measurable quantity, so distinct values mean distinguishable states; (2) distinction requires a comparison mechanism; (3) comparison without an external reference is self-recognition. The Meta Principle then rules out empty recognition, forcing nontrivial structure.
An Observable on a state space is a real-valued map (here, the classical position coordinate). Recognition.Recognize Observer Observed is the type of recognition events linking an observer type to an observed type. Upstream, Observer structures appear both as finite-resolution coarse-grainers and as coherent recognition with a persistent reference event; this theorem only needs the existence form used by the main necessity result.
The local claim specializes that machinery to classical mechanics: phase space with position and momentum as real coordinates, under the sole hypothesis that position is not constant.
proof idea
Term-mode, essentially a one-line wrapper. Build an Observable on PhaseSpace whose value map is the given position function. Feed that Observable and the hypothesis that position takes two distinct values into observables_require_recognition, which already combines distinction-from-values, comparison-as-recognition, and the Meta Principle ban on empty recognition. Momentum is unused; it is present only to match the classical phase-space signature.
why it matters
Closes the classical side of the necessity story: recognition is not an exotic quantum or RS-only demand. Even textbook classical observation (non-constant position on phase space) already forces a nonempty Recognize structure. The module lists observables_require_recognition as the main combined theorem; this declaration is the classical packaging of that result.
In the broader Verification/Exclusivity arc it supports the claim that frameworks deriving observables cannot avoid recognition structure, aligning with the Recognition Composition Law and the forcing chain's insistence on recognition as primitive. No downstream consumers are wired yet (used_by is empty), so it currently stands as a terminal citation point for classical necessity rather than an intermediate lemma. It does not touch T5–T8 constants or the mass ladder; its role is structural exclusivity, not numerics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.