pith. sign in
def

SameKernel

definition
show as:
module
IndisputableMonolith.Foundation.RecognitionLatticeFromRecognizer
domain
Foundation
line
116 · github
papers citing
1 paper (below)

plain-language theorem explainer

SameKernel declares the predicate under which two primitive interfaces on a carrier K induce identical indistinguishability relations. Lattice constructions in the Recognition framework cite it to obtain canonical equivalence of quotients. The definition is the direct pointwise biconditional on the kernel predicates of the two interfaces.

Claim. Let $I$ and $J$ be primitive interfaces on a carrier set $K$. Then $I$ and $J$ have the same kernel when, for all configurations $x,y$ in $K$, the observer map of $I$ sends $x$ and $y$ to the same label if and only if the observer map of $J$ does.

background

A primitive interface on carrier $K$ consists of a positive integer resolution $n$ and an observation function $K$ to Fin $n$. Its kernel is the binary relation on $K$ holding exactly when two configurations map to the same event label and are therefore indistinguishable to the interface. The module RecognitionLatticeFromRecognizer defines the recognition lattice as the quotient of $K$ by this kernel. SameKernel identifies interfaces that produce identical quotients. This rests on the definition of PrimitiveInterface and its kernel predicate supplied in ObserverFromRecognition.

proof idea

The declaration is a direct definition. It equates the two kernel relations by requiring the biconditional to hold for all pairs $x,y$. No external lemmas are invoked; the body simply unfolds the definition of the kernel inside each interface.

why it matters

SameKernel supplies the hypothesis for latticeEquivOfSameKernel, which constructs the canonical equivalence between the two recognition lattices. It thereby completes the uniqueness statement for the pre-spatial lattice in the module. This step aligns with the Recognition Geometry claim that the lattice is determined solely by the distinctions made by the recognizer.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.

papers checked against this theorem (showing 1 of 1)