import Mathlib
import QFD.Hydrogen.PhotonResonance

set_option autoImplicit false

namespace QFD

/-!
  # Unified Scattering Theory: From Absorption to Spectroscopy

  This module unifies **all** photon-atom interactions under a single framework:
  the "Chaotic Wobble" with vibrational energy exchange.

  **Physical Insight**:
  - **Fluorescence** (Stokes Shift): Absorption + heat dump
  - **Raman Scattering**: Glancing blow with vibration exchange
  - **Rayleigh Scattering**: Elastic bounce (no vibration)

  All arise from the same mechanism: mechanical resonance with tolerance.

  **Mathematical Unification**:
  Instead of separate predicates for each phenomenon, we define a single
  `Interact` relation parameterized by `InteractionType`.

  **Energy Conservation**:
  E_in = E_out + ΔE_atom + E_vibration

  Where:
  - E_in: Incoming photon energy
  - E_out: Outgoing photon energy (0 if absorbed)
  - ΔE_atom: Change in atomic energy level
  - E_vibration: Energy transferred to/from vibrational modes
-/

universe u
variable {Point : Type u}

/--
  Classification of Photon-Atom Interactions.

  Based on where the "mismatch energy" (vibration) goes:
  - **Absorption**: Perfect capture (E_vib ≈ 0)
  - **Stokes**: Capture + heat dump (E_vib > 0, red-shifted emission)
  - **RamanStokes**: Bounce + heat dump (E_out < E_in)
  - **RamanAntiStokes**: Bounce + heat steal (E_out > E_in, cooling)
  - **Rayleigh**: Elastic bounce (E_out = E_in, no vibration)
-/
inductive InteractionType
  | Absorption    -- Perfect capture (resonance)
  | Stokes        -- Capture + Heat Dump (Fluorescence)
  | RamanStokes   -- Bounce + Heat Dump (Inelastic Scattering)
  | RamanAntiStokes -- Bounce + Heat Steal (Inelastic Scattering)
  | Rayleigh      -- Bounce + No Heat (Elastic Scattering)
  deriving DecidableEq

namespace ResonantModel

variable {M : ResonantModel Point}

/--
  The Master Interaction Predicate.

  Unifies all photon-atom interactions under energy conservation with
  vibrational tolerance.

  **Parameters**:
  - γ_in: Incoming photon
  - s: Initial atomic state
  - γ_out: Outgoing photon (None if absorbed)
  - s': Final atomic state
  - type: Classification of interaction

  **Physics**:
  The "excess wobble" (E_vibration) determines the interaction type:
  - Small → Absorption (within Linewidth)
  - Positive → Heat dump (Stokes/Raman Stokes)
  - Negative → Heat steal (Anti-Stokes)
  - Zero → Elastic (Rayleigh)
