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

interfaceSetoid

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.RecognitionLatticeFromRecognizer on GitHub at line 48.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  45
  46/-- The setoid induced by a primitive interface. Two configurations are
  47equivalent iff the interface sends them to the same event. -/
  48def interfaceSetoid {K : Type*} (I : PrimitiveInterface K) : Setoid K where
  49  r := I.kernel
  50  iseqv := kernel_is_equivalence I
  51
  52/-- The **recognition lattice** generated by an interface: the quotient by
  53the interface kernel. -/
  54def RecognitionLattice {K : Type*} (I : PrimitiveInterface K) : Type _ :=
  55  Quotient (interfaceSetoid I)
  56
  57/-- The lattice cell containing a configuration. -/
  58def cellOf {K : Type*} (I : PrimitiveInterface K) (x : K) :
  59    RecognitionLattice I :=
  60  Quotient.mk (interfaceSetoid I) x
  61
  62/-- Two configurations determine the same cell iff the recognizer cannot
  63distinguish them. -/
  64theorem cell_eq_iff_kernel {K : Type*} (I : PrimitiveInterface K) (x y : K) :
  65    cellOf I x = cellOf I y ↔ I.kernel x y := by
  66  exact Quotient.eq
  67
  68/-! ## Finite-resolution labels and neighborhoods -/
  69
  70/-- The finite event label of a recognition cell. This is well-defined because
  71the quotient identifies exactly configurations with equal observed labels. -/
  72def cellLabel {K : Type*} (I : PrimitiveInterface K) :
  73    RecognitionLattice I → Fin I.n :=
  74  Quotient.lift (fun x => I.observe x) (by
  75    intro x y h
  76    exact h)
  77
  78@[simp] theorem cellLabel_cellOf {K : Type*} (I : PrimitiveInterface K) (x : K) :

papers checked against this theorem (showing 1 of 1)