1. Physlib
  2. Particles
  3. FlavorPhysics
  4. CKMMatrix
  5. Relations
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

Relations for the CKM Matrix

This file contains a collection of relations and properties between the elements of the CKM matrix.

@[expose] public section

The absolute value squared of any row of a CKM matrix is 1, in terms of Vabs.

i:Fin 3V:CKMMatrixhV:↑V * star ↑V = 1ht:↑(‖↑V i 0‖ ^ 2) + ↑(‖↑V i 1‖ ^ 2) + ↑(‖↑V i 2‖ ^ 2) = 1⊢ ↑(VAbs i 0 (Quot.mk (⇑CKMMatrixSetoid) V) ^ 2 + VAbs i 1 (Quot.mk (⇑CKMMatrixSetoid) V) ^ 2 + VAbs i 2 (Quot.mk (⇑CKMMatrixSetoid) V) ^ 2) = ↑1 i:Fin 3V:CKMMatrixht:↑‖↑V i 0‖ ^ 2 + ↑‖↑V i 1‖ ^ 2 + ↑‖↑V i 2‖ ^ 2 = 1⊢ ↑(VAbs i 0 (Quot.mk (⇑CKMMatrixSetoid) V)) ^ 2 + ↑(VAbs i 1 (Quot.mk (⇑CKMMatrixSetoid) V)) ^ 2 + ↑(VAbs i 2 (Quot.mk (⇑CKMMatrixSetoid) V)) ^ 2 = 1 All goals completed! 🐙

The absolute value squared of the first row of a CKM matrix is 1, in terms of norm.

lemma fst_row_normalized_abs (V : CKMMatrix) : norm [V]ud ^ 2 + norm [V]us ^ 2 + norm [V]ub ^ 2 = 1 := VAbs_sum_sq_row_eq_one ⟦V⟧ 0

The absolute value squared of the second row of a CKM matrix is 1, in terms of norm.

lemma snd_row_normalized_abs (V : CKMMatrix) : norm [V]cd ^ 2 + norm [V]cs ^ 2 + norm [V]cb ^ 2 = 1 := VAbs_sum_sq_row_eq_one ⟦V⟧ 1

The absolute value squared of the third row of a CKM matrix is 1, in terms of norm.

lemma thd_row_normalized_abs (V : CKMMatrix) : norm [V]td ^ 2 + norm [V]ts ^ 2 + norm [V]tb ^ 2 = 1 := VAbs_sum_sq_row_eq_one ⟦V⟧ 2

The absolute value squared of the first row of a CKM matrix is 1, in terms of nomSq.

V:CKMMatrix⊢ ‖↑V 0 0‖ ^ 2 + ‖↑V 0 1‖ ^ 2 + ‖↑V 0 2‖ ^ 2 = 1 All goals completed! 🐙

The absolute value squared of the second row of a CKM matrix is 1, in terms of nomSq.

V:CKMMatrix⊢ ‖↑V 1 0‖ ^ 2 + ‖↑V 1 1‖ ^ 2 + ‖↑V 1 2‖ ^ 2 = 1 All goals completed! 🐙

The absolute value squared of the third row of a CKM matrix is 1, in terms of nomSq.

