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)
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 -/
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (10)
Lean names referenced from this declaration's body.
-
tick
in IndisputableMonolith.Constants
decl_use
-
tick
in IndisputableMonolith.Constants.RSNativeUnits
decl_use
-
has
in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
decl_use
-
neighborhood
in IndisputableMonolith.Foundation.RecognitionLatticeFromRecognizer
decl_use
-
E
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
RSConfigSpace
in IndisputableMonolith.RecogGeom.RSBridge
decl_use
-
RSLocalityFromRHat
in IndisputableMonolith.RecogGeom.RSBridge
decl_use
-
RSMeasurement
in IndisputableMonolith.RecogGeom.RSBridge
decl_use
-
L
in IndisputableMonolith.Recognition
decl_use
-
L
in IndisputableMonolith.Recognition.Cycle3
decl_use