RSMeasurement

formal source

 118    - Two states with the same measurement outcome are indistinguishable
 119
 120    The 8-tick cadence ensures measurements have finite local resolution. -/
 121structure RSMeasurement (L E : Type*) [RSConfigSpace L] where
 122  /-- The measurement function -/
 123  measure : L → E
 124  /-- Measurements are nontrivial (can distinguish at least two states) -/
 125  nontrivial : ∃ ℓ₁ ℓ₂ : L, measure ℓ₁ ≠ measure ℓ₂
 126
 127/-- Convert RS measurement to RecogGeom recognizer -/
 128def toRecognizer {L E : Type*} [RSConfigSpace L]
 129    (m : RSMeasurement L E) : Recognizer L E where
 130  R := m.measure
 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. -/
 143structure EightTickFiniteResolution (L E : Type*) [RSConfigSpace L]
 144    (rs : RSLocalityFromRHat L) (m : RSMeasurement L E) : Prop where
 145  /-- Every R̂ neighborhood has finitely many distinguishable outcomes -/
 146  finite_local_events : ∀ ℓ, (m.measure '' rs.RHat ℓ).Finite
 147
 148/-- 8-tick finite resolution implies RG4 -/
 149theorem eight_tick_implies_RG4 {L E : Type*} [RSConfigSpace L]
 150    (rs : RSLocalityFromRHat L) (m : RSMeasurement L E)
 151    (h8 : EightTickFiniteResolution L E rs m) :