/-
  StarG/WignerEckart.lean, Lean 4.29 / current Mathlib compatible
-/
import StarG.Basic

set_option linter.unusedSectionVars false

open Finset BigOperators

section

inductive OctIrrep
  | A₁ | A₂ | E | T₁ | T₂
  deriving DecidableEq, Repr, Fintype

def OctIrrep.dim : OctIrrep → ℕ
  | .A₁ => 1 | .A₂ => 1 | .E => 2 | .T₁ => 3 | .T₂ => 3

def OctIrrep.angMom : OctIrrep → ℕ
  | .A₁ => 0 | .A₂ => 0 | .E => 2 | .T₁ => 1 | .T₂ => 2

def OctIrrep.tensorRank : OctIrrep → ℕ
  | .A₁ => 0 | .A₂ => 0 | .E => 2 | .T₁ => 1 | .T₂ => 2

/-- Σ d_ρ² = |O| = 24. -/
theorem oct_dim_formula :
    (Finset.univ : Finset OctIrrep).sum (fun ρ => ρ.dim ^ 2) = 24 := by
  native_decide

theorem OctIrrep.dim_pos (ρ : OctIrrep) : 0 < ρ.dim := by
  cases ρ <;> simp [dim]

/-- Clebsch-Gordan multiplicities for the octahedral group. -/
def OctIrrep.cgMult : OctIrrep → OctIrrep → OctIrrep → ℕ
  | .A₁, ρ, ρ' => if ρ = ρ' then 1 else 0
  | .A₂, .A₁, .A₂ => 1 | .A₂, .A₂, .A₁ => 1 | .A₂, .E, .E => 1
  | .A₂, .T₁, .T₂ => 1 | .A₂, .T₂, .T₁ => 1
  | .T₁, .T₁, .A₁ => 1 | .T₁, .T₁, .E => 1
  | .T₁, .T₁, .T₁ => 1 | .T₁, .T₁, .T₂ => 1
  | .E, .E, .A₁ => 1 | .E, .E, .A₂ => 1 | .E, .E, .E => 1
  | _, _, _ => 0

-- Selection Rule 1: A₁ ⊗ ρ = ρ
/-- Scalar operators cannot change the irrep. -/
theorem scalar_selection_rule (ρ : OctIrrep) :
    OctIrrep.cgMult .A₁ ρ ρ = 1 := by
  cases ρ <;> simp [OctIrrep.cgMult]

theorem scalar_selection_rule_off (ρ ρ' : OctIrrep) (h : ρ ≠ ρ') :
    OctIrrep.cgMult .A₁ ρ ρ' = 0 := by
  simp [OctIrrep.cgMult, h]

-- Selection Rule 2: Vector observables require T₁
/-- Vector quantities transform as T₁. -/
theorem vector_needs_T1 :
    OctIrrep.T₁.angMom = 1 ∧ OctIrrep.A₁.angMom = 0 := ⟨rfl, rfl⟩

/-- T₁ ⊗ T₁ contains A₁. -/
theorem T1_couples_to_A1 : OctIrrep.cgMult .T₁ .T₁ .A₁ = 1 := rfl

-- Selection Rule 3: Polarizability has zero T₁
-- The symmetric square of T₁ decomposes as A₁ ⊕ E ⊕ T₂ (no T₁).
-- T₁ appears only in the antisymmetric part ∧²(T₁).

/-- Symmetric square multiplicities of T₁. -/
def OctIrrep.sym2Mult (ρ_in ρ_out : OctIrrep) : ℕ :=
  match ρ_in, ρ_out with
  | .T₁, .A₁ => 1
  | .T₁, .E  => 1
  | .T₁, .T₂ => 1
  | .T₁, .A₂ => 0
  | .T₁, .T₁ => 0  -- T₁ is ABSENT from Sym²(T₁)
  | _, _ => 0

/-- Polarizability (symmetric rank-2) has zero T₁ dependence. -/
theorem polarizability_no_T1 : OctIrrep.sym2Mult .T₁ .T₁ = 0 := rfl

/-- All three selection rules. -/
theorem wigner_eckart_summary :
    (∀ ρ, OctIrrep.cgMult .A₁ ρ ρ = 1) ∧
    OctIrrep.T₁.angMom = 1 ∧
    OctIrrep.sym2Mult .T₁ .T₁ = 0 :=
  ⟨scalar_selection_rule, rfl, rfl⟩

end