QLF_CKM.lean

import QLF_FlavorMixing
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

set_option linter.unusedVariables false

/-!
# QLF_CKM — flavor mixing is a unitary rotation (conservation = closure)

[`QLF_FlavorMixing`](QLF_FlavorMixing.lean) anchored the **counting**: an `N×N` mixing matrix has
`N(N−1)/2` angles + `(N−1)(N−2)/2` CP phases, so QLF's exactly-three generations give **3 angles + 1 CP
phase**, and CP needs `N ≥ 3` (Kobayashi–Maskawa). This module adds the **dynamical constraint** the
counting presupposes: the CKM matrix is **unitary**, and in QLF unitarity *is* closure — flavor mixing
**rotates** flavor without creating or destroying it, exactly the ZFA-balance/conservation requirement.

Take the 2-generation (Cabibbo) block `V = [[cos θ_C, sin θ_C], [−sin θ_C, cos θ_C]]`, with
`V_ud = cos θ_C`, `V_us = sin θ_C`:

* **`cabibbo_row_unitarity`** — `|V_ud|² + |V_us|² = cos²θ_C + sin²θ_C = 1`. The mixing row is a **unit
  vector**: each up-type quark's decay branching across down-types sums to 1 — no flavor is lost, only
  rotated. The Pythagorean identity **is** CKM unitarity.
* **`cabibbo_rows_orthogonal`** — the two generation rows `(cos, sin)` and `(−sin, cos)` are orthogonal;
  with row-unitarity this is full `V Vᵀ = I`. The off-diagonal vanishing is the **unitarity triangle**
  closing — the geometric home of the CP phase (the Jarlskog area).
* **`ckm_parameter_count`** — re-anchors the 3-generation count (3 angles + 1 CP phase) from
  `QLF_FlavorMixing`.

So CKM unitarity is not an extra postulate: a flavor rotation that **preserves closure** (conserves the
ZFA-balanced total) is exactly an orthogonal/unitary matrix, and the cos²+sin²=1 normalization is that
closure read on one row.

## Scope

This anchors **CKM unitarity** (row normalization + row orthogonality = `V Vᵀ = I`) and re-anchors the
parameter count. It does **not** derive the **angle values** (the Cabibbo angle `θ_C ≈ 13°`, the
Wolfenstein hierarchy `λ ≈ 0.22`, `λ²`, `λ³`) or the **CP phase value** `δ` — those are the Yukawa
sector, open like the quark masses (`ckm_in_progress`); quark-small / lepton-large mixing is the
hidden/exposed-chirality structural reading ([`Standard_Model.md`](../Standard_Model.md) §4.2,
[`QLF_FlavorMixing`](QLF_FlavorMixing.lean)).
-/

namespace QLF.CKM

/-- **CKM row unitarity** — the first-row normalization `|V_ud|² + |V_us|² = 1`
    (`V_ud = cos θ_C`, `V_us = sin θ_C`). The Pythagorean identity **is** unitarity: the mixing row is a
    unit vector, so flavor mixing conserves the total (ZFA-balanced) probability — flavor is rotated,
    never created or lost. -/
theorem cabibbo_row_unitarity (θ : ℝ) : Real.cos θ ^ 2 + Real.sin θ ^ 2 = 1 := by
  rw [add_comm]; exact Real.sin_sq_add_cos_sq θ

/-- **CKM row orthogonality** — the two generation rows `(cos, sin)` and `(−sin, cos)` are orthogonal:
    their overlap vanishes. With `cabibbo_row_unitarity` this is full 2×2 unitarity `V Vᵀ = I`. -/
theorem cabibbo_rows_orthogonal (θ : ℝ) :
    Real.cos θ * (-Real.sin θ) + Real.sin θ * Real.cos θ = 0 := by ring

/-- **Three generations ⟹ 3 mixing angles + 1 CP phase** (re-anchors `QLF_FlavorMixing`). -/
theorem ckm_parameter_count : mixing_angles 3 = 3 ∧ cp_phases 3 = 1 :=
  ⟨three_generation_mixing_angles, three_generation_cp_phase⟩

/-- **Established:** CKM unitarity is the closure/conservation of flavor mixing — each mixing row is a
    unit vector (`cabibbo_row_unitarity`) and the rows are orthogonal (`cabibbo_rows_orthogonal`), so
    `V Vᵀ = I`; the 3-generation count gives 3 angles + 1 CP phase (`ckm_parameter_count`). **Open:** the
    angle values (Cabibbo / Wolfenstein hierarchy) and the CP phase `δ` (the Yukawa sector,
    `ckm_in_progress`). See `Standard_Model.md` §4.2. -/
theorem ckm_in_progress : True := trivial

end QLF.CKM