kernel_refl
plain-language theorem explainer
The kernel relation induced by any primitive interface on a carrier is reflexive. Recognition Science foundations cite this to begin constructing the equivalence relation that partitions configurations into observational classes. The proof is a direct one-line application of reflexivity to the definition of the kernel as equality of observations.
Claim. Let $I$ be a primitive interface on carrier $K$, consisting of a positive integer $n$ and observation map $observe_I : K → Fin n$. Then for every $x ∈ K$, $observe_I(x) = observe_I(x)$.
background
The module ObserverFromRecognition shows that non-trivial recognition forces a primitive interface, which is the pre-physical form of an observer. A PrimitiveInterface on $K$ comprises a positive natural number $n$ and a map $observe : K → Fin n$ of finite resolution; two configurations are indistinguishable under the interface precisely when they produce the same observed value in Fin n. The kernel predicate is therefore defined by equality of these observed values.
proof idea
The proof is a one-line term that applies reflexivity (rfl) directly to the equality $I.observe x = I.observe x$ arising from the kernel definition.
why it matters
This supplies the reflexive leg of the equivalence relation proved in the downstream theorem kernel_is_equivalence, which states that every primitive interface partitions its carrier into observational equivalence classes. The result sits inside the module's derivation of a minimal interface from non-trivial distinction and supplies the pre-physical floor before later upgrades to ledger-based recognizers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.