pith. machine review for the scientific record. sign in
lemma proved term proof

constructive_at_zero

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 194lemma constructive_at_zero (path1 path2 : List Config)
 195    (_ : path1 ≠ []) (_ : path2 ≠ []) :
 196    constructive_interference path1 path2 := by

proof body

Term-mode proof.

 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⁺) -/

depends on (29)

Lean names referenced from this declaration's body.