kernel_symm
plain-language theorem explainer
kernel_symm establishes symmetry of the kernel relation induced by any primitive interface on a carrier. Researchers constructing equivalence classes from finite-resolution recognizers in the Recognition Science foundation would cite this step. The proof is a direct one-line term that applies equality symmetry to the observed Fin n values.
Claim. Let $I$ be a primitive interface on carrier $K$. If $I$ maps $x,y$ to the same value in its finite codomain, then it maps $y,x$ to the same value.
background
The module derives a primitive observer from non-trivial recognition. A PrimitiveInterface consists of a positive integer $n$ together with an observation map $K$ to Fin $n$; its kernel declares two carriers indistinguishable exactly when they receive identical observations. This supplies the pre-physical floor before later modules upgrade the structure to ledger configurations.
proof idea
The proof is a one-line term wrapper that applies the built-in symmetry of equality to the observed values in Fin $n$. No external lemmas are invoked.
why it matters
The result supplies the symmetry leg for kernel_is_equivalence, which assembles the full equivalence relation that partitions the carrier into observational classes. It completes one of the three required properties in the chain from recognition to a primitive interface, consistent with the forcing steps that generate structure from distinctions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.