pointInterface
plain-language theorem explainer
The pointInterface supplies the minimal two-outcome recognizer on any carrier K that maps a chosen reference point x₀ to outcome 1 in Fin 2 while sending every other element to 0. Researchers working on the pre-physical observer structure cite it as the canonical finite interface induced by a single named distinction. The definition is given by direct construction of the observe map together with a norm_num check that n exceeds zero.
Claim. Let $K$ be a type and $x_0$ an element of $K$. The point interface is the primitive interface $I$ on $K$ with $n=2$, $0<n$, and observation map sending $x_0$ to $1$ and every other element to $0$ in Fin 2.
background
A primitive interface on a carrier $K$ is a finite-valued recognizer consisting of a positive integer $n$ and a map $K$ to Fin $n$. This encodes the minimal structure through which a distinction becomes an event, as stated in the module on observers from recognition. The module shows that any non-trivial recognition forces existence of such an interface; the pointInterface supplies the explicit $n=2$ case for one reference point.
proof idea
The definition sets $n$ to 2 and defines the observe function by a conditional that returns 1 precisely when the input equals the reference point. Positivity of $n$ is discharged by norm_num. This is a direct structural definition with no external lemmas applied beyond the interface constructor.
why it matters
This definition provides the concrete witness used in nontrivial_recognition_forces_interface, the theorem that non-trivial recognition forces a primitive observer. It is invoked by pointInterface_at_ref, pointInterface_away, pointInterface_separates, pointLattice, and Recognizer. In the Recognition Science chain it realizes the base finite interface that later upgrades to lattices and logic, aligning with the step from distinctions to the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.