pith. machine review for the scientific record. sign in
def

interfaceSetoid

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

plain-language theorem explainer

interfaceSetoid defines the setoid on carrier K whose relation is the kernel of a given primitive interface I. Recognition-geometry constructions cite it to form the quotient lattice of configurations that produce identical events. The definition is a direct wrapper that installs the kernel as the relation and supplies the equivalence proof kernel_is_equivalence.

Claim. Let $I$ be a primitive interface on carrier $K$, consisting of a positive integer $n$ and an observation map $K$ to Fin $n$. The induced setoid on $K$ declares $x$ equivalent to $y$ precisely when the observation map sends both to the same element of Fin $n$.

background

PrimitiveInterface packages a finite-resolution recognizer: a positive natural $n$ together with a map from configurations in $K$ to the event set Fin $n$. Its kernel is the equivalence relation on $K$ that identifies two configurations exactly when they yield the same event. The module turns the structural claim of Recognition Geometry into a Lean theorem by forming the quotient of $K$ by this kernel, producing the recognition lattice whose cells are the observational equivalence classes. Upstream, the theorem kernel_is_equivalence establishes that the kernel is reflexive, symmetric and transitive for any such interface.

proof idea

This is a one-line wrapper definition. It constructs the Setoid record by setting the relation field to the kernel of $I$ and the iseqv field to the theorem kernel_is_equivalence applied to $I$.

why it matters

The definition supplies the equivalence relation required by the Quotient constructor that yields RecognitionLattice and by the map cellOf that sends each configuration to its cell. In the Recognition Science framework it realizes the initial recognition lattice: the quotient of configurations by the indistinguishability kernel of any primitive interface. The module documentation records that the lattice remains pre-spatial, inherits finite resolution from Fin $n$, and that the interpretation of LogicNat into the lattice is not necessarily injective when the lattice is finite.

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

papers checked against this theorem (showing 1 of 1)