nontrivial_recognition_forces_interface
plain-language theorem explainer
If a carrier admits a non-trivial distinction, a finite interface exists that separates the distinguished pair. A physicist would cite this when tracing observer-like structure back to the first recognition event rather than to any measurement postulate. The proof is a direct term construction that instantiates the canonical two-outcome point interface on the given pair and applies the separation lemma for that interface.
Claim. Let $K$ be a carrier. If $K$ admits nontrivial recognition (there exist $x,y$ with equalityDistinction $K$ $x$ $y$), then there exists a primitive interface $I$ on $K$ (a map $K$ to Fin $n$ for some $n>0$) together with $x,y$ such that $I$ separates $x$ and $y$ (i.e., the observed values differ).
background
In this module a carrier $K$ carries primitive distinctions. NontrivialRecognition $K$ is the proposition that at least one pair $x,y$ satisfies equalityDistinction $K$ $x$ $y$, the minimal notion of distinguishability at the foundation. A PrimitiveInterface on $K$ is a structure with positive integer $n$ and an observe map $K$ to Fin $n$; it encodes a finite-resolution recognizer. Separates $I$ $x$ $y$ holds precisely when the observed values differ.
proof idea
The proof is a one-line term wrapper. It performs case analysis on the witness pair supplied by NontrivialRecognition, then returns the tuple consisting of the pointInterface constructed on the first element, the pair itself, the original distinction, and the result of pointInterface_separates applied to that pair.
why it matters
This supplies the pre-physical observer theorem: once any distinction exists, a finite interface is forced and functions as the primitive observer. It is invoked directly by nontrivial_recognition_forces_observer (which renames the interface an observer) and by nontrivial_recognition_forces_lattice (which builds a recognition lattice from the interface). The step sits at the base of the forcing chain, before the phi-ladder, the eight-tick octave, or the derivation of $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Geometry rebuilt as a quotient of what measurements can distinguish
"A finite local resolution axiom formalizes the fact that any observer can distinguish only finitely many outcomes within a local region."