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

toRecognizer

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)

 128def toRecognizer {L E : Type*} [RSConfigSpace L]
 129    (m : RSMeasurement L E) : Recognizer L E where
 130  R := m.measure

proof body

Definition body.

 131  nontrivial := m.nontrivial
 132
 133/-! ## 8-Tick Finite Resolution -/
 134
 135/-- **Structural Definition**: The 8-tick cycle provides finite resolution.
 136
 137    In RS, any local region can only support finitely many distinguishable
 138    states within one 8-tick cycle. This is the fundamental discreteness
 139    of recognition physics.
 140
 141    Mathematically: For any ℓ and any R̂-neighborhood U of ℓ,
 142    the set m(U) of measurement outcomes is finite. -/

used by (3)

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

depends on (32)

Lean names referenced from this declaration's body.

… and 2 more