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

RSLocalityFromRHat

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  77structure RSLocalityFromRHat (L : Type*) [RSConfigSpace L] where
  78  /-- The R̂ operator: recognition events -/
  79  RHat : L → Set L
  80  /-- Self is always reachable (identity recognition) -/
  81  self_in_RHat : ∀ ℓ, ℓ ∈ RHat ℓ
  82  /-- R̂ neighborhoods have a refinement property -/
  83  refinement : ∀ ℓ ℓ', ℓ' ∈ RHat ℓ → ∃ U ⊆ RHat ℓ, ℓ' ∈ U ∧ U ⊆ RHat ℓ'
  84  /-- Recognition transitivity: when ℓ' is reachable from ℓ, then anything reachable
  85      from ℓ' is also reachable from ℓ. This is the RS analog of neighborhood containment. -/
  86  transitivity : ∀ ℓ ℓ' : L, ℓ' ∈ RHat ℓ → RHat ℓ' ⊆ RHat ℓ
  87
  88/-- Convert RS locality to RecogGeom locality.
  89
  90    Note: Full implementation requires showing R̂ neighborhoods satisfy
  91    the refinement property. This structural version shows the pattern. -/

used by (5)

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

depends on (20)

Lean names referenced from this declaration's body.