lean4/AnuQuantumInterference.lean

/-
  AnuQuantumInterference
  Phase mask operations with constructive/destructive interference
-/
import Mathlib

noncomputable section

open Real

-- ============================================================
-- Core Definitions
-- ============================================================

/-- Apply a phase mask: true = constructive (keep), false = destructive (negate) -/
def apply_phase_mask (w : ℝ) (constructive : Bool) : ℝ :=
  if constructive then w else -w

/-- Phase shift values for a layer -/
def phase_shift (layer_idx : Nat) (n_layers : Nat) : ℝ :=
  2 * Real.pi * (layer_idx : ℝ) / (n_layers : ℝ)

/-- Perturbation: small noise added to weights -/
def perturb (w : ℝ) (epsilon : ℝ) : ℝ :=
  w + epsilon

/-- Pipeline: sequence of phase-masked operations -/
def pipeline (weights : List ℝ) (masks : List Bool) : List ℝ :=
  List.zipWith apply_phase_mask weights masks

-- ============================================================
-- Theorems (6)
-- ============================================================

/-- Destructive interference negates the weight -/
theorem destructive_cancellation (w : ℝ) :
    apply_phase_mask w false = -w := by
  simp [apply_phase_mask]

/-- Constructive interference preserves the weight -/
theorem constructive_preservation (w : ℝ) :
    apply_phase_mask w true = w := by
  simp [apply_phase_mask]

/-- Phase shift values are in [0, 2*pi) for valid layer indices -/
theorem phase_shift_values (layer_idx n_layers : Nat)
    (h_valid : layer_idx < n_layers)
    (h_pos : n_layers > 0) :
    0 ≤ phase_shift layer_idx n_layers ∧
    phase_shift layer_idx n_layers < 2 * Real.pi := by
  have h₁ : (layer_idx : ℝ) ≥ 0 := by exact_mod_cast Nat.zero_le layer_idx
  have h₂ : (n_layers : ℝ) > 0 := by exact_mod_cast h_pos
  have h₃ : (layer_idx : ℝ) < (n_layers : ℝ) := by exact_mod_cast h_valid
  have h₅ : (layer_idx : ℝ) / (n_layers : ℝ) < 1 := by
    rw [div_lt_one h₂]; exact_mod_cast h_valid
  constructor
  · simp [phase_shift]
    positivity
  · simp [phase_shift]
    have : (layer_idx : ℝ) / (n_layers : ℝ) < 1 := h₅
    have hpi : 0 < Real.pi := Real.pi_pos
    nlinarith

/-- Small perturbation preserves sign structure -/
theorem perturbation_preserves_structure (w epsilon : ℝ)
    (h_small : |epsilon| < |w|)
    (h_w_pos : w > 0) :
    perturb w epsilon > 0 := by
  have h₁ : |w| = w := abs_of_pos h_w_pos
  have h₂ : |epsilon| < w := by rwa [h₁] at h_small
  have h₃ : -w < epsilon := (abs_lt.mp h₂).1
  simp only [perturb]
  linarith

/-- Pipeline produces output for every input with a matching mask -/
theorem pipeline_soundness (weights : List ℝ) (masks : List Bool)
    (h_len : weights.length = masks.length) :
    (pipeline weights masks).length = weights.length := by
  simp only [pipeline, List.length_zipWith, h_len, min_self]

/-- Pipeline output fully determined by inputs (no hidden state) -/
theorem pipeline_completeness (weights1 weights2 : List ℝ) (masks1 masks2 : List Bool)
    (h_w : weights1 = weights2)
    (h_m : masks1 = masks2) :
    pipeline weights1 masks1 = pipeline weights2 masks2 := by
  rw [h_w, h_m]

end