pointInterface
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not claim uniqueness among all possible interfaces on K.
- Does not extend to carriers lacking decidable equality.
- Does not incorporate physical constants or the phi-ladder.
- Does not handle multiple simultaneous reference points.
formal statement (Lean)
91noncomputable def pointInterface {K : Type*} (x₀ : K) :
92 PrimitiveInterface K where
93 n := 2
proof body
Definition body.
94 hpos := by norm_num
95 observe := fun x =>
96 if x = x₀ then (1 : Fin 2) else (0 : Fin 2)
97
98/-- The point interface recognizes its reference point as outcome `1`. -/