`constructive_at_zero`

proved

show as: view math explainer →

module: IndisputableMonolith.Modal.ModalGeometry
domain: Modal
line: 194 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Modal.ModalGeometry on GitHub at line 194.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.