Separates
plain-language theorem explainer
Separates is the predicate that a primitive interface on carrier K distinguishes two elements x and y by assigning them different values in its finite codomain. Theorems deriving the existence of a primitive observer from any non-trivial recognition cite this predicate to record separation of a distinguished pair. The definition is the direct inequality of the two images under the observe map of the supplied interface structure.
Claim. Let $I$ be a primitive interface on a carrier $K$, consisting of a positive integer $n$ and a map $I : K → Fin n$. For $x, y ∈ K$, the proposition Separates$(I, x, y)$ holds precisely when $I(x) ≠ I(y)$.
background
The module establishes that non-trivial recognition on any carrier forces a finite interface, which functions as the primitive observer. A PrimitiveInterface is the structure supplying a positive natural number $n$ together with an observation map from the carrier to the finite set Fin $n$; this map converts configurations into distinguishable events at finite resolution and supplies the pre-physical form of an observer.
proof idea
This declaration is a one-line definition that applies the observe map of the given PrimitiveInterface to test inequality of the images of $x$ and $y$.
why it matters
Separates supplies the predicate appearing in nontrivial_recognition_forces_interface and nontrivial_recognition_forces_observer, which prove that non-trivial recognition forces a primitive observer. The module documentation positions the construction as the pre-physical floor: the interface is forced at the first distinction and supplies the event structure before any physical measurement layer. It supports the RecognizerInducesLogicCert by providing the separation condition required for the induced logic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.