kernel_trans
plain-language theorem explainer
Transitivity of the kernel relation on a primitive interface follows from equality transitivity on its finite observed values. Researchers formalizing the primitive observer in Recognition Science cite this to complete the equivalence relation axioms before partitioning carriers into observational classes. The proof is a direct one-line term applying equality transitivity to the observe map outputs.
Claim. Let $I$ be a primitive interface on carrier $K$, consisting of a positive integer $n$ and a map observe$: K to Fin n$. The kernel relation is defined by $x sim_I y$ iff observe$(x)=$observe$(y)$. Then $x sim_I y$ and $y sim_I z$ imply $x sim_I z$.
background
PrimitiveInterface equips a carrier type $K$ with a positive integer $n$ and an observation map to the finite set Fin n; this is the pre-physical form of an observer as a finite-resolution recognizer. The kernel is the induced indistinguishability relation: two elements are related precisely when they produce the same observed outcome under this map. The module proves that non-trivial recognition forces such an interface, supplying the minimal structure through which distinctions become events.
proof idea
The proof is a one-line term that applies the transitivity of equality to the two hypotheses. Each hypothesis states equality of the observe images, so their composition yields equality of the outer pair under the same map.
why it matters
This supplies the transitivity axiom for kernel_is_equivalence, which asserts that the kernel forms an Equivalence and therefore partitions the carrier into observational classes. It closes the foundational step from recognition to a primitive observer interface before the upgrade to ledger configurations in ObserverFormalization. The result sits inside the chain that derives an interface from non-trivial distinction and precedes any physical scaling of equivalence classes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.