EightTickFiniteResolution

formal source

 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) :
 152    HasFiniteResolution (toLocalConfigSpace rs) (toRecognizer m) := by
 153  intro ℓ
 154  use rs.RHat ℓ
 155  constructor
 156  · exact ⟨1, rfl, trivial⟩
 157  · exact h8.finite_local_events ℓ
 158
 159/-! ## Master Bridge Statement -/
 160
 161/-- **Master theorem (RG4)**: RS's 8-tick finite-resolution hypothesis yields Recognition Geometry's
 162finite-resolution axiom (RG4) for the induced locality and recognizer. -/
 163theorem RS_instantiates_RG {L E : Type*} [RSConfigSpace L]
 164    (rs : RSLocalityFromRHat L) (m : RSMeasurement L E)
 165    (h8 : EightTickFiniteResolution L E rs m) :
 166    HasFiniteResolution (toLocalConfigSpace rs) (toRecognizer m) :=
 167  eight_tick_implies_RG4 rs m h8
 168
 169/-! ## Physical Space as Recognition Quotient -/
 170
 171/-- **Key construction**: for a measurement recognizer, the observable space is the recognition
 172quotient, and it is canonically isomorphic to the *image* of the measurement.
 173