def
definition
constructive_interference
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 184.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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)
195 (_ : path1 ≠ []) (_ : path2 ≠ []) :
196 constructive_interference path1 path2 := by
197 use 0
198 simp only [interference_amplitude, Real.cos_zero, mul_one]
199 apply mul_pos
200 · apply Real.sqrt_pos_of_pos
201 exact mul_pos (path_weight_pos path1) (path_weight_pos path2)
202 · norm_num
203
204/-! ## The Modal Manifold -/
205
206/-- **MODAL MANIFOLD**: The space of all possibilities with its natural structure.
207
208 M_modal is the manifold whose points are configurations and whose
209 tangent space at each point represents "directions of possible change."
210
211 Key properties:
212 - Dimension = 1 (value) + 1 (time) = 2
213 - Metric = modal_distance
214 - Curvature = possibility_curvature