import Mathlib.Data.Real.Basic
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

/-
# Angular Selection Theorem (Appendix P.1)

This file formalizes the geometric argument that the overlap of
photon polarization bivectors after a rotor action is `cos θ`.
The proof works in a reduced model that keeps only the two active
components (coefficients of γ₁ ∧ γ₀ and γ₃ ∧ γ₀) because the rotor
in Appendix P acts entirely inside that plane.
-/

namespace QFD

/-- Minimal two–component representation of polarization bivectors.

* `x` tracks the coefficient in front of γ₁ ∧ γ₀ (incoming polarization).
* `z` tracks the coefficient in front of γ₃ ∧ γ₀ (scattered component).
-/
structure PolarizationBivector where
  x : ℝ
  z : ℝ

/-- Scalar product induced by the spacetime scalar part on bivectors. -/
@[simp] def PolarizationBivector.dot (a b : PolarizationBivector) : ℝ :=
  a.x * b.x + a.z * b.z

/-- Rotor action generated by γ₃ ∧ γ₁.

In the `(x,z)` coordinate plane the rotor is the usual 2D rotation:
```
(x,z) ↦ (cos θ · x - sin θ · z,  sin θ · x + cos θ · z).
``` -/
noncomputable def PolarizationBivector.rotate (θ : ℝ)
    (F : PolarizationBivector) : PolarizationBivector :=
  { x := Real.cos θ * F.x - Real.sin θ * F.z
  , z := Real.sin θ * F.x + Real.cos θ * F.z }

/-- Incoming polarization bivector (aligned with γ₁ ∧ γ₀). -/
def PolarizationBivector.F_in : PolarizationBivector :=
  ⟨1, 0⟩

/-- Outgoing polarization after the rotor action. -/
noncomputable def PolarizationBivector.F_out (θ : ℝ) : PolarizationBivector :=
  PolarizationBivector.rotate θ PolarizationBivector.F_in

/--
Angular Selection Theorem.

The rotor preserves the scalar part of the bivector overlap and the
result equals `cos θ`.  This encodes the blueprint statement
`⟨F_in, F_out⟩ = cos θ`.
-/
theorem angular_selection_is_cosine (θ : ℝ) :
    PolarizationBivector.F_in.dot (PolarizationBivector.F_out θ)
      = Real.cos θ := by
  simp [PolarizationBivector.F_in, PolarizationBivector.F_out,
    PolarizationBivector.rotate, PolarizationBivector.dot,
    mul_comm, mul_left_comm, mul_assoc]

end QFD