theorem
proved
modal_nyquist
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 164.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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.
173
174 When two paths have similar cost, they can "interfere."
175 I(γ₁, γ₂) = √(W[γ₁] · W[γ₂]) · cos(Δφ)
176
177 where Δφ is the phase difference. -/
178noncomputable def interference_amplitude (path1 path2 : List Config) (phase_diff : ℝ) : ℝ :=
179 Real.sqrt (PathWeight path1 * PathWeight path2) * Real.cos phase_diff
180
181/-- **CONSTRUCTIVE INTERFERENCE**: When paths reinforce.
182
183 Occurs when phase_diff = 2πn (paths in phase). -/
184def constructive_interference (path1 path2 : List Config) : Prop :=
185 ∃ n : ℤ, interference_amplitude path1 path2 (2 * Real.pi * n) > 0
186
187/-- **DESTRUCTIVE INTERFERENCE**: When paths cancel.
188
189 Occurs when phase_diff = π(2n+1) (paths out of phase). -/
190def destructive_interference (path1 path2 : List Config) : Prop :=
191 ∃ n : ℤ, interference_amplitude path1 path2 (Real.pi * (2 * n + 1)) < 0
192
193/-- Constructive interference at phase 0. -/
194lemma constructive_at_zero (path1 path2 : List Config)