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

PrimitiveInterface

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.ObserverFromRecognition on GitHub at line 38.

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

  35The codomain is `Fin n`, so the interface has finite resolution. This is the
  36pre-physical form of an observer: not a mind, but the map through which
  37configurations become distinguishable events. -/
  38structure PrimitiveInterface (K : Type*) where
  39  n : ℕ
  40  hpos : 0 < n
  41  observe : K → Fin n
  42
  43/-- The kernel of an interface: two configurations are indistinguishable
  44relative to the interface iff they produce the same observed outcome. -/
  45def PrimitiveInterface.kernel {K : Type*} (I : PrimitiveInterface K)
  46    (x y : K) : Prop :=
  47  I.observe x = I.observe y
  48
  49/-- A primitive observer is exactly a primitive interface. This is a naming
  50choice, but it is important: the observer is not external to recognition; it is
  51the interface structure recognition forces. -/
  52abbrev PrimitiveObserver (K : Type*) := PrimitiveInterface K
  53
  54/-- The observer kernel is reflexive. -/
  55theorem kernel_refl {K : Type*} (I : PrimitiveInterface K) (x : K) :
  56    I.kernel x x := rfl
  57
  58/-- The observer kernel is symmetric. -/
  59theorem kernel_symm {K : Type*} (I : PrimitiveInterface K) {x y : K}
  60    (h : I.kernel x y) : I.kernel y x := h.symm
  61
  62/-- The observer kernel is transitive. -/
  63theorem kernel_trans {K : Type*} (I : PrimitiveInterface K) {x y z : K}
  64    (hxy : I.kernel x y) (hyz : I.kernel y z) : I.kernel x z :=
  65  hxy.trans hyz
  66
  67/-- Every primitive interface partitions its carrier into observational
  68equivalence classes. -/

papers checked against this theorem (showing 1 of 1)