Physlib.Particles.FlavorPhysics.CKMMatrix.StandardParameterization.Basic

Imports

/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.Particles.FlavorPhysics.CKMMatrix.Rows
public import Physlib.Particles.FlavorPhysics.CKMMatrix.Invariants

Standard parameterization for the CKM Matrix

This file defines the standard parameterization of CKM matrices in terms of four real numbers θ₁₂, θ₁₃, θ₂₃ and δ₁₃.

We will show that every CKM matrix can be written within this standard parameterization in the file FlavorPhysics.CKMMatrix.StandardParameters.

@[expose] public section

Given four reals θ₁₂ θ₁₃ θ₂₃ δ₁₃ the standard parameterization of the CKM matrix as a 3×3 complex matrix.

def standParamAsMatrix (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : Matrix (Fin 3) (Fin 3) ℂ :=
  ![![Real.cos θ₁₂ * Real.cos θ₁₃, Real.sin θ₁₂ * Real.cos θ₁₃, Real.sin θ₁₃ * exp (-I * δ₁₃)],
    ![(-Real.sin θ₁₂ * Real.cos θ₂₃) - (Real.cos θ₁₂ * Real.sin θ₁₃ * Real.sin θ₂₃ * exp (I * δ₁₃)),
      Real.cos θ₁₂ * Real.cos θ₂₃ - Real.sin θ₁₂ * Real.sin θ₁₃ * Real.sin θ₂₃ * exp (I * δ₁₃),
      Real.sin θ₂₃ * Real.cos θ₁₃],
    ![Real.sin θ₁₂ * Real.sin θ₂₃ - Real.cos θ₁₂ * Real.sin θ₁₃ * Real.cos θ₂₃ * exp (I * δ₁₃),
      (-Real.cos θ₁₂ * Real.sin θ₂₃) - (Real.sin θ₁₂ * Real.sin θ₁₃ * Real.cos θ₂₃ * exp (I * δ₁₃)),
      Real.cos θ₂₃ * Real.cos θ₁₃]]

The standard parameterization forms a unitary matrix.

lemma standParamAsMatrix_unitary (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) :
    ((standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃)ᴴ * standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃) = 1 := byθ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ (standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃)ᴴ * standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃ = 1
  funext j iθ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝj:Fin 3i:Fin 3⊢ ((standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃)ᴴ * standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃) j i = 1 j i
  fin_cases j«0»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝi:Fin 3⊢ ((standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃)ᴴ * standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃) ((fun i => i) ⟨0, ⋯⟩) i =
  1 ((fun i => i) ⟨0, ⋯⟩) i«1»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝi:Fin 3⊢ ((standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃)ᴴ * standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃) ((fun i => i) ⟨1, ⋯⟩) i =
  1 ((fun i => i) ⟨1, ⋯⟩) i«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝi:Fin 3⊢ ((standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃)ᴴ * standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃) ((fun i => i) ⟨2, ⋯⟩) i =
  1 ((fun i => i) ⟨2, ⋯⟩) i <;>«0»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝi:Fin 3⊢ ((standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃)ᴴ * standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃) ((fun i => i) ⟨0, ⋯⟩) i =
  1 ((fun i => i) ⟨0, ⋯⟩) i«1»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝi:Fin 3⊢ ((standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃)ᴴ * standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃) ((fun i => i) ⟨1, ⋯⟩) i =
  1 ((fun i => i) ⟨1, ⋯⟩) i«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝi:Fin 3⊢ ((standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃)ᴴ * standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃) ((fun i => i) ⟨2, ⋯⟩) i =
  1 ((fun i => i) ⟨2, ⋯⟩) i fin_cases i«2».«0»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ ((standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃)ᴴ * standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃) ((fun i => i) ⟨2, ⋯⟩)
    ((fun i => i) ⟨0, ⋯⟩) =
  1 ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)«2».«1»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ ((standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃)ᴴ * standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃) ((fun i => i) ⟨2, ⋯⟩)
    ((fun i => i) ⟨1, ⋯⟩) =
  1 ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)«2».«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ ((standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃)ᴴ * standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃) ((fun i => i) ⟨2, ⋯⟩)
    ((fun i => i) ⟨2, ⋯⟩) =
  1 ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) <;>«0».«0»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ ((standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃)ᴴ * standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃) ((fun i => i) ⟨0, ⋯⟩)
    ((fun i => i) ⟨0, ⋯⟩) =
  1 ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)«0».«1»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ ((standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃)ᴴ * standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃) ((fun i => i) ⟨0, ⋯⟩)
    ((fun i => i) ⟨1, ⋯⟩) =
  1 ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)«0».«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ ((standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃)ᴴ * standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃) ((fun i => i) ⟨0, ⋯⟩)
    ((fun i => i) ⟨2, ⋯⟩) =
  1 ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩)«1».«0»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ ((standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃)ᴴ * standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃) ((fun i => i) ⟨1, ⋯⟩)
    ((fun i => i) ⟨0, ⋯⟩) =
  1 ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)«1».«1»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ ((standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃)ᴴ * standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃) ((fun i => i) ⟨1, ⋯⟩)
    ((fun i => i) ⟨1, ⋯⟩) =
  1 ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)«1».«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ ((standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃)ᴴ * standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃) ((fun i => i) ⟨1, ⋯⟩)
    ((fun i => i) ⟨2, ⋯⟩) =
  1 ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩)«2».«0»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ ((standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃)ᴴ * standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃) ((fun i => i) ⟨2, ⋯⟩)
    ((fun i => i) ⟨0, ⋯⟩) =
  1 ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)«2».«1»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ ((standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃)ᴴ * standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃) ((fun i => i) ⟨2, ⋯⟩)
    ((fun i => i) ⟨1, ⋯⟩) =
  1 ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)«2».«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ ((standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃)ᴴ * standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃) ((fun i => i) ⟨2, ⋯⟩)
    ((fun i => i) ⟨2, ⋯⟩) =
  1 ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩)
    simp only [standParamAsMatrix, mul_apply, Fin.sum_univ_three, conjTranspose_apply,
      cons_val', cons_val_zero, cons_val_one, cons_val_two, cons_val_fin_one, head_cons,
      head_fin_const, tail_cons, empty_val', RCLike.star_def, map_mul, map_sub, map_neg,
      ← exp_conj, conj_I, conj_ofReal, neg_mul, neg_neg, one_apply_eq, one_apply_ne, ne_eq,
      Fin.isValue, Fin.zero_eta, Fin.mk_one, Fin.reduceFinMk, Fin.reduceEq,
      not_false_eq_true]«2».«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ ↑(Real.sin θ₁₃) * cexp (I * ↑δ₁₃) * (↑(Real.sin θ₁₃) * cexp (-(I * ↑δ₁₃))) +
      ↑(Real.sin θ₂₃) * ↑(Real.cos θ₁₃) * (↑(Real.sin θ₂₃) * ↑(Real.cos θ₁₃)) +
    ↑(Real.cos θ₂₃) * ↑(Real.cos θ₁₃) * (↑(Real.cos θ₂₃) * ↑(Real.cos θ₁₃)) =
  1 <;>«0».«0»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ ↑(Real.cos θ₁₂) * ↑(Real.cos θ₁₃) * (↑(Real.cos θ₁₂) * ↑(Real.cos θ₁₃)) +
      (-(↑(Real.sin θ₁₂) * ↑(Real.cos θ₂₃)) -
          ↑(Real.cos θ₁₂) * ↑(Real.sin θ₁₃) * ↑(Real.sin θ₂₃) * cexp (-(I * ↑δ₁₃))) *
        (-(↑(Real.sin θ₁₂) * ↑(Real.cos θ₂₃)) - ↑(Real.cos θ₁₂) * ↑(Real.sin θ₁₃) * ↑(Real.sin θ₂₃) * cexp (I * ↑δ₁₃)) +
    (↑(Real.sin θ₁₂) * ↑(Real.sin θ₂₃) - ↑(Real.cos θ₁₂) * ↑(Real.sin θ₁₃) * ↑(Real.cos θ₂₃) * cexp (-(I * ↑δ₁₃))) *
      (↑(Real.sin θ₁₂) * ↑(Real.sin θ₂₃) - ↑(Real.cos θ₁₂) * ↑(Real.sin θ₁₃) * ↑(Real.cos θ₂₃) * cexp (I * ↑δ₁₃)) =
  1«0».«1»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ ↑(Real.cos θ₁₂) * ↑(Real.cos θ₁₃) * (↑(Real.sin θ₁₂) * ↑(Real.cos θ₁₃)) +
      (-(↑(Real.sin θ₁₂) * ↑(Real.cos θ₂₃)) -
          ↑(Real.cos θ₁₂) * ↑(Real.sin θ₁₃) * ↑(Real.sin θ₂₃) * cexp (-(I * ↑δ₁₃))) *
        (↑(Real.cos θ₁₂) * ↑(Real.cos θ₂₃) - ↑(Real.sin θ₁₂) * ↑(Real.sin θ₁₃) * ↑(Real.sin θ₂₃) * cexp (I * ↑δ₁₃)) +
    (↑(Real.sin θ₁₂) * ↑(Real.sin θ₂₃) - ↑(Real.cos θ₁₂) * ↑(Real.sin θ₁₃) * ↑(Real.cos θ₂₃) * cexp (-(I * ↑δ₁₃))) *
      (-(↑(Real.cos θ₁₂) * ↑(Real.sin θ₂₃)) - ↑(Real.sin θ₁₂) * ↑(Real.sin θ₁₃) * ↑(Real.cos θ₂₃) * cexp (I * ↑δ₁₃)) =
  0«0».«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ ↑(Real.cos θ₁₂) * ↑(Real.cos θ₁₃) * (↑(Real.sin θ₁₃) * cexp (-(I * ↑δ₁₃))) +
      (-(↑(Real.sin θ₁₂) * ↑(Real.cos θ₂₃)) -
          ↑(Real.cos θ₁₂) * ↑(Real.sin θ₁₃) * ↑(Real.sin θ₂₃) * cexp (-(I * ↑δ₁₃))) *
        (↑(Real.sin θ₂₃) * ↑(Real.cos θ₁₃)) +
    (↑(Real.sin θ₁₂) * ↑(Real.sin θ₂₃) - ↑(Real.cos θ₁₂) * ↑(Real.sin θ₁₃) * ↑(Real.cos θ₂₃) * cexp (-(I * ↑δ₁₃))) *
      (↑(Real.cos θ₂₃) * ↑(Real.cos θ₁₃)) =
  0«1».«0»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ ↑(Real.sin θ₁₂) * ↑(Real.cos θ₁₃) * (↑(Real.cos θ₁₂) * ↑(Real.cos θ₁₃)) +
      (↑(Real.cos θ₁₂) * ↑(Real.cos θ₂₃) - ↑(Real.sin θ₁₂) * ↑(Real.sin θ₁₃) * ↑(Real.sin θ₂₃) * cexp (-(I * ↑δ₁₃))) *
        (-(↑(Real.sin θ₁₂) * ↑(Real.cos θ₂₃)) - ↑(Real.cos θ₁₂) * ↑(Real.sin θ₁₃) * ↑(Real.sin θ₂₃) * cexp (I * ↑δ₁₃)) +
    (-(↑(Real.cos θ₁₂) * ↑(Real.sin θ₂₃)) - ↑(Real.sin θ₁₂) * ↑(Real.sin θ₁₃) * ↑(Real.cos θ₂₃) * cexp (-(I * ↑δ₁₃))) *
      (↑(Real.sin θ₁₂) * ↑(Real.sin θ₂₃) - ↑(Real.cos θ₁₂) * ↑(Real.sin θ₁₃) * ↑(Real.cos θ₂₃) * cexp (I * ↑δ₁₃)) =
  0«1».«1»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ ↑(Real.sin θ₁₂) * ↑(Real.cos θ₁₃) * (↑(Real.sin θ₁₂) * ↑(Real.cos θ₁₃)) +
      (↑(Real.cos θ₁₂) * ↑(Real.cos θ₂₃) - ↑(Real.sin θ₁₂) * ↑(Real.sin θ₁₃) * ↑(Real.sin θ₂₃) * cexp (-(I * ↑δ₁₃))) *
        (↑(Real.cos θ₁₂) * ↑(Real.cos θ₂₃) - ↑(Real.sin θ₁₂) * ↑(Real.sin θ₁₃) * ↑(Real.sin θ₂₃) * cexp (I * ↑δ₁₃)) +
    (-(↑(Real.cos θ₁₂) * ↑(Real.sin θ₂₃)) - ↑(Real.sin θ₁₂) * ↑(Real.sin θ₁₃) * ↑(Real.cos θ₂₃) * cexp (-(I * ↑δ₁₃))) *
      (-(↑(Real.cos θ₁₂) * ↑(Real.sin θ₂₃)) - ↑(Real.sin θ₁₂) * ↑(Real.sin θ₁₃) * ↑(Real.cos θ₂₃) * cexp (I * ↑δ₁₃)) =
  1«1».«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ ↑(Real.sin θ₁₂) * ↑(Real.cos θ₁₃) * (↑(Real.sin θ₁₃) * cexp (-(I * ↑δ₁₃))) +
      (↑(Real.cos θ₁₂) * ↑(Real.cos θ₂₃) - ↑(Real.sin θ₁₂) * ↑(Real.sin θ₁₃) * ↑(Real.sin θ₂₃) * cexp (-(I * ↑δ₁₃))) *
        (↑(Real.sin θ₂₃) * ↑(Real.cos θ₁₃)) +
    (-(↑(Real.cos θ₁₂) * ↑(Real.sin θ₂₃)) - ↑(Real.sin θ₁₂) * ↑(Real.sin θ₁₃) * ↑(Real.cos θ₂₃) * cexp (-(I * ↑δ₁₃))) *
      (↑(Real.cos θ₂₃) * ↑(Real.cos θ₁₃)) =
  0«2».«0»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ ↑(Real.sin θ₁₃) * cexp (I * ↑δ₁₃) * (↑(Real.cos θ₁₂) * ↑(Real.cos θ₁₃)) +
      ↑(Real.sin θ₂₃) * ↑(Real.cos θ₁₃) *
        (-(↑(Real.sin θ₁₂) * ↑(Real.cos θ₂₃)) - ↑(Real.cos θ₁₂) * ↑(Real.sin θ₁₃) * ↑(Real.sin θ₂₃) * cexp (I * ↑δ₁₃)) +
    ↑(Real.cos θ₂₃) * ↑(Real.cos θ₁₃) *
      (↑(Real.sin θ₁₂) * ↑(Real.sin θ₂₃) - ↑(Real.cos θ₁₂) * ↑(Real.sin θ₁₃) * ↑(Real.cos θ₂₃) * cexp (I * ↑δ₁₃)) =
  0«2».«1»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ ↑(Real.sin θ₁₃) * cexp (I * ↑δ₁₃) * (↑(Real.sin θ₁₂) * ↑(Real.cos θ₁₃)) +
      ↑(Real.sin θ₂₃) * ↑(Real.cos θ₁₃) *
        (↑(Real.cos θ₁₂) * ↑(Real.cos θ₂₃) - ↑(Real.sin θ₁₂) * ↑(Real.sin θ₁₃) * ↑(Real.sin θ₂₃) * cexp (I * ↑δ₁₃)) +
    ↑(Real.cos θ₂₃) * ↑(Real.cos θ₁₃) *
      (-(↑(Real.cos θ₁₂) * ↑(Real.sin θ₂₃)) - ↑(Real.sin θ₁₂) * ↑(Real.sin θ₁₃) * ↑(Real.cos θ₂₃) * cexp (I * ↑δ₁₃)) =
  0«2».«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ ↑(Real.sin θ₁₃) * cexp (I * ↑δ₁₃) * (↑(Real.sin θ₁₃) * cexp (-(I * ↑δ₁₃))) +
      ↑(Real.sin θ₂₃) * ↑(Real.cos θ₁₃) * (↑(Real.sin θ₂₃) * ↑(Real.cos θ₁₃)) +
    ↑(Real.cos θ₂₃) * ↑(Real.cos θ₁₃) * (↑(Real.cos θ₂₃) * ↑(Real.cos θ₁₃)) =
  1
    simp only [ofReal_cos, ofReal_sin, exp_neg]«2».«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ sin ↑θ₁₃ * cexp (I * ↑δ₁₃) * (sin ↑θ₁₃ * (cexp (I * ↑δ₁₃))⁻¹) + sin ↑θ₂₃ * cos ↑θ₁₃ * (sin ↑θ₂₃ * cos ↑θ₁₃) +
    cos ↑θ₂₃ * cos ↑θ₁₃ * (cos ↑θ₂₃ * cos ↑θ₁₃) =
  1 <;>«0».«0»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ cos ↑θ₁₂ * cos ↑θ₁₃ * (cos ↑θ₁₂ * cos ↑θ₁₃) +
      (-(sin ↑θ₁₂ * cos ↑θ₂₃) - cos ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃ * (cexp (I * ↑δ₁₃))⁻¹) *
        (-(sin ↑θ₁₂ * cos ↑θ₂₃) - cos ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃ * cexp (I * ↑δ₁₃)) +
    (sin ↑θ₁₂ * sin ↑θ₂₃ - cos ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ * (cexp (I * ↑δ₁₃))⁻¹) *
      (sin ↑θ₁₂ * sin ↑θ₂₃ - cos ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ * cexp (I * ↑δ₁₃)) =
  1«0».«1»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ cos ↑θ₁₂ * cos ↑θ₁₃ * (sin ↑θ₁₂ * cos ↑θ₁₃) +
      (-(sin ↑θ₁₂ * cos ↑θ₂₃) - cos ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃ * (cexp (I * ↑δ₁₃))⁻¹) *
        (cos ↑θ₁₂ * cos ↑θ₂₃ - sin ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃ * cexp (I * ↑δ₁₃)) +
    (sin ↑θ₁₂ * sin ↑θ₂₃ - cos ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ * (cexp (I * ↑δ₁₃))⁻¹) *
      (-(cos ↑θ₁₂ * sin ↑θ₂₃) - sin ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ * cexp (I * ↑δ₁₃)) =
  0«0».«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ cos ↑θ₁₂ * cos ↑θ₁₃ * (sin ↑θ₁₃ * (cexp (I * ↑δ₁₃))⁻¹) +
      (-(sin ↑θ₁₂ * cos ↑θ₂₃) - cos ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃ * (cexp (I * ↑δ₁₃))⁻¹) * (sin ↑θ₂₃ * cos ↑θ₁₃) +
    (sin ↑θ₁₂ * sin ↑θ₂₃ - cos ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ * (cexp (I * ↑δ₁₃))⁻¹) * (cos ↑θ₂₃ * cos ↑θ₁₃) =
  0«1».«0»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ sin ↑θ₁₂ * cos ↑θ₁₃ * (cos ↑θ₁₂ * cos ↑θ₁₃) +
      (cos ↑θ₁₂ * cos ↑θ₂₃ - sin ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃ * (cexp (I * ↑δ₁₃))⁻¹) *
        (-(sin ↑θ₁₂ * cos ↑θ₂₃) - cos ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃ * cexp (I * ↑δ₁₃)) +
    (-(cos ↑θ₁₂ * sin ↑θ₂₃) - sin ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ * (cexp (I * ↑δ₁₃))⁻¹) *
      (sin ↑θ₁₂ * sin ↑θ₂₃ - cos ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ * cexp (I * ↑δ₁₃)) =
  0«1».«1»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ sin ↑θ₁₂ * cos ↑θ₁₃ * (sin ↑θ₁₂ * cos ↑θ₁₃) +
      (cos ↑θ₁₂ * cos ↑θ₂₃ - sin ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃ * (cexp (I * ↑δ₁₃))⁻¹) *
        (cos ↑θ₁₂ * cos ↑θ₂₃ - sin ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃ * cexp (I * ↑δ₁₃)) +
    (-(cos ↑θ₁₂ * sin ↑θ₂₃) - sin ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ * (cexp (I * ↑δ₁₃))⁻¹) *
      (-(cos ↑θ₁₂ * sin ↑θ₂₃) - sin ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ * cexp (I * ↑δ₁₃)) =
  1«1».«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ sin ↑θ₁₂ * cos ↑θ₁₃ * (sin ↑θ₁₃ * (cexp (I * ↑δ₁₃))⁻¹) +
      (cos ↑θ₁₂ * cos ↑θ₂₃ - sin ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃ * (cexp (I * ↑δ₁₃))⁻¹) * (sin ↑θ₂₃ * cos ↑θ₁₃) +
    (-(cos ↑θ₁₂ * sin ↑θ₂₃) - sin ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ * (cexp (I * ↑δ₁₃))⁻¹) * (cos ↑θ₂₃ * cos ↑θ₁₃) =
  0«2».«0»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ sin ↑θ₁₃ * cexp (I * ↑δ₁₃) * (cos ↑θ₁₂ * cos ↑θ₁₃) +
      sin ↑θ₂₃ * cos ↑θ₁₃ * (-(sin ↑θ₁₂ * cos ↑θ₂₃) - cos ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃ * cexp (I * ↑δ₁₃)) +
    cos ↑θ₂₃ * cos ↑θ₁₃ * (sin ↑θ₁₂ * sin ↑θ₂₃ - cos ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ * cexp (I * ↑δ₁₃)) =
  0«2».«1»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ sin ↑θ₁₃ * cexp (I * ↑δ₁₃) * (sin ↑θ₁₂ * cos ↑θ₁₃) +
      sin ↑θ₂₃ * cos ↑θ₁₃ * (cos ↑θ₁₂ * cos ↑θ₂₃ - sin ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃ * cexp (I * ↑δ₁₃)) +
    cos ↑θ₂₃ * cos ↑θ₁₃ * (-(cos ↑θ₁₂ * sin ↑θ₂₃) - sin ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ * cexp (I * ↑δ₁₃)) =
  0«2».«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ sin ↑θ₁₃ * cexp (I * ↑δ₁₃) * (sin ↑θ₁₃ * (cexp (I * ↑δ₁₃))⁻¹) + sin ↑θ₂₃ * cos ↑θ₁₃ * (sin ↑θ₂₃ * cos ↑θ₁₃) +
    cos ↑θ₂₃ * cos ↑θ₁₃ * (cos ↑θ₂₃ * cos ↑θ₁₃) =
  1
    field_simp«2».«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ sin ↑θ₁₃ ^ 2 + sin ↑θ₂₃ ^ 2 * cos ↑θ₁₃ ^ 2 + cos ↑θ₁₃ ^ 2 * cos ↑θ₂₃ ^ 2 = 1 <;>«0».«0»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ cos ↑θ₁₂ ^ 2 * cos ↑θ₁₃ ^ 2 * cexp (I * ↑δ₁₃) +
      (-(sin ↑θ₁₂ * cos ↑θ₂₃ * cexp (I * ↑δ₁₃)) - cos ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃) *
        (-(sin ↑θ₁₂ * cos ↑θ₂₃) - cos ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃ * cexp (I * ↑δ₁₃)) +
    (sin ↑θ₁₂ * sin ↑θ₂₃ * cexp (I * ↑δ₁₃) - cos ↑θ₁₂ * cos ↑θ₂₃ * sin ↑θ₁₃) *
      (sin ↑θ₁₂ * sin ↑θ₂₃ - cos ↑θ₁₂ * cos ↑θ₂₃ * sin ↑θ₁₃ * cexp (I * ↑δ₁₃)) =
  cexp (I * ↑δ₁₃)«0».«1»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ cos ↑θ₁₂ * cos ↑θ₁₃ ^ 2 * sin ↑θ₁₂ * cexp (I * ↑δ₁₃) +
      (-(sin ↑θ₁₂ * cos ↑θ₂₃ * cexp (I * ↑δ₁₃)) - cos ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃) *
        (cos ↑θ₁₂ * cos ↑θ₂₃ - sin ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃ * cexp (I * ↑δ₁₃)) +
    (sin ↑θ₁₂ * sin ↑θ₂₃ * cexp (I * ↑δ₁₃) - cos ↑θ₁₂ * cos ↑θ₂₃ * sin ↑θ₁₃) *
      (-(cos ↑θ₁₂ * sin ↑θ₂₃) - sin ↑θ₁₂ * cos ↑θ₂₃ * sin ↑θ₁₃ * cexp (I * ↑δ₁₃)) =
  cexp (I * ↑δ₁₃) * 0«0».«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ cos ↑θ₁₃ *
    (cos ↑θ₁₂ * sin ↑θ₁₃ + sin ↑θ₂₃ * (-(cexp (I * ↑δ₁₃) * sin ↑θ₁₂ * cos ↑θ₂₃) - cos ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃) +
      cos ↑θ₂₃ * (cexp (I * ↑δ₁₃) * sin ↑θ₁₂ * sin ↑θ₂₃ - cos ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃)) =
  cexp (I * ↑δ₁₃) * 0«1».«0»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ sin ↑θ₁₂ * cos ↑θ₁₃ ^ 2 * cos ↑θ₁₂ * cexp (I * ↑δ₁₃) +
      (cos ↑θ₁₂ * cos ↑θ₂₃ * cexp (I * ↑δ₁₃) - sin ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃) *
        (-(sin ↑θ₁₂ * cos ↑θ₂₃) - cos ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃ * cexp (I * ↑δ₁₃)) +
    (-(cos ↑θ₁₂ * sin ↑θ₂₃ * cexp (I * ↑δ₁₃)) - sin ↑θ₁₂ * cos ↑θ₂₃ * sin ↑θ₁₃) *
      (sin ↑θ₁₂ * sin ↑θ₂₃ - cos ↑θ₁₂ * cos ↑θ₂₃ * sin ↑θ₁₃ * cexp (I * ↑δ₁₃)) =
  cexp (I * ↑δ₁₃) * 0«1».«1»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ sin ↑θ₁₂ ^ 2 * cos ↑θ₁₃ ^ 2 * cexp (I * ↑δ₁₃) +
      (cos ↑θ₁₂ * cos ↑θ₂₃ * cexp (I * ↑δ₁₃) - sin ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃) *
        (cos ↑θ₁₂ * cos ↑θ₂₃ - sin ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃ * cexp (I * ↑δ₁₃)) +
    (-(cos ↑θ₁₂ * sin ↑θ₂₃ * cexp (I * ↑δ₁₃)) - sin ↑θ₁₂ * cos ↑θ₂₃ * sin ↑θ₁₃) *
      (-(cos ↑θ₁₂ * sin ↑θ₂₃) - sin ↑θ₁₂ * cos ↑θ₂₃ * sin ↑θ₁₃ * cexp (I * ↑δ₁₃)) =
  cexp (I * ↑δ₁₃)«1».«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ cos ↑θ₁₃ *
    (sin ↑θ₁₂ * sin ↑θ₁₃ + sin ↑θ₂₃ * (cexp (I * ↑δ₁₃) * cos ↑θ₁₂ * cos ↑θ₂₃ - sin ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃) +
      cos ↑θ₂₃ * (-(cexp (I * ↑δ₁₃) * cos ↑θ₁₂ * sin ↑θ₂₃) - sin ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃)) =
  cexp (I * ↑δ₁₃) * 0«2».«0»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ cos ↑θ₁₃ *
    (sin ↑θ₁₃ * cexp (I * ↑δ₁₃) * cos ↑θ₁₂ +
        sin ↑θ₂₃ * (-(sin ↑θ₁₂ * cos ↑θ₂₃) - sin ↑θ₁₃ * cexp (I * ↑δ₁₃) * cos ↑θ₁₂ * sin ↑θ₂₃) +
      cos ↑θ₂₃ * (sin ↑θ₂₃ * sin ↑θ₁₂ - sin ↑θ₁₃ * cexp (I * ↑δ₁₃) * cos ↑θ₁₂ * cos ↑θ₂₃)) =
  0«2».«1»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ cos ↑θ₁₃ *
    (sin ↑θ₁₃ * cexp (I * ↑δ₁₃) * sin ↑θ₁₂ +
        sin ↑θ₂₃ * (cos ↑θ₁₂ * cos ↑θ₂₃ - sin ↑θ₁₃ * cexp (I * ↑δ₁₃) * sin ↑θ₁₂ * sin ↑θ₂₃) +
      cos ↑θ₂₃ * (-(sin ↑θ₂₃ * cos ↑θ₁₂) - sin ↑θ₁₃ * cexp (I * ↑δ₁₃) * sin ↑θ₁₂ * cos ↑θ₂₃)) =
  0«2».«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ sin ↑θ₁₃ ^ 2 + sin ↑θ₂₃ ^ 2 * cos ↑θ₁₃ ^ 2 + cos ↑θ₁₃ ^ 2 * cos ↑θ₂₃ ^ 2 = 1 ring_nf«2».«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ sin ↑θ₁₃ ^ 2 + sin ↑θ₂₃ ^ 2 * cos ↑θ₁₃ ^ 2 + cos ↑θ₁₃ ^ 2 * cos ↑θ₂₃ ^ 2 = 1 <;>«0».«0»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ cos ↑θ₁₂ ^ 2 * cos ↑θ₁₃ ^ 2 * cexp (I * ↑δ₁₃) + cos ↑θ₁₂ ^ 2 * cexp (I * ↑δ₁₃) * cos ↑θ₂₃ ^ 2 * sin ↑θ₁₃ ^ 2 +
        cos ↑θ₁₂ ^ 2 * cexp (I * ↑δ₁₃) * sin ↑θ₁₃ ^ 2 * sin ↑θ₂₃ ^ 2 +
      cexp (I * ↑δ₁₃) * sin ↑θ₁₂ ^ 2 * cos ↑θ₂₃ ^ 2 +
    cexp (I * ↑δ₁₃) * sin ↑θ₁₂ ^ 2 * sin ↑θ₂₃ ^ 2 =
  cexp (I * ↑δ₁₃)«0».«1»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ cos ↑θ₁₂ * cos ↑θ₁₃ ^ 2 * sin ↑θ₁₂ * cexp (I * ↑δ₁₃) - cos ↑θ₁₂ * sin ↑θ₁₂ * cexp (I * ↑δ₁₃) * cos ↑θ₂₃ ^ 2 +
        cos ↑θ₁₂ * sin ↑θ₁₂ * cexp (I * ↑δ₁₃) * cos ↑θ₂₃ ^ 2 * sin ↑θ₁₃ ^ 2 +
      cos ↑θ₁₂ * sin ↑θ₁₂ * cexp (I * ↑δ₁₃) * sin ↑θ₁₃ ^ 2 * sin ↑θ₂₃ ^ 2 -
    cos ↑θ₁₂ * sin ↑θ₁₂ * cexp (I * ↑δ₁₃) * sin ↑θ₂₃ ^ 2 =
  0«0».«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ cos ↑θ₁₃ * cos ↑θ₁₂ * sin ↑θ₁₃ - cos ↑θ₁₃ * cos ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃ ^ 2 -
    cos ↑θ₁₃ * cos ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ ^ 2 =
  0«1».«0»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ sin ↑θ₁₂ * cos ↑θ₁₃ ^ 2 * cos ↑θ₁₂ * cexp (I * ↑δ₁₃) - sin ↑θ₁₂ * cos ↑θ₁₂ * cexp (I * ↑δ₁₃) * cos ↑θ₂₃ ^ 2 +
        sin ↑θ₁₂ * cos ↑θ₁₂ * cexp (I * ↑δ₁₃) * cos ↑θ₂₃ ^ 2 * sin ↑θ₁₃ ^ 2 +
      sin ↑θ₁₂ * cos ↑θ₁₂ * cexp (I * ↑δ₁₃) * sin ↑θ₁₃ ^ 2 * sin ↑θ₂₃ ^ 2 -
    sin ↑θ₁₂ * cos ↑θ₁₂ * cexp (I * ↑δ₁₃) * sin ↑θ₂₃ ^ 2 =
  0«1».«1»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ sin ↑θ₁₂ ^ 2 * cos ↑θ₁₃ ^ 2 * cexp (I * ↑δ₁₃) + sin ↑θ₁₂ ^ 2 * cexp (I * ↑δ₁₃) * cos ↑θ₂₃ ^ 2 * sin ↑θ₁₃ ^ 2 +
        sin ↑θ₁₂ ^ 2 * cexp (I * ↑δ₁₃) * sin ↑θ₁₃ ^ 2 * sin ↑θ₂₃ ^ 2 +
      cexp (I * ↑δ₁₃) * cos ↑θ₁₂ ^ 2 * cos ↑θ₂₃ ^ 2 +
    cexp (I * ↑δ₁₃) * cos ↑θ₁₂ ^ 2 * sin ↑θ₂₃ ^ 2 =
  cexp (I * ↑δ₁₃)«1».«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ cos ↑θ₁₃ * sin ↑θ₁₂ * sin ↑θ₁₃ - cos ↑θ₁₃ * sin ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃ ^ 2 -
    cos ↑θ₁₃ * sin ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ ^ 2 =
  0«2».«0»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ cos ↑θ₁₃ * sin ↑θ₁₃ * cexp (I * ↑δ₁₃) * cos ↑θ₁₂ - cos ↑θ₁₃ * sin ↑θ₁₃ * cexp (I * ↑δ₁₃) * cos ↑θ₁₂ * sin ↑θ₂₃ ^ 2 -
    cos ↑θ₁₃ * sin ↑θ₁₃ * cexp (I * ↑δ₁₃) * cos ↑θ₁₂ * cos ↑θ₂₃ ^ 2 =
  0«2».«1»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ cos ↑θ₁₃ * sin ↑θ₁₃ * cexp (I * ↑δ₁₃) * sin ↑θ₁₂ - cos ↑θ₁₃ * sin ↑θ₁₃ * cexp (I * ↑δ₁₃) * sin ↑θ₁₂ * sin ↑θ₂₃ ^ 2 -
    cos ↑θ₁₃ * sin ↑θ₁₃ * cexp (I * ↑δ₁₃) * sin ↑θ₁₂ * cos ↑θ₂₃ ^ 2 =
  0«2».«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ sin ↑θ₁₃ ^ 2 + sin ↑θ₂₃ ^ 2 * cos ↑θ₁₃ ^ 2 + cos ↑θ₁₃ ^ 2 * cos ↑θ₂₃ ^ 2 = 1 simp only [Complex.sin_sq]«2».«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ 1 - cos ↑θ₁₃ ^ 2 + (1 - cos ↑θ₂₃ ^ 2) * cos ↑θ₁₃ ^ 2 + cos ↑θ₁₃ ^ 2 * cos ↑θ₂₃ ^ 2 = 1 <;>«0».«0»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ cos ↑θ₁₂ ^ 2 * cos ↑θ₁₃ ^ 2 * cexp (I * ↑δ₁₃) + cos ↑θ₁₂ ^ 2 * cexp (I * ↑δ₁₃) * cos ↑θ₂₃ ^ 2 * (1 - cos ↑θ₁₃ ^ 2) +
        cos ↑θ₁₂ ^ 2 * cexp (I * ↑δ₁₃) * (1 - cos ↑θ₁₃ ^ 2) * (1 - cos ↑θ₂₃ ^ 2) +
      cexp (I * ↑δ₁₃) * (1 - cos ↑θ₁₂ ^ 2) * cos ↑θ₂₃ ^ 2 +
    cexp (I * ↑δ₁₃) * (1 - cos ↑θ₁₂ ^ 2) * (1 - cos ↑θ₂₃ ^ 2) =
  cexp (I * ↑δ₁₃)«0».«1»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ cos ↑θ₁₂ * cos ↑θ₁₃ ^ 2 * sin ↑θ₁₂ * cexp (I * ↑δ₁₃) - cos ↑θ₁₂ * sin ↑θ₁₂ * cexp (I * ↑δ₁₃) * cos ↑θ₂₃ ^ 2 +
        cos ↑θ₁₂ * sin ↑θ₁₂ * cexp (I * ↑δ₁₃) * cos ↑θ₂₃ ^ 2 * (1 - cos ↑θ₁₃ ^ 2) +
      cos ↑θ₁₂ * sin ↑θ₁₂ * cexp (I * ↑δ₁₃) * (1 - cos ↑θ₁₃ ^ 2) * (1 - cos ↑θ₂₃ ^ 2) -
    cos ↑θ₁₂ * sin ↑θ₁₂ * cexp (I * ↑δ₁₃) * (1 - cos ↑θ₂₃ ^ 2) =
  0«0».«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ cos ↑θ₁₃ * cos ↑θ₁₂ * sin ↑θ₁₃ - cos ↑θ₁₃ * cos ↑θ₁₂ * sin ↑θ₁₃ * (1 - cos ↑θ₂₃ ^ 2) -
    cos ↑θ₁₃ * cos ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ ^ 2 =
  0«1».«0»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ sin ↑θ₁₂ * cos ↑θ₁₃ ^ 2 * cos ↑θ₁₂ * cexp (I * ↑δ₁₃) - sin ↑θ₁₂ * cos ↑θ₁₂ * cexp (I * ↑δ₁₃) * cos ↑θ₂₃ ^ 2 +
        sin ↑θ₁₂ * cos ↑θ₁₂ * cexp (I * ↑δ₁₃) * cos ↑θ₂₃ ^ 2 * (1 - cos ↑θ₁₃ ^ 2) +
      sin ↑θ₁₂ * cos ↑θ₁₂ * cexp (I * ↑δ₁₃) * (1 - cos ↑θ₁₃ ^ 2) * (1 - cos ↑θ₂₃ ^ 2) -
    sin ↑θ₁₂ * cos ↑θ₁₂ * cexp (I * ↑δ₁₃) * (1 - cos ↑θ₂₃ ^ 2) =
  0«1».«1»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ (1 - cos ↑θ₁₂ ^ 2) * cos ↑θ₁₃ ^ 2 * cexp (I * ↑δ₁₃) +
          (1 - cos ↑θ₁₂ ^ 2) * cexp (I * ↑δ₁₃) * cos ↑θ₂₃ ^ 2 * (1 - cos ↑θ₁₃ ^ 2) +
        (1 - cos ↑θ₁₂ ^ 2) * cexp (I * ↑δ₁₃) * (1 - cos ↑θ₁₃ ^ 2) * (1 - cos ↑θ₂₃ ^ 2) +
      cexp (I * ↑δ₁₃) * cos ↑θ₁₂ ^ 2 * cos ↑θ₂₃ ^ 2 +
    cexp (I * ↑δ₁₃) * cos ↑θ₁₂ ^ 2 * (1 - cos ↑θ₂₃ ^ 2) =
  cexp (I * ↑δ₁₃)«1».«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ cos ↑θ₁₃ * sin ↑θ₁₂ * sin ↑θ₁₃ - cos ↑θ₁₃ * sin ↑θ₁₂ * sin ↑θ₁₃ * (1 - cos ↑θ₂₃ ^ 2) -
    cos ↑θ₁₃ * sin ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ ^ 2 =
  0«2».«0»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ cos ↑θ₁₃ * sin ↑θ₁₃ * cexp (I * ↑δ₁₃) * cos ↑θ₁₂ -
      cos ↑θ₁₃ * sin ↑θ₁₃ * cexp (I * ↑δ₁₃) * cos ↑θ₁₂ * (1 - cos ↑θ₂₃ ^ 2) -
    cos ↑θ₁₃ * sin ↑θ₁₃ * cexp (I * ↑δ₁₃) * cos ↑θ₁₂ * cos ↑θ₂₃ ^ 2 =
  0«2».«1»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ cos ↑θ₁₃ * sin ↑θ₁₃ * cexp (I * ↑δ₁₃) * sin ↑θ₁₂ -
      cos ↑θ₁₃ * sin ↑θ₁₃ * cexp (I * ↑δ₁₃) * sin ↑θ₁₂ * (1 - cos ↑θ₂₃ ^ 2) -
    cos ↑θ₁₃ * sin ↑θ₁₃ * cexp (I * ↑δ₁₃) * sin ↑θ₁₂ * cos ↑θ₂₃ ^ 2 =
  0«2».«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ 1 - cos ↑θ₁₃ ^ 2 + (1 - cos ↑θ₂₃ ^ 2) * cos ↑θ₁₃ ^ 2 + cos ↑θ₁₃ ^ 2 * cos ↑θ₂₃ ^ 2 = 1 ringAll goals completed! 🐙

