def
definition
toRecognizer
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.RecogGeom.RSBridge on GitHub at line 128.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
nontrivial -
of -
tick -
tick -
U -
of -
one -
is -
of -
one -
neighborhood -
is -
E -
of -
Tick -
is -
of -
Tick -
Tick -
Resolution -
is -
Tick -
and -
Resolution -
one -
Resolution -
RSConfigSpace -
RSMeasurement -
L -
U -
L -
one
used by
formal source
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) :
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