def
definition
modally_equivalent
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Modal.ModalGeometry on GitHub at line 142.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
139def modal_nyquist_limit : ℕ := modal_period / 2
140
141/-- Two configs are **modally equivalent** if they differ by less than one tick. -/
142def modally_equivalent (c1 c2 : Config) : Prop :=
143 c1.value = c2.value ∧ (c1.time : ℤ) - (c2.time : ℤ) < 1 ∧ (c2.time : ℤ) - (c1.time : ℤ) < 1
144
145/-- Modal equivalence is reflexive. -/
146lemma modally_equivalent_refl (c : Config) : modally_equivalent c c := by
147 simp [modally_equivalent]
148
149/-- Modal equivalence is symmetric. -/
150lemma modally_equivalent_symm (c1 c2 : Config) :
151 modally_equivalent c1 c2 ↔ modally_equivalent c2 c1 := by
152 simp [modally_equivalent]
153 constructor <;> (intro ⟨h1, h2, h3⟩; exact ⟨h1.symm, h3, h2⟩)
154
155/-- **MODAL NYQUIST THEOREM**: The universe cannot distinguish possibilities
156 finer than one tick.
157
158 This is the modal analog of:
159 - Nyquist sampling (time)
160 - Heisenberg uncertainty (phase space)
161 - Gap-45 consciousness threshold (qualia)
162
163 The 8-tick structure forces this limit. -/
164theorem modal_nyquist (c1 c2 : Config)
165 (h_val : c1.value = c2.value)
166 (h_time : c1.time = c2.time) :
167 modally_equivalent c1 c2 := by
168 simp [modally_equivalent, h_val, h_time]
169
170/-! ## Possibility Interference -/
171
172/-- **INTERFERENCE AMPLITUDE**: The overlap between two possibility paths.