A CKM Matrix from four reals θ₁₂, θ₁₃, θ₂₃, and δ₁₃. This is the standard parameterization of CKM matrices.


def standParam (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : CKMMatrix :=
  ⟨standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃, byθ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃ ∈ unitaryGroup (Fin 3) ℂ
    rw [mem_unitaryGroup_iff'θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ star (standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃) * standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃ = 1θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ star (standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃) * standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃ = 1]θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ star (standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃) * standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃ = 1
    exact standParamAsMatrix_unitary θ₁₂ θ₁₃ θ₂₃ δ₁₃All goals completed! 🐙⟩

The top-row of the standard parameterization is the cross product of the conjugate of the up and charm rows.


lemma cross_product_t (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) :
    [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]t =
    (conj [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]u ⨯₃ conj [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]c) := byθ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]t =
  (crossProduct ((starRingEnd (Fin 3 → ℂ)) [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]u))
    ((starRingEnd (Fin 3 → ℂ)) [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]c)
  funext iθ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝi:Fin 3⊢ [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]t i =
  (crossProduct ((starRingEnd (Fin 3 → ℂ)) [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]u))
    ((starRingEnd (Fin 3 → ℂ)) [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]c) i
  fin_cases i«0»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]t ((fun i => i) ⟨0, ⋯⟩) =
  (crossProduct ((starRingEnd (Fin 3 → ℂ)) [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]u))
    ((starRingEnd (Fin 3 → ℂ)) [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]c) ((fun i => i) ⟨0, ⋯⟩)«1»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]t ((fun i => i) ⟨1, ⋯⟩) =
  (crossProduct ((starRingEnd (Fin 3 → ℂ)) [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]u))
    ((starRingEnd (Fin 3 → ℂ)) [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]c) ((fun i => i) ⟨1, ⋯⟩)«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]t ((fun i => i) ⟨2, ⋯⟩) =
  (crossProduct ((starRingEnd (Fin 3 → ℂ)) [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]u))
    ((starRingEnd (Fin 3 → ℂ)) [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]c) ((fun i => i) ⟨2, ⋯⟩) <;>«0»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]t ((fun i => i) ⟨0, ⋯⟩) =
  (crossProduct ((starRingEnd (Fin 3 → ℂ)) [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]u))
    ((starRingEnd (Fin 3 → ℂ)) [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]c) ((fun i => i) ⟨0, ⋯⟩)«1»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]t ((fun i => i) ⟨1, ⋯⟩) =
  (crossProduct ((starRingEnd (Fin 3 → ℂ)) [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]u))
    ((starRingEnd (Fin 3 → ℂ)) [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]c) ((fun i => i) ⟨1, ⋯⟩)«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]t ((fun i => i) ⟨2, ⋯⟩) =
  (crossProduct ((starRingEnd (Fin 3 → ℂ)) [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]u))
    ((starRingEnd (Fin 3 → ℂ)) [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]c) ((fun i => i) ⟨2, ⋯⟩)
    simp only [tRow, standParam, standParamAsMatrix, neg_mul, exp_neg, Fin.isValue, cons_val',
      cons_val_zero, empty_val', cons_val_fin_one, cons_val_two, tail_cons, head_fin_const,
      cons_val_one, head_cons, Fin.zero_eta, Fin.mk_one, Fin.reduceFinMk, crossProduct, uRow, cRow,
      LinearMap.mk₂_apply, Pi.conj_apply, _root_.map_mul, map_inv₀, ← exp_conj, conj_I, conj_ofReal,
      inv_inv, map_sub, map_neg]«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ ↑(Real.cos θ₂₃) * ↑(Real.cos θ₁₃) =
  ↑(Real.cos θ₁₂) * ↑(Real.cos θ₁₃) *
      (↑(Real.cos θ₁₂) * ↑(Real.cos θ₂₃) - ↑(Real.sin θ₁₂) * ↑(Real.sin θ₁₃) * ↑(Real.sin θ₂₃) * (cexp (I * ↑δ₁₃))⁻¹) -
    ↑(Real.sin θ₁₂) * ↑(Real.cos θ₁₃) *
      (-(↑(Real.sin θ₁₂) * ↑(Real.cos θ₂₃)) - ↑(Real.cos θ₁₂) * ↑(Real.sin θ₁₃) * ↑(Real.sin θ₂₃) * (cexp (I * ↑δ₁₃))⁻¹) <;>«0»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ ↑(Real.sin θ₁₂) * ↑(Real.sin θ₂₃) - ↑(Real.cos θ₁₂) * ↑(Real.sin θ₁₃) * ↑(Real.cos θ₂₃) * cexp (I * ↑δ₁₃) =
  ↑(Real.sin θ₁₂) * ↑(Real.cos θ₁₃) * (↑(Real.sin θ₂₃) * ↑(Real.cos θ₁₃)) -
    ↑(Real.sin θ₁₃) * cexp (I * ↑δ₁₃) *
      (↑(Real.cos θ₁₂) * ↑(Real.cos θ₂₃) - ↑(Real.sin θ₁₂) * ↑(Real.sin θ₁₃) * ↑(Real.sin θ₂₃) * (cexp (I * ↑δ₁₃))⁻¹)«1»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ -(↑(Real.cos θ₁₂) * ↑(Real.sin θ₂₃)) - ↑(Real.sin θ₁₂) * ↑(Real.sin θ₁₃) * ↑(Real.cos θ₂₃) * cexp (I * ↑δ₁₃) =
  ↑(Real.sin θ₁₃) * cexp (I * ↑δ₁₃) *
      (-(↑(Real.sin θ₁₂) * ↑(Real.cos θ₂₃)) -
        ↑(Real.cos θ₁₂) * ↑(Real.sin θ₁₃) * ↑(Real.sin θ₂₃) * (cexp (I * ↑δ₁₃))⁻¹) -
    ↑(Real.cos θ₁₂) * ↑(Real.cos θ₁₃) * (↑(Real.sin θ₂₃) * ↑(Real.cos θ₁₃))«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ ↑(Real.cos θ₂₃) * ↑(Real.cos θ₁₃) =
  ↑(Real.cos θ₁₂) * ↑(Real.cos θ₁₃) *
      (↑(Real.cos θ₁₂) * ↑(Real.cos θ₂₃) - ↑(Real.sin θ₁₂) * ↑(Real.sin θ₁₃) * ↑(Real.sin θ₂₃) * (cexp (I * ↑δ₁₃))⁻¹) -
    ↑(Real.sin θ₁₂) * ↑(Real.cos θ₁₃) *
      (-(↑(Real.sin θ₁₂) * ↑(Real.cos θ₂₃)) - ↑(Real.cos θ₁₂) * ↑(Real.sin θ₁₃) * ↑(Real.sin θ₂₃) * (cexp (I * ↑δ₁₃))⁻¹)
    simp only [ofReal_sin, ofReal_cos]«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ cos ↑θ₂₃ * cos ↑θ₁₃ =
  cos ↑θ₁₂ * cos ↑θ₁₃ * (cos ↑θ₁₂ * cos ↑θ₂₃ - sin ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃ * (cexp (I * ↑δ₁₃))⁻¹) -
    sin ↑θ₁₂ * cos ↑θ₁₃ * (-(sin ↑θ₁₂ * cos ↑θ₂₃) - cos ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃ * (cexp (I * ↑δ₁₃))⁻¹) <;>«0»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ sin ↑θ₁₂ * sin ↑θ₂₃ - cos ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ * cexp (I * ↑δ₁₃) =
  sin ↑θ₁₂ * cos ↑θ₁₃ * (sin ↑θ₂₃ * cos ↑θ₁₃) -
    sin ↑θ₁₃ * cexp (I * ↑δ₁₃) * (cos ↑θ₁₂ * cos ↑θ₂₃ - sin ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃ * (cexp (I * ↑δ₁₃))⁻¹)«1»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ -(cos ↑θ₁₂ * sin ↑θ₂₃) - sin ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ * cexp (I * ↑δ₁₃) =
  sin ↑θ₁₃ * cexp (I * ↑δ₁₃) * (-(sin ↑θ₁₂ * cos ↑θ₂₃) - cos ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃ * (cexp (I * ↑δ₁₃))⁻¹) -
    cos ↑θ₁₂ * cos ↑θ₁₃ * (sin ↑θ₂₃ * cos ↑θ₁₃)«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ cos ↑θ₂₃ * cos ↑θ₁₃ =
  cos ↑θ₁₂ * cos ↑θ₁₃ * (cos ↑θ₁₂ * cos ↑θ₂₃ - sin ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃ * (cexp (I * ↑δ₁₃))⁻¹) -
    sin ↑θ₁₂ * cos ↑θ₁₃ * (-(sin ↑θ₁₂ * cos ↑θ₂₃) - cos ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃ * (cexp (I * ↑δ₁₃))⁻¹)
    field_simp«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ cos ↑θ₂₃ * cos ↑θ₁₃ * cexp (I * ↑δ₁₃) =
  cos ↑θ₁₃ *
    (cos ↑θ₁₂ * (cos ↑θ₂₃ * cos ↑θ₁₂ * cexp (I * ↑δ₁₃) - sin ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃) -
      sin ↑θ₁₂ * (-(cos ↑θ₂₃ * sin ↑θ₁₂ * cexp (I * ↑δ₁₃)) - cos ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃)) <;>«0»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ sin ↑θ₁₂ * sin ↑θ₂₃ - cos ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ * cexp (I * ↑δ₁₃) =
  sin ↑θ₁₂ * sin ↑θ₂₃ * cos ↑θ₁₃ ^ 2 -
    sin ↑θ₁₃ * (cos ↑θ₁₂ * cos ↑θ₂₃ * cexp (I * ↑δ₁₃) - sin ↑θ₁₂ * sin ↑θ₂₃ * sin ↑θ₁₃)«1»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ -(cos ↑θ₁₂ * sin ↑θ₂₃) - sin ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ * cexp (I * ↑δ₁₃) =
  sin ↑θ₁₃ * (-(sin ↑θ₁₂ * cos ↑θ₂₃ * cexp (I * ↑δ₁₃)) - cos ↑θ₁₂ * sin ↑θ₂₃ * sin ↑θ₁₃) -
    cos ↑θ₁₂ * sin ↑θ₂₃ * cos ↑θ₁₃ ^ 2«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ cos ↑θ₂₃ * cos ↑θ₁₃ * cexp (I * ↑δ₁₃) =
  cos ↑θ₁₃ *
    (cos ↑θ₁₂ * (cos ↑θ₂₃ * cos ↑θ₁₂ * cexp (I * ↑δ₁₃) - sin ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃) -
      sin ↑θ₁₂ * (-(cos ↑θ₂₃ * sin ↑θ₁₂ * cexp (I * ↑δ₁₃)) - cos ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃))
    ring_nf«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ cos ↑θ₂₃ * cos ↑θ₁₃ * cexp (I * ↑δ₁₃) =
  cos ↑θ₂₃ * cos ↑θ₁₃ * cexp (I * ↑δ₁₃) * cos ↑θ₁₂ ^ 2 + cos ↑θ₂₃ * cos ↑θ₁₃ * cexp (I * ↑δ₁₃) * sin ↑θ₁₂ ^ 2 <;>«0»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ sin ↑θ₁₂ * sin ↑θ₂₃ - cos ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ * cexp (I * ↑δ₁₃) =
  sin ↑θ₁₂ * sin ↑θ₂₃ * sin ↑θ₁₃ ^ 2 + sin ↑θ₁₂ * sin ↑θ₂₃ * cos ↑θ₁₃ ^ 2 -
    cos ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ * cexp (I * ↑δ₁₃)«1»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ -(cos ↑θ₁₂ * sin ↑θ₂₃) - sin ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ * cexp (I * ↑δ₁₃) =
  -(cos ↑θ₁₂ * sin ↑θ₂₃ * sin ↑θ₁₃ ^ 2) - cos ↑θ₁₂ * sin ↑θ₂₃ * cos ↑θ₁₃ ^ 2 -
    sin ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ * cexp (I * ↑δ₁₃)«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ cos ↑θ₂₃ * cos ↑θ₁₃ * cexp (I * ↑δ₁₃) =
  cos ↑θ₂₃ * cos ↑θ₁₃ * cexp (I * ↑δ₁₃) * cos ↑θ₁₂ ^ 2 + cos ↑θ₂₃ * cos ↑θ₁₃ * cexp (I * ↑δ₁₃) * sin ↑θ₁₂ ^ 2
    rw [sin_sq«0»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ sin ↑θ₁₂ * sin ↑θ₂₃ - cos ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ * cexp (I * ↑δ₁₃) =
  sin ↑θ₁₂ * sin ↑θ₂₃ * (1 - cos ↑θ₁₃ ^ 2) + sin ↑θ₁₂ * sin ↑θ₂₃ * cos ↑θ₁₃ ^ 2 -
    cos ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ * cexp (I * ↑δ₁₃)«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ cos ↑θ₂₃ * cos ↑θ₁₃ * cexp (I * ↑δ₁₃) =
  cos ↑θ₂₃ * cos ↑θ₁₃ * cexp (I * ↑δ₁₃) * cos ↑θ₁₂ ^ 2 + cos ↑θ₂₃ * cos ↑θ₁₃ * cexp (I * ↑δ₁₃) * (1 - cos ↑θ₁₂ ^ 2)]«1»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ -(cos ↑θ₁₂ * sin ↑θ₂₃) - sin ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ * cexp (I * ↑δ₁₃) =
  -(cos ↑θ₁₂ * sin ↑θ₂₃ * (1 - cos ↑θ₁₃ ^ 2)) - cos ↑θ₁₂ * sin ↑θ₂₃ * cos ↑θ₁₃ ^ 2 -
    sin ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ * cexp (I * ↑δ₁₃)«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ cos ↑θ₂₃ * cos ↑θ₁₃ * cexp (I * ↑δ₁₃) =
  cos ↑θ₂₃ * cos ↑θ₁₃ * cexp (I * ↑δ₁₃) * cos ↑θ₁₂ ^ 2 + cos ↑θ₂₃ * cos ↑θ₁₃ * cexp (I * ↑δ₁₃) * (1 - cos ↑θ₁₂ ^ 2)«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ cos ↑θ₂₃ * cos ↑θ₁₃ * cexp (I * ↑δ₁₃) =
  cos ↑θ₂₃ * cos ↑θ₁₃ * cexp (I * ↑δ₁₃) * cos ↑θ₁₂ ^ 2 + cos ↑θ₂₃ * cos ↑θ₁₃ * cexp (I * ↑δ₁₃) * (1 - cos ↑θ₁₂ ^ 2) <;>«0»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ sin ↑θ₁₂ * sin ↑θ₂₃ - cos ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ * cexp (I * ↑δ₁₃) =
  sin ↑θ₁₂ * sin ↑θ₂₃ * (1 - cos ↑θ₁₃ ^ 2) + sin ↑θ₁₂ * sin ↑θ₂₃ * cos ↑θ₁₃ ^ 2 -
    cos ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ * cexp (I * ↑δ₁₃)«1»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ -(cos ↑θ₁₂ * sin ↑θ₂₃) - sin ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ * cexp (I * ↑δ₁₃) =
  -(cos ↑θ₁₂ * sin ↑θ₂₃ * (1 - cos ↑θ₁₃ ^ 2)) - cos ↑θ₁₂ * sin ↑θ₂₃ * cos ↑θ₁₃ ^ 2 -
    sin ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ * cexp (I * ↑δ₁₃)«2»θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝ⊢ cos ↑θ₂₃ * cos ↑θ₁₃ * cexp (I * ↑δ₁₃) =
  cos ↑θ₂₃ * cos ↑θ₁₃ * cexp (I * ↑δ₁₃) * cos ↑θ₁₂ ^ 2 + cos ↑θ₂₃ * cos ↑θ₁₃ * cexp (I * ↑δ₁₃) * (1 - cos ↑θ₁₂ ^ 2)
    ringAll goals completed! 🐙