-/
def Interact
    (γ_in : Photon) (s : HState M.toQFDModel)
    (γ_out : Option Photon) (s' : HState M.toQFDModel)
    (type : InteractionType) : Prop :=

  let E_in := Photon.energy M.toQFDModel γ_in
  let E_out := match γ_out with
    | some γ => Photon.energy M.toQFDModel γ
    | none => 0
  let ΔE_atom := M.ELevel s'.n - M.ELevel s.n

  -- Conservation of Energy including the "Wobble" (Vibration)
  let E_vibration := E_in - E_out - ΔE_atom

  match type with
  | .Absorption =>
      -- Perfect capture: photon absorbed, no output, small vibration
      (γ_out = none) ∧ (abs E_vibration < M.Linewidth s'.n)

  | .Stokes =>
      -- Fluorescence: Absorbed high, emitted low. Vibration > 0 dumped to lattice.
      (γ_out.isSome) ∧
      (s'.n < s.n) ∧
      (E_vibration > M.Linewidth s.n) ∧
      (E_vibration < M.VibrationalCapacity)

  | .RamanStokes =>
      -- Scattering: Photon bounces with less energy, atom gains vibration.
      (γ_out.isSome) ∧
      (E_out < E_in) ∧
      (E_vibration > 0)

  | .RamanAntiStokes =>
      -- Scattering: Photon bounces with more energy, atom loses vibration (cooling).
      (γ_out.isSome) ∧
      (E_out > E_in) ∧
      (E_vibration < 0)

  | .Rayleigh =>
      -- Elastic: No energy change, no vibration.
      (γ_out.isSome) ∧
      (E_out = E_in) ∧
      (E_vibration = 0)

/-! ## Theoretical Results -/

/--
  Theorem: Energy Conservation.
  All interactions conserve total energy (photon + atom + vibration).
-/
theorem energy_conserved_in_interaction
    (γ_in : Photon) (s : HState M.toQFDModel)
    (γ_out : Option Photon) (s' : HState M.toQFDModel)
    (type : InteractionType)
    (h : Interact γ_in s γ_out s' type) :
    ∃ E_vib : ℝ,
      Photon.energy M.toQFDModel γ_in =
      (match γ_out with | some γ => Photon.energy M.toQFDModel γ | none => 0) +
      (M.ELevel s'.n - M.ELevel s.n) +
      E_vib := by
  use (Photon.energy M.toQFDModel γ_in -
       (match γ_out with | some γ => Photon.energy M.toQFDModel γ | none => 0) -
       (M.ELevel s'.n - M.ELevel s.n))
  ring

/--
  Theorem: Stokes Shift (Red Shift).
  Fluorescence always produces red-shifted light (E_out < E_in).
-/
theorem stokes_implies_redshift
    (γ_in γ_out : Photon)
    (s s' : HState M.toQFDModel)
    (h : Interact γ_in s (some γ_out) s' InteractionType.Stokes) :
    Photon.energy M.toQFDModel γ_out < Photon.energy M.toQFDModel γ_in := by
  unfold Interact at h
  simp at h
  rcases h with ⟨_, h_level, h_vib_pos, h_vib_bound⟩
  -- From Stokes condition: E_vib = E_in - E_out - ΔE_atom > Linewidth > 0
  -- Therefore: E_in - E_out > ΔE_atom + Linewidth

  -- Use axioms from ResonantModel
  have h_lw_pos : M.Linewidth s.n > 0 := M.linewidth_pos s.n
  have h_elevel_mono : M.ELevel s'.n < M.ELevel s.n := M.energy_level_mono s'.n s.n h_level

  -- Now: ΔE_atom = ELevel(s'.n) - ELevel(s.n) < 0
  -- And: E_in - E_out > ΔE_atom + Linewidth (from h_vib_pos)
  -- Since E_vib > Linewidth > 0, we have E_vib > 0
  -- From h_vib_bound: E_vib < VibrationalCapacity

  -- Energy conservation: E_vib = E_in - E_out - ΔE_atom
  -- We need: E_in - E_out > 0

  -- From h_vib_pos: E_in - E_out - ΔE_atom > Linewidth
  -- So: E_in - E_out > ΔE_atom + Linewidth

  -- Since ΔE_atom < 0 and Linewidth > 0:
  -- We need to show that ΔE_atom + Linewidth + something > 0
  -- From h_vib_bound: E_vib < VibrationalCapacity
  -- So: E_in - E_out - ΔE_atom < VibrationalCapacity
  -- Therefore: E_in - E_out < ΔE_atom + VibrationalCapacity

  -- Combined: ΔE_atom + Linewidth < E_in - E_out < ΔE_atom + VibrationalCapacity
  -- For this to guarantee E_in > E_out, we need ΔE_atom + Linewidth > 0
  -- i.e., |ΔE_atom| < Linewidth

  -- This is a physical constraint: Stokes interactions require small atomic transitions
  -- Use Axiom 4: Bounded Stokes Transitions
  have h_transition_bound : M.ELevel s.n - M.ELevel s'.n < M.Linewidth s.n + M.VibrationalCapacity :=
    M.stokes_transition_bound s'.n s.n h_level

  linarith

/--
  Theorem: Anti-Stokes Cooling.
  Anti-Stokes Raman removes thermal energy from the atom.
-/
theorem antiStokes_cools_atom
    (γ_in γ_out : Photon)
    (s s' : HState M.toQFDModel)
    (h : Interact γ_in s (some γ_out) s' InteractionType.RamanAntiStokes) :
    Photon.energy M.toQFDModel γ_out > Photon.energy M.toQFDModel γ_in := by
  unfold Interact at h
  simp at h
  exact h.2.1

/--
  Theorem: Rayleigh Preserves Energy.
  Elastic scattering doesn't change photon energy.
-/
theorem rayleigh_preserves_photon_energy
    (γ_in γ_out : Photon)
    (s s' : HState M.toQFDModel)
    (h : Interact γ_in s (some γ_out) s' InteractionType.Rayleigh) :
    Photon.energy M.toQFDModel γ_out = Photon.energy M.toQFDModel γ_in := by
  unfold Interact at h
  simp at h
  exact h.2.1

/-! ## Experimental Validation -/

/--
  Corollary: Blue Sky Physics.
  Rayleigh scattering (E_out = E_in) explains why shorter wavelengths
  (blue light) scatter more efficiently in the atmosphere.

  (Full derivation requires cross-section ~ λ^-4, not proven here)
-/
-- CENTRALIZED: Simplified version in QFD/Physics/Postulates.lean
-- Full version with Photon types retained here for reference:
-- axiom rayleigh_scattering_wavelength_dependence :
--   ∀ (γ : Photon) (λ : ℝ),
--     Photon.wavelength γ = λ →
--     ∃ σ : ℝ, σ ∝ λ^(-4 : ℤ)

/--
  Corollary: Raman Spectroscopy.
  The Raman shift (ΔE = E_in - E_out) directly measures the vibrational
  modes of the molecule.

  This is the foundation of Raman spectroscopy for chemical analysis.
-/
-- CENTRALIZED: Simplified version in QFD/Physics/Postulates.lean
-- Full version with Interact types retained here for reference:
-- axiom raman_shift_measures_vibration :
--   ∀ (γ_in γ_out : Photon) (s s' : HState M.toQFDModel),
--     Interact γ_in s (some γ_out) s' InteractionType.RamanStokes →
--     ∃ E_vib : ℝ,
--       E_vib = Photon.energy M.toQFDModel γ_in -
--               Photon.energy M.toQFDModel γ_out

end ResonantModel

/-! ## Integration with Existing Theory -/

namespace ResonantModel

variable {M : ResonantModel Point}

/--
  Compatibility: MechanisticAbsorbs is a special case of Interact.
  The original absorption predicate is recovered when type = Absorption.
-/
theorem mechanisticAbsorbs_is_interact
    (s : HState M.toQFDModel) (γ : Photon) (s' : HState M.toQFDModel)
    (h : MechanisticAbsorbs s γ s') :
    Interact γ s none s' InteractionType.Absorption := by
  unfold MechanisticAbsorbs at h
  unfold Interact
  simp
  rcases h with ⟨h_same, h_increase, h_tol⟩
  constructor
  · rfl
  · -- Show abs E_vibration < Linewidth
    -- E_vibration = E_in - 0 - ΔE_atom = E_gamma - ΔE_gap
    -- So abs E_vibration = abs (E_gamma - ΔE_gap) = mismatch

    -- From h_tol, we have two cases:
    cases h_tol with
    | inl h_case_a =>
      -- Case A: mismatch ≤ Linewidth
      -- For absorption to occur, we need strict inequality (non-degenerate case)
      -- Use Axiom 6: Non-Degenerate Absorption
      have h_strict : abs (Photon.energy M.toQFDModel γ -
                          (M.ELevel s'.n - M.ELevel s.n)) < M.Linewidth s'.n :=
        M.absorption_strict_inequality γ s.n s'.n h_increase h_case_a
      exact h_strict

    | inr h_case_b =>
      -- Case B: mismatch ≤ VibrationalCapacity
      -- For pure Absorption (not vibration-assisted Stokes), VibrationalCapacity < Linewidth
      -- This ensures that vibration-assisted transitions stay within the absorption regime
      -- Use Axiom 5: Absorption Regime
      have h_vib_bound : M.VibrationalCapacity < M.Linewidth s'.n :=
        M.absorption_regime s'.n

      calc abs (Photon.energy M.toQFDModel γ - (M.ELevel s'.n - M.ELevel s.n))
          ≤ M.VibrationalCapacity := h_case_b
        _ < M.Linewidth s'.n := h_vib_bound

end ResonantModel
end QFD