nontrivial_recognition_forces_interface
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.
claimLet $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 in Recognition Science
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$.
scope and limits
- Does not claim the interface corresponds to any physical measuring device.
- Does not constrain the resolution $n$ beyond positivity.
- Does not invoke the Recognition Composition Law or any RS constants.
- Does not extend to continuous carriers or infinite resolution.
formal statement (Lean)
129theorem nontrivial_recognition_forces_interface (K : Type*) :
130 NontrivialRecognition K →
131 ∃ (I : PrimitiveInterface K) (x y : K),
132 equalityDistinction K x y ∧ Separates I x y := by
proof body
Term-mode proof.
133 intro h
134 rcases h with ⟨x, y, hxy⟩
135 exact ⟨pointInterface x, x, y, hxy, pointInterface_separates hxy⟩
136
137/-- Same theorem under the observer name: non-trivial recognition forces a
138primitive observer. -/