A CKM matrix which has rows equal to that of a standard parameterisation is equal to that standard parameterisation.


lemma eq_rows (U : CKMMatrix) {θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ} (hu : [U]u = [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]u)
    (hc : [U]c = [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]c) (hU : [U]t = conj [U]u ⨯₃ conj [U]c) :
    U = standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃ := byU:CKMMatrixθ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝhu:[U]u = [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]uhc:[U]c = [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]chU:[U]t = (crossProduct ((starRingEnd (Fin 3 → ℂ)) [U]u)) ((starRingEnd (Fin 3 → ℂ)) [U]c)⊢ U = standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃
  apply ext_Rows hu hcU:CKMMatrixθ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝhu:[U]u = [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]uhc:[U]c = [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]chU:[U]t = (crossProduct ((starRingEnd (Fin 3 → ℂ)) [U]u)) ((starRingEnd (Fin 3 → ℂ)) [U]c)⊢ [U]t = [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]t
  rw [hU,U:CKMMatrixθ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝhu:[U]u = [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]uhc:[U]c = [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]chU:[U]t = (crossProduct ((starRingEnd (Fin 3 → ℂ)) [U]u)) ((starRingEnd (Fin 3 → ℂ)) [U]c)⊢ (crossProduct ((starRingEnd (Fin 3 → ℂ)) [U]u)) ((starRingEnd (Fin 3 → ℂ)) [U]c) = [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]tAll goals completed! 🐙 cross_product_t,U:CKMMatrixθ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝhu:[U]u = [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]uhc:[U]c = [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]chU:[U]t = (crossProduct ((starRingEnd (Fin 3 → ℂ)) [U]u)) ((starRingEnd (Fin 3 → ℂ)) [U]c)⊢ (crossProduct ((starRingEnd (Fin 3 → ℂ)) [U]u)) ((starRingEnd (Fin 3 → ℂ)) [U]c) =
  (crossProduct ((starRingEnd (Fin 3 → ℂ)) [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]u))
    ((starRingEnd (Fin 3 → ℂ)) [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]c)All goals completed! 🐙 hu,U:CKMMatrixθ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝhu:[U]u = [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]uhc:[U]c = [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]chU:[U]t = (crossProduct ((starRingEnd (Fin 3 → ℂ)) [U]u)) ((starRingEnd (Fin 3 → ℂ)) [U]c)⊢ (crossProduct ((starRingEnd (Fin 3 → ℂ)) [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]u)) ((starRingEnd (Fin 3 → ℂ)) [U]c) =
  (crossProduct ((starRingEnd (Fin 3 → ℂ)) [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]u))
    ((starRingEnd (Fin 3 → ℂ)) [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]c)All goals completed! 🐙 hcU:CKMMatrixθ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝhu:[U]u = [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]uhc:[U]c = [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]chU:[U]t = (crossProduct ((starRingEnd (Fin 3 → ℂ)) [U]u)) ((starRingEnd (Fin 3 → ℂ)) [U]c)⊢ (crossProduct ((starRingEnd (Fin 3 → ℂ)) [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]u))
    ((starRingEnd (Fin 3 → ℂ)) [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]c) =
  (crossProduct ((starRingEnd (Fin 3 → ℂ)) [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]u))
    ((starRingEnd (Fin 3 → ℂ)) [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]c)All goals completed! 🐙]All goals completed! 🐙

