constructive_at_zero

formal source

 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
 215    - Boundary = J → ∞ (x → 0⁺) -/
 216structure ModalManifold where
 217  /-- Points of the manifold -/
 218  points : Set Config
 219  /-- Dimension (value + time) -/
 220  dimension : ℕ := 2
 221  /-- The metric structure -/
 222  metric : Config → Config → ℝ := modal_distance
 223  /-- The curvature function -/
 224  curvature : Config → ℝ := possibility_curvature