eight_tick_implies_RG4

formal source

 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
 174This is the precise Lean analogue of the paper statement “observable space \(\cong \mathrm{Im}(R)\)”. -/
 175noncomputable def physical_space_is_quotient {L E : Type*} [RSConfigSpace L]
 176    (m : RSMeasurement L E) :
 177    RecognitionQuotient (toRecognizer m) ≃ Set.range m.measure := by
 178  -- Specialize the generic quotient≃image theorem to the recognizer induced by `m`.
 179  simpa [toRecognizer] using (quotient_equiv_image (r := toRecognizer m))