Two standard parameterisations of CKM matrices are the same matrix if they have the same angles and the exponential of their faces is equal.


lemma eq_exp_of_phases (θ₁₂ θ₁₃ θ₂₃ δ₁₃ δ₁₃' : ℝ) (h : cexp (δ₁₃ * I) = cexp (δ₁₃' * I)) :
    standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃ = standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃' := byθ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝδ₁₃':ℝh:cexp (↑δ₁₃ * I) = cexp (↑δ₁₃' * I)⊢ standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃ = standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃'
  have he : cexp (I * ↑δ₁₃) = cexp (I * ↑δ₁₃') := by rw [mul_comm,θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝδ₁₃':ℝh:cexp (↑δ₁₃ * I) = cexp (↑δ₁₃' * I)⊢ cexp (↑δ₁₃ * I) = cexp (I * ↑δ₁₃')θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝδ₁₃':ℝh:cexp (↑δ₁₃ * I) = cexp (↑δ₁₃' * I)he:cexp (I * ↑δ₁₃) = cexp (I * ↑δ₁₃')⊢ standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃ = standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃' h,θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝδ₁₃':ℝh:cexp (↑δ₁₃ * I) = cexp (↑δ₁₃' * I)⊢ cexp (↑δ₁₃' * I) = cexp (I * ↑δ₁₃')θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝδ₁₃':ℝh:cexp (↑δ₁₃ * I) = cexp (↑δ₁₃' * I)he:cexp (I * ↑δ₁₃) = cexp (I * ↑δ₁₃')⊢ standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃ = standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃' mul_commθ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝδ₁₃':ℝh:cexp (↑δ₁₃ * I) = cexp (↑δ₁₃' * I)⊢ cexp (I * ↑δ₁₃') = cexp (I * ↑δ₁₃')θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝδ₁₃':ℝh:cexp (↑δ₁₃ * I) = cexp (↑δ₁₃' * I)he:cexp (I * ↑δ₁₃) = cexp (I * ↑δ₁₃')⊢ standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃ = standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃']θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝδ₁₃':ℝh:cexp (↑δ₁₃ * I) = cexp (↑δ₁₃' * I)he:cexp (I * ↑δ₁₃) = cexp (I * ↑δ₁₃')⊢ standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃ = standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃'θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝδ₁₃':ℝh:cexp (↑δ₁₃ * I) = cexp (↑δ₁₃' * I)he:cexp (I * ↑δ₁₃) = cexp (I * ↑δ₁₃')⊢ standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃ = standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃'
  simp only [standParam, standParamAsMatrix, ofReal_cos, ofReal_sin, neg_mul]θ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝδ₁₃':ℝh:cexp (↑δ₁₃ * I) = cexp (↑δ₁₃' * I)he:cexp (I * ↑δ₁₃) = cexp (I * ↑δ₁₃')⊢ ⟨![![cos ↑θ₁₂ * cos ↑θ₁₃, sin ↑θ₁₂ * cos ↑θ₁₃, sin ↑θ₁₃ * cexp (-(I * ↑δ₁₃))],
      ![-(sin ↑θ₁₂ * cos ↑θ₂₃) - cos ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃ * cexp (I * ↑δ₁₃),
        cos ↑θ₁₂ * cos ↑θ₂₃ - sin ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃ * cexp (I * ↑δ₁₃), sin ↑θ₂₃ * cos ↑θ₁₃],
      ![sin ↑θ₁₂ * sin ↑θ₂₃ - cos ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ * cexp (I * ↑δ₁₃),
        -(cos ↑θ₁₂ * sin ↑θ₂₃) - sin ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ * cexp (I * ↑δ₁₃), cos ↑θ₂₃ * cos ↑θ₁₃]],
    ⋯⟩ =
  ⟨![![cos ↑θ₁₂ * cos ↑θ₁₃, sin ↑θ₁₂ * cos ↑θ₁₃, sin ↑θ₁₃ * cexp (-(I * ↑δ₁₃'))],
      ![-(sin ↑θ₁₂ * cos ↑θ₂₃) - cos ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃ * cexp (I * ↑δ₁₃'),
        cos ↑θ₁₂ * cos ↑θ₂₃ - sin ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃ * cexp (I * ↑δ₁₃'), sin ↑θ₂₃ * cos ↑θ₁₃],
      ![sin ↑θ₁₂ * sin ↑θ₂₃ - cos ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ * cexp (I * ↑δ₁₃'),
        -(cos ↑θ₁₂ * sin ↑θ₂₃) - sin ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ * cexp (I * ↑δ₁₃'), cos ↑θ₂₃ * cos ↑θ₁₃]],
    ⋯⟩
  apply CKMMatrix_extθ₁₂:ℝθ₁₃:ℝθ₂₃:ℝδ₁₃:ℝδ₁₃':ℝh:cexp (↑δ₁₃ * I) = cexp (↑δ₁₃' * I)he:cexp (I * ↑δ₁₃) = cexp (I * ↑δ₁₃')⊢ ↑⟨![![cos ↑θ₁₂ * cos ↑θ₁₃, sin ↑θ₁₂ * cos ↑θ₁₃, sin ↑θ₁₃ * cexp (-(I * ↑δ₁₃))],
        ![-(sin ↑θ₁₂ * cos ↑θ₂₃) - cos ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃ * cexp (I * ↑δ₁₃),
          cos ↑θ₁₂ * cos ↑θ₂₃ - sin ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃ * cexp (I * ↑δ₁₃), sin ↑θ₂₃ * cos ↑θ₁₃],
        ![sin ↑θ₁₂ * sin ↑θ₂₃ - cos ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ * cexp (I * ↑δ₁₃),
          -(cos ↑θ₁₂ * sin ↑θ₂₃) - sin ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ * cexp (I * ↑δ₁₃), cos ↑θ₂₃ * cos ↑θ₁₃]],
      ⋯⟩ =
  ↑⟨![![cos ↑θ₁₂ * cos ↑θ₁₃, sin ↑θ₁₂ * cos ↑θ₁₃, sin ↑θ₁₃ * cexp (-(I * ↑δ₁₃'))],
        ![-(sin ↑θ₁₂ * cos ↑θ₂₃) - cos ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃ * cexp (I * ↑δ₁₃'),
          cos ↑θ₁₂ * cos ↑θ₂₃ - sin ↑θ₁₂ * sin ↑θ₁₃ * sin ↑θ₂₃ * cexp (I * ↑δ₁₃'), sin ↑θ₂₃ * cos ↑θ₁₃],
        ![sin ↑θ₁₂ * sin ↑θ₂₃ - cos ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ * cexp (I * ↑δ₁₃'),
          -(cos ↑θ₁₂ * sin ↑θ₂₃) - sin ↑θ₁₂ * sin ↑θ₁₃ * cos ↑θ₂₃ * cexp (I * ↑δ₁₃'), cos ↑θ₂₃ * cos ↑θ₁₃]],
      ⋯⟩
  simp only [exp_neg, he]All goals completed! 🐙