pointInterface
plain-language theorem explainer
pointInterface supplies the canonical two-outcome recognizer on any carrier K that flags whether an input equals a chosen reference x0. Workers on the pre-physical observer theorem cite this construction when exhibiting the finite interface forced by a single named distinction. The definition directly instantiates the PrimitiveInterface structure with n fixed at 2 and an observe map that returns 1 precisely at x0.
Claim. For any carrier set $K$ and reference element $x_0$ in $K$, the point interface is the structure with two outcomes whose observation map returns 1 on $x_0$ and 0 on every other element of $K$.
background
A primitive interface on a carrier $K$ is a finite-valued recognizer whose codomain is Fin n for some positive natural number n; the observation map turns configurations into distinguishable events of finite resolution and is the pre-physical form of an observer. The module establishes that non-trivial recognition on $K$ forces the existence of such an interface, supplying the floor before any physical measuring device appears. The upstream PrimitiveInterface structure records exactly these three fields: n, the positivity proof hpos, and the observe function.
proof idea
The definition is a direct structure instance. It sets n to 2, discharges hpos by norm_num, and defines observe by an if-then-else that returns 1 precisely when the input equals the reference x0 and 0 otherwise.
why it matters
This definition is the concrete witness used inside nontrivial_recognition_forces_interface to produce the primitive observer once a distinction exists. It is invoked again to build pointLattice and to equip the Recognizer structure. In the Recognition Science chain it realizes the first finite-resolution map that converts a named distinction into an event, prior to any upgrade in ObserverFormalization.lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.