PrimitiveInterface
plain-language theorem explainer
PrimitiveInterface defines a finite-valued recognizer on any carrier set K as a positive integer n together with an observe map into Fin n. Researchers deriving observers from recognition distinctions cite it as the minimal pre-physical structure that turns configurations into distinguishable events. The declaration is a direct structure definition with no lemmas or tactics required.
Claim. A primitive interface on a carrier set $K$ consists of a positive integer $n$ and a function observe$: K → Fin n$ that assigns each element of $K$ to one of $n$ possible outcomes.
background
The module establishes that non-trivial recognition forces an interface, which is the primitive observer. The module documentation states: 'non-trivial recognition forces an interface, and an interface is the primitive observer. The word observer here is not yet a biological observer or a physical measuring device. It is the minimal interface through which a distinction becomes an event.' This supplies the pre-physical floor later upgraded to ledger configurations in ObserverFormalization.lean. The structure supplies finite resolution via the codomain Fin n, ensuring only finitely many distinguishable outcomes from the carrier.
proof idea
The declaration is a direct structure definition. It introduces the three fields n, hpos, and observe with no lemmas applied and no tactics used.
why it matters
This structure feeds the parent theorems nontrivial_recognition_forces_interface and kernel_is_equivalence. The former shows that any non-trivial recognition admits a separating finite interface; the latter shows that the induced kernel is an equivalence relation. It realizes the module claim that observer-dependence is forced at the first distinction rather than added later. The definition aligns with the Recognition Science step in which distinctions become events through finite recognizers, prior to the eight-tick octave or spatial dimension D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Geometry rebuilt as a quotient of what measurements can distinguish
"A finite local resolution axiom formalizes the fact that any observer can distinguish only finitely many outcomes within a local region."