V:CKMMatrix⊢ ‖↑V 2 0‖ ^ 2 + ‖↑V 2 1‖ ^ 2 + ‖↑V 2 2‖ ^ 2 = 1 All goals completed! 🐙
lemma normSq_Vud_plus_normSq_Vus (V : CKMMatrix) : normSq [V]ud + normSq [V]us = 1 - normSq [V]ub := V:CKMMatrix⊢ normSq (↑V 0 0) + normSq (↑V 0 1) = 1 - normSq (↑V 0 2) All goals completed! 🐙lemma VudAbs_sq_add_VusAbs_sq : VudAbs V ^ 2 + VusAbs V ^2 = 1 - VubAbs V ^2 := V:Quotient CKMMatrixSetoid⊢ VudAbs V ^ 2 + VusAbs V ^ 2 = 1 - VubAbs V ^ 2 All goals completed! 🐙V:CKMMatrixh2:‖↑V 0 2‖ = -1h:¬-1 = 1hn:↑V 0 0 = 0 ∧ ↑V 0 1 = 0h1:0 ≤ -1⊢ False V:CKMMatrixh2:‖↑V 0 2‖ = -1h:¬-1 = 1hn:↑V 0 0 = 0 ∧ ↑V 0 1 = 0h1:0 ≤ -1⊢ ¬0 ≤ -1 All goals completed! 🐙V:CKMMatrixhb:‖↑V 0 2‖ ≠ 1hn:1 - ‖↑V 0 2‖ ^ 2 = 0h2✝:‖↑V 0 2‖ = -1h3:0 ≤ -1h2:¬0 ≤ -1⊢ False All goals completed! 🐙V✝:Quotient CKMMatrixSetoidV:CKMMatrixhV:↑V 0 0 ≠ 0 ∨ ↑V 0 1 ≠ 0⊢ VudAbs (Quot.mk (⇑CKMMatrixSetoid) V) ^ 2 + VusAbs (Quot.mk (⇑CKMMatrixSetoid) V) ^ 2 ≠ 0 V✝:Quotient CKMMatrixSetoidV:CKMMatrixhV:↑V 0 0 ≠ 0 ∨ ↑V 0 1 ≠ 0this:normSq (↑V 0 0) + normSq (↑V 0 1) ≠ 0⊢ VudAbs (Quot.mk (⇑CKMMatrixSetoid) V) ^ 2 + VusAbs (Quot.mk (⇑CKMMatrixSetoid) V) ^ 2 ≠ 0 V✝:Quotient CKMMatrixSetoidV:CKMMatrixhV:¬↑V 0 0 = 0 ∨ ¬↑V 0 1 = 0this:¬‖↑V 0 0‖ ^ 2 + ‖↑V 0 1‖ ^ 2 = 0⊢ ¬VAbs 0 0 (Quot.mk (⇑CKMMatrixSetoid) V) ^ 2 + VAbs 0 1 (Quot.mk (⇑CKMMatrixSetoid) V) ^ 2 = 0 All goals completed! 🐙V✝:Quotient CKMMatrixSetoidV:CKMMatrixhV:↑V 0 0 ≠ 0 ∨ ↑V 0 1 ≠ 0⊢ VudAbs (Quot.mk (⇑CKMMatrixSetoid) V) ^ 2 + VusAbs (Quot.mk (⇑CKMMatrixSetoid) V) ^ 2 ≠ 0 V✝:Quotient CKMMatrixSetoidV:CKMMatrixhV:↑V 0 0 ≠ 0 ∨ ↑V 0 1 ≠ 0this:normSq (↑V 0 0) + normSq (↑V 0 1) ≠ 0⊢ VudAbs (Quot.mk (⇑CKMMatrixSetoid) V) ^ 2 + VusAbs (Quot.mk (⇑CKMMatrixSetoid) V) ^ 2 ≠ 0 V✝:Quotient CKMMatrixSetoidV:CKMMatrixhV:¬↑V 0 0 = 0 ∨ ¬↑V 0 1 = 0this:¬‖↑V 0 0‖ ^ 2 + ‖↑V 0 1‖ ^ 2 = 0⊢ ¬VAbs 0 0 (Quot.mk (⇑CKMMatrixSetoid) V) ^ 2 + VAbs 0 1 (Quot.mk (⇑CKMMatrixSetoid) V) ^ 2 = 0 All goals completed! 🐙V:CKMMatrixhb:↑V 0 0 ≠ 0 ∨ ↑V 0 1 ≠ 0h1:¬↑(normSq (↑V 0 0) + normSq (↑V 0 1)) = ↑0⊢ ↑(normSq (↑V 0 0)) + ↑(normSq (↑V 0 1)) ≠ 0 All goals completed! 🐙V:CKMMatrixhb:↑V 0 0 ≠ 0 ∨ ↑V 0 1 ≠ 0h1:↑(‖↑V 0 0‖ ^ 2) + ↑(‖↑V 0 1‖ ^ 2) ≠ 0⊢ ↑(VudAbs ⟦V⟧) * ↑(VudAbs ⟦V⟧) + ↑(VusAbs ⟦V⟧) * ↑(VusAbs ⟦V⟧) ≠ 0 V:CKMMatrixhb:↑V 0 0 ≠ 0 ∨ ↑V 0 1 ≠ 0h1:¬↑‖↑V 0 0‖ * ↑‖↑V 0 0‖ + ↑‖↑V 0 1‖ * ↑‖↑V 0 1‖ = 0⊢ ↑(VudAbs ⟦V⟧) * ↑(VudAbs ⟦V⟧) + ↑(VusAbs ⟦V⟧) * ↑(VusAbs ⟦V⟧) ≠ 0 All goals completed! 🐙V:CKMMatrixhV:↑V * star ↑V = 1⊢ ↑V 1 0 * (starRingEnd ℂ) (↑V 0 0) + ↑V 1 1 * (starRingEnd ℂ) (↑V 0 1) + ↑V 1 2 * (starRingEnd ℂ) (↑V 0 2) = 0 V:CKMMatrixhV:↑V * star ↑V = 1ht:(↑V * star ↑V) 1 0 = 1 1 0⊢ ↑V 1 0 * (starRingEnd ℂ) (↑V 0 0) + ↑V 1 1 * (starRingEnd ℂ) (↑V 0 1) + ↑V 1 2 * (starRingEnd ℂ) (↑V 0 2) = 0 V:CKMMatrixhV:↑V * star ↑V = 1ht:↑V 1 0 * (starRingEnd ℂ) (↑V 0 0) + ↑V 1 1 * (starRingEnd ℂ) (↑V 0 1) + ↑V 1 2 * (starRingEnd ℂ) (↑V 0 2) = 0⊢ ↑V 1 0 * (starRingEnd ℂ) (↑V 0 0) + ↑V 1 1 * (starRingEnd ℂ) (↑V 0 1) + ↑V 1 2 * (starRingEnd ℂ) (↑V 0 2) = 0 All goals completed! 🐙V:CKMMatrixhV:↑V * star ↑V = 1⊢ ↑V 2 0 * (starRingEnd ℂ) (↑V 0 0) + ↑V 2 1 * (starRingEnd ℂ) (↑V 0 1) + ↑V 2 2 * (starRingEnd ℂ) (↑V 0 2) = 0 V:CKMMatrixhV:↑V * star ↑V = 1ht:(↑V * star ↑V) 2 0 = 1 2 0⊢ ↑V 2 0 * (starRingEnd ℂ) (↑V 0 0) + ↑V 2 1 * (starRingEnd ℂ) (↑V 0 1) + ↑V 2 2 * (starRingEnd ℂ) (↑V 0 2) = 0 V:CKMMatrixhV:↑V * star ↑V = 1ht:↑V 2 0 * (starRingEnd ℂ) (↑V 0 0) + ↑V 2 1 * (starRingEnd ℂ) (↑V 0 1) + ↑V 2 2 * (starRingEnd ℂ) (↑V 0 2) = 0⊢ ↑V 2 0 * (starRingEnd ℂ) (↑V 0 0) + ↑V 2 1 * (starRingEnd ℂ) (↑V 0 1) + ↑V 2 2 * (starRingEnd ℂ) (↑V 0 2) = 0 All goals completed! 🐙lemma Vcd_mul_conj_Vud (V : CKMMatrix) : [V]cd * conj [V]ud = -[V]cs * conj [V]us - [V]cb * conj [V]ub := V:CKMMatrix⊢ ↑V 1 0 * (starRingEnd ℂ) (↑V 0 0) = -↑V 1 1 * (starRingEnd ℂ) (↑V 0 1) - ↑V 1 2 * (starRingEnd ℂ) (↑V 0 2) All goals completed! 🐙lemma Vcs_mul_conj_Vus (V : CKMMatrix) : [V]cs * conj [V]us = - [V]cd * conj [V]ud - [V]cb * conj [V]ub := V:CKMMatrix⊢ ↑V 1 1 * (starRingEnd ℂ) (↑V 0 1) = -↑V 1 0 * (starRingEnd ℂ) (↑V 0 0) - ↑V 1 2 * (starRingEnd ℂ) (↑V 0 2) All goals completed! 🐙V:Quotient CKMMatrixSetoidi:Fin 3hV:VAbs i 2 V = 1h:VAbs i 0 V ^ 2 + VAbs i 1 V ^ 2 + 1 ^ 2 = 1⊢ VAbs i 0 V = 0 V:Quotient CKMMatrixSetoidi:Fin 3hV:VAbs i 2 V = 1h:VAbs i 0 V ^ 2 + VAbs i 1 V ^ 2 = 0⊢ VAbs i 0 V = 0 All goals completed! 🐙V:Quotient CKMMatrixSetoidi:Fin 3hV:VAbs i 2 V = 1h:VAbs i 0 V ^ 2 + VAbs i 1 V ^ 2 + 1 ^ 2 = 1⊢ VAbs i 1 V = 0 V:Quotient CKMMatrixSetoidi:Fin 3hV:VAbs i 2 V = 1h:VAbs i 0 V ^ 2 + VAbs i 1 V ^ 2 = 0⊢ VAbs i 1 V = 0 All goals completed! 🐙V:CKMMatrixτ:ℝhτ:[V]t = cexp (↑τ * I) • (crossProduct ((starRingEnd (Fin 3 → ℂ)) [V]u)) ((starRingEnd (Fin 3 → ℂ)) [V]c)h1✝:↑V 2 2 = cexp (↑τ * I) * ((starRingEnd ℂ) (↑V 0 0) * (starRingEnd ℂ) (↑V 1 1) - (starRingEnd ℂ) (↑V 0 1) * (starRingEnd ℂ) (↑V 1 0))h1:(starRingEnd ℂ) (↑V 2 2) = (starRingEnd ℂ) (cexp (↑τ * I)) * (↑V 0 0 * ↑V 1 1 - ↑V 0 1 * ↑V 1 0)⊢ (starRingEnd ℂ) (cexp (↑τ * I)) * (↑V 0 0 * ↑V 1 1 - ↑V 0 1 * ↑V 1 0) = cexp (-↑τ * I) * (↑V 1 1 * ↑V 0 0 - ↑V 0 1 * ↑V 1 0) V:CKMMatrixτ:ℝhτ:[V]t = cexp (↑τ * I) • (crossProduct ((starRingEnd (Fin 3 → ℂ)) [V]u)) ((starRingEnd (Fin 3 → ℂ)) [V]c)h1✝:↑V 2 2 = cexp (↑τ * I) * ((starRingEnd ℂ) (↑V 0 0) * (starRingEnd ℂ) (↑V 1 1) - (starRingEnd ℂ) (↑V 0 1) * (starRingEnd ℂ) (↑V 1 0))h1:(starRingEnd ℂ) (↑V 2 2) = (starRingEnd ℂ) (cexp (↑τ * I)) * (↑V 0 0 * ↑V 1 1 - ↑V 0 1 * ↑V 1 0)⊢ cexp (-(↑τ * I)) * (↑V 0 0 * ↑V 1 1 - ↑V 0 1 * ↑V 1 0) = cexp (-(↑τ * I)) * (↑V 1 1 * ↑V 0 0 - ↑V 0 1 * ↑V 1 0) V:CKMMatrixτ:ℝhτ:[V]t = cexp (↑τ * I) • (crossProduct ((starRingEnd (Fin 3 → ℂ)) [V]u)) ((starRingEnd (Fin 3 → ℂ)) [V]c)h1✝:↑V 2 2 = cexp (↑τ * I) * ((starRingEnd ℂ) (↑V 0 0) * (starRingEnd ℂ) (↑V 1 1) - (starRingEnd ℂ) (↑V 0 1) * (starRingEnd ℂ) (↑V 1 0))h1:(starRingEnd ℂ) (↑V 2 2) = (starRingEnd ℂ) (cexp (↑τ * I)) * (↑V 0 0 * ↑V 1 1 - ↑V 0 1 * ↑V 1 0)⊢ ↑V 0 0 * ↑V 1 1 = ↑V 1 1 * ↑V 0 0 All goals completed! 🐙V:CKMMatrixτ:ℝhτ:[V]t = cexp (↑τ * I) • (crossProduct ((starRingEnd (Fin 3 → ℂ)) [V]u)) ((starRingEnd (Fin 3 → ℂ)) [V]c)h2:(↑V 1 1 * ↑V 0 0 - ↑V 0 1 * ↑V 1 0) * (starRingEnd ℂ) (↑V 0 0) = ↑V 1 1 * ↑V 0 0 * (starRingEnd ℂ) (↑V 0 0) - ↑V 0 1 * (↑V 1 0 * (starRingEnd ℂ) (↑V 0 0))⊢ ↑V 1 1 * ↑V 0 0 * (starRingEnd ℂ) (↑V 0 0) - ↑V 0 1 * (-↑V 1 1 * (starRingEnd ℂ) (↑V 0 1) - ↑V 1 2 * (starRingEnd ℂ) (↑V 0 2)) = ↑V 1 1 * ((starRingEnd ℂ) (↑V 0 0) * ↑V 0 0 + (starRingEnd ℂ) (↑V 0 1) * ↑V 0 1) + ↑V 1 2 * (starRingEnd ℂ) (↑V 0 2) * ↑V 0 1 V:CKMMatrixτ:ℝhτ:[V]t = cexp (↑τ * I) • (crossProduct ((starRingEnd (Fin 3 → ℂ)) [V]u)) ((starRingEnd (Fin 3 → ℂ)) [V]c)h2:(↑V 1 1 * ↑V 0 0 - ↑V 0 1 * ↑V 1 0) * (starRingEnd ℂ) (↑V 0 0) = ↑V 1 1 * ↑V 0 0 * (starRingEnd ℂ) (↑V 0 0) - ↑V 0 1 * (↑V 1 0 * (starRingEnd ℂ) (↑V 0 0))⊢ ↑V 1 1 * ↑V 0 0 * (starRingEnd ℂ) (↑V 0 0) - ↑V 0 1 * (-(↑V 1 1 * (starRingEnd ℂ) (↑V 0 1)) - ↑V 1 2 * (starRingEnd ℂ) (↑V 0 2)) = ↑V 1 1 * ((starRingEnd ℂ) (↑V 0 0) * ↑V 0 0 + (starRingEnd ℂ) (↑V 0 1) * ↑V 0 1) + ↑V 1 2 * (starRingEnd ℂ) (↑V 0 2) * ↑V 0 1 All goals completed! 🐙V:CKMMatrixτ:ℝhτ:[V]t = cexp (↑τ * I) • (crossProduct ((starRingEnd (Fin 3 → ℂ)) [V]u)) ((starRingEnd (Fin 3 → ℂ)) [V]c)h2:(↑V 1 1 * ↑V 0 0 - ↑V 0 1 * ↑V 1 0) * (starRingEnd ℂ) (↑V 0 1) = ↑V 1 1 * (starRingEnd ℂ) (↑V 0 1) * ↑V 0 0 - ↑V 0 1 * ↑V 1 0 * (starRingEnd ℂ) (↑V 0 1)⊢ (-↑V 1 0 * (starRingEnd ℂ) (↑V 0 0) - ↑V 1 2 * (starRingEnd ℂ) (↑V 0 2)) * ↑V 0 0 - ↑V 0 1 * ↑V 1 0 * (starRingEnd ℂ) (↑V 0 1) = -(↑V 1 2 * (starRingEnd ℂ) (↑V 0 2) * ↑V 0 0) + -(↑V 1 0 * ((starRingEnd ℂ) (↑V 0 0) * ↑V 0 0 + (starRingEnd ℂ) (↑V 0 1) * ↑V 0 1)) V:CKMMatrixτ:ℝhτ:[V]t = cexp (↑τ * I) • (crossProduct ((starRingEnd (Fin 3 → ℂ)) [V]u)) ((starRingEnd (Fin 3 → ℂ)) [V]c)h2:(↑V 1 1 * ↑V 0 0 - ↑V 0 1 * ↑V 1 0) * (starRingEnd ℂ) (↑V 0 1) = ↑V 1 1 * (starRingEnd ℂ) (↑V 0 1) * ↑V 0 0 - ↑V 0 1 * ↑V 1 0 * (starRingEnd ℂ) (↑V 0 1)⊢ (-(↑V 1 0 * (starRingEnd ℂ) (↑V 0 0)) - ↑V 1 2 * (starRingEnd ℂ) (↑V 0 2)) * ↑V 0 0 - ↑V 0 1 * ↑V 1 0 * (starRingEnd ℂ) (↑V 0 1) = -(↑V 1 2 * (starRingEnd ℂ) (↑V 0 2) * ↑V 0 0) + -(↑V 1 0 * ((starRingEnd ℂ) (↑V 0 0) * ↑V 0 0 + (starRingEnd ℂ) (↑V 0 1) * ↑V 0 1)) All goals completed! 🐙V:CKMMatrixh:↑V 0 0 ≠ 0 ∨ ↑V 0 1 ≠ 0τ:ℝhτ:[V]t = cexp (↑τ * I) • (crossProduct ((starRingEnd (Fin 3 → ℂ)) [V]u)) ((starRingEnd (Fin 3 → ℂ)) [V]c)h1:↑(normSq (↑V 0 0)) + ↑(normSq (↑V 0 1)) ≠ 0⊢ ↑V 1 1 = (-(starRingEnd ℂ) (↑V 0 2) * ↑V 0 1 * ↑V 1 2 + (↑V 1 1 * (↑(normSq (↑V 0 0)) + ↑(normSq (↑V 0 1))) + ↑V 1 2 * (starRingEnd ℂ) (↑V 0 2) * ↑V 0 1)) / (↑(normSq (↑V 0 0)) + ↑(normSq (↑V 0 1))) V:CKMMatrixh:↑V 0 0 ≠ 0 ∨ ↑V 0 1 ≠ 0τ:ℝhτ:[V]t = cexp (↑τ * I) • (crossProduct ((starRingEnd (Fin 3 → ℂ)) [V]u)) ((starRingEnd (Fin 3 → ℂ)) [V]c)h1:↑(normSq (↑V 0 0)) + ↑(normSq (↑V 0 1)) ≠ 0⊢ ↑V 1 1 * (↑(normSq (↑V 0 0)) + ↑(normSq (↑V 0 1))) = -((starRingEnd ℂ) (↑V 0 2) * ↑V 0 1 * ↑V 1 2) + (↑V 1 1 * (↑(normSq (↑V 0 0)) + ↑(normSq (↑V 0 1))) + (starRingEnd ℂ) (↑V 0 2) * ↑V 0 1 * ↑V 1 2) All goals completed! 🐙V:CKMMatrixh:↑V 0 0 ≠ 0 ∨ ↑V 0 1 ≠ 0τ:ℝhτ:[V]t = cexp (↑τ * I) • (crossProduct ((starRingEnd (Fin 3 → ℂ)) [V]u)) ((starRingEnd (Fin 3 → ℂ)) [V]c)h1:↑(normSq (↑V 0 0)) + ↑(normSq (↑V 0 1)) ≠ 0⊢ ↑V 1 0 = -((starRingEnd ℂ) (↑V 0 2) * ↑V 0 0 * ↑V 1 2 + -(↑V 1 0 * (↑(normSq (↑V 0 0)) + ↑(normSq (↑V 0 1))) + ↑V 1 2 * (starRingEnd ℂ) (↑V 0 2) * ↑V 0 0)) / (↑(normSq (↑V 0 0)) + ↑(normSq (↑V 0 1))) V:CKMMatrixh:↑V 0 0 ≠ 0 ∨ ↑V 0 1 ≠ 0τ:ℝhτ:[V]t = cexp (↑τ * I) • (crossProduct ((starRingEnd (Fin 3 → ℂ)) [V]u)) ((starRingEnd (Fin 3 → ℂ)) [V]c)h1:↑(normSq (↑V 0 0)) + ↑(normSq (↑V 0 1)) ≠ 0⊢ ↑V 1 0 * (↑(normSq (↑V 0 0)) + ↑(normSq (↑V 0 1))) = -((starRingEnd ℂ) (↑V 0 2) * ↑V 0 0 * ↑V 1 2 + -(↑V 1 0 * (↑(normSq (↑V 0 0)) + ↑(normSq (↑V 0 1))) + (starRingEnd ℂ) (↑V 0 2) * ↑V 0 0 * ↑V 1 2)) All goals completed! 🐙i:Fin 3j:Fin 3V✝:Quotient CKMMatrixSetoidV:CKMMatrixhV:Quot.mk (⇑CKMMatrixSetoid) V = V✝⊢ 0 ≤ VAbs i j (Quot.mk (⇑CKMMatrixSetoid) V) All goals completed! 🐙lemma VAbs_leq_one (i j : Fin 3) (V : Quotient CKMMatrixSetoid) : VAbs i j V ≤ 1 := i:Fin 3j:Fin 3V:Quotient CKMMatrixSetoid⊢ VAbs i j V ≤ 1 i:Fin 3j:Fin 3V:Quotient CKMMatrixSetoidh:VAbs i 0 V ^ 2 + VAbs i 1 V ^ 2 + VAbs i 2 V ^ 2 = 1⊢ VAbs i j V ≤ 1 i:Fin 3V:Quotient CKMMatrixSetoidh:VAbs i 0 V ^ 2 + VAbs i 1 V ^ 2 + VAbs i 2 V ^ 2 = 1⊢ VAbs i ((fun i => i) ⟨0, ⋯⟩) V ≤ 1i:Fin 3V:Quotient CKMMatrixSetoidh:VAbs i 0 V ^ 2 + VAbs i 1 V ^ 2 + VAbs i 2 V ^ 2 = 1⊢ VAbs i ((fun i => i) ⟨1, ⋯⟩) V ≤ 1i:Fin 3V:Quotient CKMMatrixSetoidh:VAbs i 0 V ^ 2 + VAbs i 1 V ^ 2 + VAbs i 2 V ^ 2 = 1⊢ VAbs i ((fun i => i) ⟨2, ⋯⟩) V ≤ 1 i:Fin 3V:Quotient CKMMatrixSetoidh:VAbs i 0 V ^ 2 + VAbs i 1 V ^ 2 + VAbs i 2 V ^ 2 = 1⊢ VAbs i ((fun i => i) ⟨0, ⋯⟩) V ≤ 1 i:Fin 3V:Quotient CKMMatrixSetoidh:VAbs i 0 V ^ 2 + VAbs i 1 V ^ 2 + VAbs i 2 V ^ 2 = 1⊢ VAbs i 0 V ≤ 1 All goals completed! 🐙 i:Fin 3V:Quotient CKMMatrixSetoidh:VAbs i 0 V ^ 2 + VAbs i 1 V ^ 2 + VAbs i 2 V ^ 2 = 1⊢ VAbs i ((fun i => i) ⟨1, ⋯⟩) V ≤ 1 i:Fin 3V:Quotient CKMMatrixSetoidh:VAbs i 0 V ^ 2 + VAbs i 1 V ^ 2 + VAbs i 2 V ^ 2 = 1⊢ VAbs i 1 V ≤ 1 All goals completed! 🐙 i:Fin 3V:Quotient CKMMatrixSetoidh:VAbs i 0 V ^ 2 + VAbs i 1 V ^ 2 + VAbs i 2 V ^ 2 = 1⊢ VAbs i ((fun i => i) ⟨2, ⋯⟩) V ≤ 1 i:Fin 3V:Quotient CKMMatrixSetoidh:VAbs i 0 V ^ 2 + VAbs i 1 V ^ 2 + VAbs i 2 V ^ 2 = 1⊢ VAbs i 2 V ≤ 1 All goals completed! 🐙i:Fin 3V:CKMMatrixhV:star ↑V * ↑V = 1ht:↑(‖↑V 0 i‖ ^ 2) + ↑(‖↑V 1 i‖ ^ 2) + ↑(‖↑V 2 i‖ ^ 2) = 1⊢ ↑(VAbs 0 i (Quot.mk (⇑CKMMatrixSetoid) V) ^ 2 + VAbs 1 i (Quot.mk (⇑CKMMatrixSetoid) V) ^ 2 + VAbs 2 i (Quot.mk (⇑CKMMatrixSetoid) V) ^ 2) = ↑1 i:Fin 3V:CKMMatrixht:↑‖↑V 0 i‖ ^ 2 + ↑‖↑V 1 i‖ ^ 2 + ↑‖↑V 2 i‖ ^ 2 = 1⊢ ↑(VAbs 0 i (Quot.mk (⇑CKMMatrixSetoid) V)) ^ 2 + ↑(VAbs 1 i (Quot.mk (⇑CKMMatrixSetoid) V)) ^ 2 + ↑(VAbs 2 i (Quot.mk (⇑CKMMatrixSetoid) V)) ^ 2 = 1 All goals completed! 🐙lemma thd_col_normalized_abs (V : CKMMatrix) : norm [V]ub ^ 2 + norm [V]cb ^ 2 + norm [V]tb ^ 2 = 1 := V:CKMMatrix⊢ ‖↑V 0 2‖ ^ 2 + ‖↑V 1 2‖ ^ 2 + ‖↑V 2 2‖ ^ 2 = 1 V:CKMMatrixh1:VAbs 0 2 ⟦V⟧ ^ 2 + VAbs 1 2 ⟦V⟧ ^ 2 + VAbs 2 2 ⟦V⟧ ^ 2 = 1⊢ ‖↑V 0 2‖ ^ 2 + ‖↑V 1 2‖ ^ 2 + ‖↑V 2 2‖ ^ 2 = 1 V:CKMMatrixh1:‖↑V 0 2‖ ^ 2 + ‖↑V 1 2‖ ^ 2 + ‖↑V 2 2‖ ^ 2 = 1⊢ ‖↑V 0 2‖ ^ 2 + ‖↑V 1 2‖ ^ 2 + ‖↑V 2 2‖ ^ 2 = 1 All goals completed! 🐙V:CKMMatrixh1:normSq (↑V 0 2) + normSq (↑V 1 2) + normSq (↑V 2 2) = 1⊢ normSq (↑V 0 2) + normSq (↑V 1 2) + normSq (↑V 2 2) = 1 All goals completed! 🐙V:CKMMatrixh:↑V 0 0 = 0 ∧ ↑V 0 1 = 0h1:‖↑V 1 2‖ ^ 2 = 0 ∧ ‖↑V 2 2‖ ^ 2 = 0⊢ ↑V 1 2 = 0 V:CKMMatrixh:↑V 0 0 = 0 ∧ ↑V 0 1 = 0h1:↑V 1 2 = 0 ∧ ↑V 2 2 = 0⊢ ↑V 1 2 = 0 All goals completed! 🐙V:CKMMatrixha:↑V 0 0 = 0 ∧ ↑V 0 1 = 0h1✝:‖↑V 1 0‖ ^ 2 + ‖↑V 1 1‖ ^ 2 + ‖↑V 1 2‖ ^ 2 = 1h1:VAbs 1 0 ⟦V⟧ ≤ 1h0:0 ≤ VAbs 1 0 ⟦V⟧hn:-1 ≤ 0⊢ -1 ≤ VAbs 1 0 ⟦V⟧ All goals completed! 🐙 V:CKMMatrixha:¬(↑V 0 0 ≠ 0 ∨ ↑V 0 1 ≠ 0)h1:‖↑V 1 0‖ ^ 2 + ‖↑V 1 1‖ ^ 2 + ‖↑V 1 2‖ ^ 2 = 1⊢ 0 ≤ VcsAbs ⟦V⟧ All goals completed! 🐙lemma VcbAbs_sq_add_VtbAbs_sq (V : Quotient CKMMatrixSetoid) : VcbAbs V ^ 2 + VtbAbs V ^ 2 = 1 - VubAbs V ^2 := V:Quotient CKMMatrixSetoid⊢ VcbAbs V ^ 2 + VtbAbs V ^ 2 = 1 - VubAbs V ^ 2 All goals completed! 🐙V:CKMMatrixh:¬-1 = 1hn:↑V 1 2 = 0 ∧ ↑V 2 2 = 0h2✝:‖↑V 0 2‖ = -1h1:1 ≤ 0h2:¬1 ≤ 0⊢ False All goals completed! 🐙V:Quotient CKMMatrixSetoidi:Fin 3hV:VAbs 0 i V = 1h:1 ^ 2 + VAbs 1 i V ^ 2 + VAbs 2 i V ^ 2 = 1⊢ VAbs 1 i V = 0 V:Quotient CKMMatrixSetoidi:Fin 3hV:VAbs 0 i V = 1h:1 + VAbs 1 i V ^ 2 + VAbs 2 i V ^ 2 = 1⊢ VAbs 1 i V = 0 All goals completed! 🐙V:Quotient CKMMatrixSetoidi:Fin 3hV:VAbs 0 i V = 1h:1 ^ 2 + VAbs 1 i V ^ 2 + VAbs 2 i V ^ 2 = 1⊢ VAbs 2 i V = 0 V:Quotient CKMMatrixSetoidi:Fin 3hV:VAbs 0 i V = 1h:1 + VAbs 1 i V ^ 2 + VAbs 2 i V ^ 2 = 1⊢ VAbs 2 i V = 0 All goals completed! 🐙