pith. machine review for the scientific record. sign in
structure definition def or abbrev high

RecognitionPreservingMap

show as:
view Lean formalization →

Recognition-preserving maps are transformations of configurations that leave the recognizer's event predicate invariant. They form the basic symmetry objects in recognition geometry and are used to build the induced action on the recognition quotient. The declaration introduces this concept directly as a structure consisting of a function and its preservation property.

claimLet $r$ be a recognizer on configuration space $C$. A recognition-preserving map is a function $f : C → C$ such that the recognizer's event predicate satisfies $r.R(f(c)) = r.R(c)$ for all $c ∈ C$.

background

Recognition geometry equips a recognizer with a configuration space $C$ and an event predicate $R$. A symmetry is any transformation of $C$ that leaves $R$ unchanged, thereby inducing a well-defined map on the quotient space of indistinguishable configurations. The module develops the algebraic properties of these maps, including composition and identity, which mirror the structure of symmetry groups in physics.

proof idea

The declaration is a structure definition. It packages the function field toFun with the predicate preserves_event that asserts invariance of the recognition predicate under the map. No further lemmas or tactics are required for the definition.

why it matters in Recognition Science

This definition anchors the symmetry theory in the module and is referenced by the composition operation, the identity map, and the quotient action theorems. It directly implements the physical interpretation of gauge symmetries as recognition-preserving transformations. Within the Recognition Science framework it supplies the geometric layer needed to quotient out unobservable degrees of freedom before applying the forcing chain from T0 to T8.

scope and limits

formal statement (Lean)

  44structure RecognitionPreservingMap (r : Recognizer C E) where
  45  /-- The underlying transformation -/
  46  toFun : C → C
  47  /-- The transformation preserves recognition events -/
  48  preserves_event : ∀ c, r.R (toFun c) = r.R c
  49
  50/-- Coercion to function -/
  51instance (r : Recognizer C E) : CoeFun (RecognitionPreservingMap r) (fun _ => C → C) where
  52  coe := RecognitionPreservingMap.toFun

proof body

Definition body.

  53
  54/-! ## Basic Properties -/
  55
  56variable {r : Recognizer C E}
  57
  58/-- A recognition-preserving map preserves indistinguishability -/

used by (14)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (5)

Lean names referenced from this declaration's body.