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) :=
proof body
Term-mode proof.
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)\)”. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.