kernel_is_equivalence
plain-language theorem explainer
The kernel relation of any primitive interface on a carrier is an equivalence relation. Workers building recognition lattices or observer certificates cite it to guarantee that observational indistinguishability yields a well-defined quotient. The proof is a one-line term-mode wrapper that assembles the three kernel lemmas into the Equivalence structure.
Claim. Let $I$ be a primitive interface on carrier $K$, consisting of a positive integer $n$ and an observation map $I.observe : K → Fin n$. The relation $x ∼ y$ defined by $I.observe(x) = I.observe(y)$ is an equivalence relation on $K$.
background
The module proves that non-trivial recognition forces a primitive interface, the minimal structure through which distinctions become events. A PrimitiveInterface on $K$ is a structure with positive $n : ℕ$ and observe : $K → Fin n$, supplying finite resolution; its kernel is the relation observe(x) = observe(y). The local setting is the pre-physical floor before ObserverFormalization upgrades the interface to ledger configurations.
proof idea
The proof is a term-mode construction that directly supplies the Equivalence record: reflexivity from kernel_refl I, symmetry from kernel_symm I, and transitivity from kernel_trans I. No tactics are used; the three sibling lemmas are packaged into the required fields.
why it matters
This result supplies the iseqv field for interfaceSetoid and the kernel_equiv component of observerFromRecognitionCert and recognitionLatticeCert. It realizes the partition into observational classes required by the Recognizer structure, advancing the chain from distinctions to the primitive observer and the induced logic. The declaration closes the equivalence step in the foundation module without invoking the phi-ladder or physical constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.