FormalConjectures.OpenQuantumProblems.«23»

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

Open Quantum Problem 23: SIC-POVMs

Mathematical problem

The OQP page presents three increasingly strong formulations of this problem. In this file we formalize the first one, closest to the physics terminology: existence of a symmetric informationally complete POVM in every finite dimension.

A SIC-POVM in dimension $d$ can be represented by a family of $d^2$ normalized vectors in $\mathbb{C}^d$ whose pairwise squared overlaps are all equal to $(d + 1)^{-1}$. We encode such a family as a map Fin (d ^ 2) → StateVector d.

Background

SIC-POVMs are a basic structure in finite-dimensional quantum information. They are closely related to equiangular lines, tight frames, quantum state reconstruction, and finite-dimensional measurement theory. The open problem asks whether such families exist in every dimension.

What this file formalizes

This file formalizes the existence problem for symmetric informationally complete POVMs through the predicate HasSICPOVM d.

More precisely, it contains the following layers.

Core API

The main definitions formalized in this file are:

StateVector d: a state vector in ℂ^d;

mkStateVector: constructor from coordinates in the computational basis;

IsNormalized ψ: normalization predicate for a state vector;

overlapSq φ ψ: squared magnitude of the inner-product overlap;

HasConstantOverlapSq c Φ: constant pairwise squared-overlap condition;

sicOverlapSq d: the SIC overlap value (d + 1)⁻¹;

IsSICFamily d Φ: the predicate that a family of d^2 vectors in ℂ^d is a SIC family;

HasSICPOVM d: existence of a SIC family in dimension d.

In addition, the file includes explicit witness families and convenient constructors used in the low-dimensional benchmark cases:

vec2, vec3;

qubitSICFamily;

hesseFamily;

bb84Family.

Complete open conjecture

The main open theorem is:

sicPOVMs, expressing the conjecture that for every d ≥ 1, there exists a SIC-POVM in dimension d.

Special cases

The file also isolates several special cases:

solved low-dimensional benchmark cases: hasSICPOVM_zero, hasSICPOVM_one, hasSICPOVM_two, hasSICPOVM_three;

a negative benchmark result: bb84Family_not_isSICFamily, showing that the BB84 family in dimension 2 does not form a SIC family;

selected open benchmark dimensions: hasSICPOVM_56, hasSICPOVM_58, hasSICPOVM_59, hasSICPOVM_60, hasSICPOVM_64, hasSICPOVM_68, hasSICPOVM_69, hasSICPOVM_70, hasSICPOVM_71, hasSICPOVM_72, hasSICPOVM_75.

Test lemmas

The file includes the following test lemmas and benchmark-support statements:

hasConstantOverlapSq_singleton;

sicOverlapSq_one, sicOverlapSq_two, sicOverlapSq_three, sicOverlapSq_pos;

isSICFamily_singleton_iff, isSICFamily_one_of_normalized;

qubitSICFamily_normalized, qubitSICFamily_pairwise;

hesseFamily_normalized, hesseFamily_pairwise;

bb84Family_normalized.

At present, these @[category test, AMS 15 47 81] results are included with placeholder proofs by sorry; they are intended to be proved in the next PR.

References

Primary source list entry:

IQOQI Vienna Open Quantum Problems, problem 23: https://oqp.iqoqi.oeaw.ac.at/sic-povms-and-zauners-conjecture

Formal Conjectures issue #1823: https://github.com/google-deepmind/formal-conjectures/issues/1823

Foundational references

J. M. Renes, R. Blume-Kohout, A. J. Scott, and M. C. Caves, Symmetric informationally complete quantum measurements, J. Math. Phys. 45, 2171-2180 (2004), arXiv:quant-ph/0310075.

G. Zauner, Quantum Designs: Foundations of a Noncommutative Design Theory, PhD thesis, University of Vienna (1999).

noncomputable sectionnamespace OpenQuantumProblem23

A state vector in the $d$-dimensional complex Hilbert space $\mathbb{C}^d$.

abbrev StateVector (d : ℕ) := EuclideanSpace ℂ (Fin d)

Build a state vector from its coordinates in the computational basis.

abbrev mkStateVector {d : ℕ} (ψ : Fin d → ℂ) : StateVector d := WithLp.toLp 2 ψ

Coercion from a state vector to its coordinate function.

instance {d : ℕ} : CoeFun (StateVector d) (fun _ => Fin d → ℂ) where
  coe ψ := ψ.ofLp

A state vector is normalized if it has $L^2$ norm $1$.

def IsNormalized {d : ℕ} (ψ : StateVector d) : Prop := ‖ψ‖ = 1

The squared magnitude of the overlap between two state vectors.

def overlapSq {d : ℕ} (φ ψ : StateVector d) : ℝ :=
  Complex.normSq (∑ i : Fin d, star (φ i) * ψ i)

A family has constant pairwise squared overlap $c$ if every two distinct members have squared overlap $c$.

def HasConstantOverlapSq {d N : ℕ} (c : ℝ) (Φ : Fin N → StateVector d) : Prop :=
  Pairwise fun i j => overlapSq (Φ i) (Φ j) = c

The squared overlap value of a SIC family in dimension $d$.

def sicOverlapSq (d : ℕ) : ℝ := (d + 1 : ℝ)⁻¹

A SIC family in dimension $d$ consists of $d^2$ normalized vectors in $\mathbb{C}^d$ with pairwise squared overlap $(d + 1)^{-1}$.

def IsSICFamily (d : ℕ) (Φ : Fin (d ^ 2) → StateVector d) : Prop :=
  (∀ i, IsNormalized (Φ i)) ∧ HasConstantOverlapSq (sicOverlapSq d) Φ

There exists a SIC-POVM in dimension $d$.

def HasSICPOVM (d : ℕ) : Prop :=
  ∃ Φ : Fin (d ^ 2) → StateVector d, IsSICFamily d Φ

Any singleton family has constant pairwise squared overlap, vacuously.

@[category test, AMS 15 47 81]
lemma hasConstantOverlapSq_singleton {d : ℕ} (c : ℝ) (ψ : StateVector d) :
    HasConstantOverlapSq c (fun _ : Fin 1 => ψ) := byd:ℕc:ℝψ:StateVector d⊢ HasConstantOverlapSq c fun x => ψ
  intro i jd:ℕc:ℝψ:StateVector di:Fin 1j:Fin 1⊢ i ≠ j → (fun i j => overlapSq ((fun x => ψ) i) ((fun x => ψ) j) = c) i j hijd:ℕc:ℝψ:StateVector di:Fin 1j:Fin 1hij:i ≠ j⊢ overlapSq ((fun x => ψ) i) ((fun x => ψ) j) = c
  exact absurd (Subsingleton.elim i j) hijAll goals completed! 🐙

The SIC overlap value in dimension $1$ is $1/2$.

@[category test, AMS 15 47 81]
lemma sicOverlapSq_one : sicOverlapSq 1 = (1 / 2 : ℝ) := by⊢ sicOverlapSq 1 = 1 / 2
  simp [sicOverlapSq]⊢ 1 + 1 = 2; norm_numAll goals completed! 🐙

The SIC overlap value is positive in every dimension.

@[category test, AMS 15 47 81]
lemma sicOverlapSq_pos (d : ℕ) : 0 < sicOverlapSq d := byd:ℕ⊢ 0 < sicOverlapSq d
  simp [sicOverlapSq]d:ℕ⊢ 0 < ↑d + 1; positivityAll goals completed! 🐙

In dimension $1$, a singleton family is SIC exactly when its vector is normalized.

@[category test, AMS 15 47 81]
lemma isSICFamily_singleton_iff {ψ : StateVector 1} :
    IsSICFamily 1 (fun _ : Fin 1 => ψ) ↔ IsNormalized ψ := byψ:StateVector 1⊢ (IsSICFamily 1 fun x => ψ) ↔ IsNormalized ψ
  constructormpψ:StateVector 1⊢ (IsSICFamily 1 fun x => ψ) → IsNormalized ψmprψ:StateVector 1⊢ IsNormalized ψ → IsSICFamily 1 fun x => ψ
  ·mpψ:StateVector 1⊢ (IsSICFamily 1 fun x => ψ) → IsNormalized ψ intro ⟨h, _⟩mpψ:StateVector 1h:∀ (i : Fin (1 ^ 2)), IsNormalized ((fun x => ψ) i)right✝:HasConstantOverlapSq (sicOverlapSq 1) fun x => ψ⊢ IsNormalized ψ; exact h 0All goals completed! 🐙
  ·mprψ:StateVector 1⊢ IsNormalized ψ → IsSICFamily 1 fun x => ψ intro hmprψ:StateVector 1h:IsNormalized ψ⊢ IsSICFamily 1 fun x => ψ; exact ⟨fun _ => h, hasConstantOverlapSq_singleton _ _⟩All goals completed! 🐙

The empty family witnesses the degenerate dimension-$0$ case.

@[category test, AMS 15 47 81]
theorem hasSICPOVM_zero : HasSICPOVM 0 := by⊢ HasSICPOVM 0
  exact ⟨Fin.elim0, fun i => Fin.elim0 i, fun i j _ => Fin.elim0 i⟩All goals completed! 🐙

Any normalized state in dimension $1$ yields a SIC family.

@[category test, AMS 15 47 81]
lemma isSICFamily_one_of_normalized {ψ : StateVector 1} (hψ : IsNormalized ψ) :
    IsSICFamily 1 (fun _ : Fin 1 => ψ) :=
  isSICFamily_singleton_iff.mpr hψ

Dimension $1$ admits a SIC-POVM.

@[category test, AMS 15 47 81]
theorem hasSICPOVM_one : HasSICPOVM 1 := by⊢ HasSICPOVM 1
  refine ⟨fun _ => EuclideanSpace.single 0 1, isSICFamily_one_of_normalized ?_⟩⊢ IsNormalized (EuclideanSpace.single 0 1)
  simp [IsNormalized, EuclideanSpace.norm_single]All goals completed! 🐙

The standard algebraic primitive cube root of unity.

def ω : ℂ :=
  ((-(1 : ℝ) / 2 : ℝ) : ℂ) + ((Real.sqrt 3 / 2 : ℝ) : ℂ) * Complex.I

The first real amplitude used in the tetrahedral qubit SIC.

def tetraA : ℝ := Real.sqrt (1 / 3)

The second real amplitude used in the tetrahedral qubit SIC.

def tetraB : ℝ := Real.sqrt (2 / 3)

The common scale used in the Hesse qutrit SIC.

def hesseS : ℝ := Real.sqrt (1 / 2)

A convenient constructor for qubit state vectors.

def vec2 (z₀ z₁ : ℂ) : StateVector 2 := mkStateVector ![z₀, z₁]

A convenient constructor for qutrit state vectors.

def vec3 (z₀ z₁ z₂ : ℂ) : StateVector 3 := mkStateVector ![z₀, z₁, z₂]

The tetrahedral qubit SIC family.

def qubitSICFamily : Fin 4 → StateVector 2
  | 0 => vec2 1 0
  | 1 => vec2 (tetraA : ℂ) (tetraB : ℂ)
  | 2 => vec2 (tetraA : ℂ) ((tetraB : ℂ) * ω)
  | _ => vec2 (tetraA : ℂ) ((tetraB : ℂ) * (ω ^ 2))

The Hesse qutrit SIC family.

def hesseFamily : Fin 9 → StateVector 3
  | 0 => vec3 0 (hesseS : ℂ) (-(hesseS : ℂ))
  | 1 => vec3 0 (hesseS : ℂ) (-((hesseS : ℂ) * ω))
  | 2 => vec3 0 (hesseS : ℂ) (-((hesseS : ℂ) * (ω ^ 2)))
  | 3 => vec3 (-(hesseS : ℂ)) 0 (hesseS : ℂ)
  | 4 => vec3 (-((hesseS : ℂ) * ω)) 0 (hesseS : ℂ)
  | 5 => vec3 (-((hesseS : ℂ) * (ω ^ 2))) 0 (hesseS : ℂ)
  | 6 => vec3 (hesseS : ℂ) (-(hesseS : ℂ)) 0
  | 7 => vec3 (hesseS : ℂ) (-((hesseS : ℂ) * ω)) 0
  | _ => vec3 (hesseS : ℂ) (-((hesseS : ℂ) * (ω ^ 2))) 0

The BB84 family of four qubit states.

def bb84Family : Fin 4 → StateVector 2
  | 0 => vec2 1 0
  | 1 => vec2 0 1
  | 2 => vec2 (hesseS : ℂ) (hesseS : ℂ)
  | _ => vec2 (hesseS : ℂ) (-(hesseS : ℂ))

The SIC overlap value in dimension $2$ is $1/3$.

@[category test, AMS 15 47 81]
lemma sicOverlapSq_two : sicOverlapSq 2 = (1 / 3 : ℝ) := by⊢ sicOverlapSq 2 = 1 / 3
  simp [sicOverlapSq]⊢ 2 + 1 = 3; norm_numAll goals completed! 🐙

The SIC overlap value in dimension $3$ is $1/4$.

@[category test, AMS 15 47 81]
lemma sicOverlapSq_three : sicOverlapSq 3 = (1 / 4 : ℝ) := by⊢ sicOverlapSq 3 = 1 / 4
  simp [sicOverlapSq]⊢ 3 + 1 = 4; norm_numAll goals completed! 🐙

The unit complex number ω (primitive cube root) has norm 1.

@[category API, AMS 15 47 81]
private lemma omega_norm : ‖ω‖ = 1 := by⊢ ‖ω‖ = 1
  rw [Complex.norm_def, ω]⊢ √(Complex.normSq (↑(-1 / 2) + ↑(√3 / 2) * Complex.I)) = 1
  simp [Complex.normSq_apply]⊢ -1 / 2 * (-1 / 2) + √3 / 2 * (√3 / 2) = 1
  have : Real.sqrt 3 * Real.sqrt 3 = 3 := Real.mul_self_sqrt (by⊢ 0 ≤ 3 norm_numAll goals completed! 🐙)
  rw [show (-1 / 2 : ℝ) * (-1 / 2) + Real.sqrt 3 / 2 * (Real.sqrt 3 / 2) = 1
    from by nlinarith]All goals completed! 🐙

Every vector in the tetrahedral qubit SIC family is normalized.

@[category test, AMS 15 47 81]
lemma qubitSICFamily_normalized (i : Fin 4) :
    IsNormalized (qubitSICFamily i) := byi:Fin 4⊢ IsNormalized (qubitSICFamily i)
  have h2 : Real.sqrt 2 ^ 2 = 2 := Real.sq_sqrt (byi:Fin 4⊢ 0 ≤ 2 norm_numAll goals completed! 🐙)
  have h3 : Real.sqrt 3 ^ 2 = 3 := Real.sq_sqrt (byi:Fin 4h2:√2 ^ 2 = 2 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl true))⊢ 0 ≤ 3 norm_numAll goals completed! 🐙)
  have sqrt2_pos : (0:ℝ) < Real.sqrt 2 := Real.sqrt_pos.mpr (byi:Fin 4h2:√2 ^ 2 = 2 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl true))h3:√3 ^ 2 = 3 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)) (Eq.refl true))⊢ 0 < 2 norm_numAll goals completed! 🐙)
  have sqrt3_pos : (0:ℝ) < Real.sqrt 3 := Real.sqrt_pos.mpr (byi:Fin 4h2:√2 ^ 2 = 2 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl true))h3:√3 ^ 2 = 3 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)) (Eq.refl true))sqrt2_pos:0 < √2 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))⊢ 0 < 3 norm_numAll goals completed! 🐙)
  have omega2_norm : ‖ω ^ 2‖ = 1 := byi:Fin 4⊢ IsNormalized (qubitSICFamily i) rw [norm_pow, omega_norm]i:Fin 4h2:√2 ^ 2 = 2 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl true))h3:√3 ^ 2 = 3 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)) (Eq.refl true))sqrt2_pos:0 < √2 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))sqrt3_pos:0 < √3 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)) (Eq.refl false))⊢ 1 ^ 2 = 1; ringAll goals completed! 🐙
  fin_cases i«0»h2:√2 ^ 2 = 2 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl true))h3:√3 ^ 2 = 3 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)) (Eq.refl true))sqrt2_pos:0 < √2 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))sqrt3_pos:0 < √3 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)) (Eq.refl false))omega2_norm:‖ω ^ 2‖ = 1 := 
  Eq.mpr (id (congrArg (fun _a => _a = 1) (norm_pow ω 2)))
    (Eq.mpr (id (congrArg (fun _a => _a ^ 2 = 1) omega_norm))
      (Mathlib.Tactic.Ring.of_eq
        (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
          (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.one_pow (Nat.rawCast 2)))
            (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 1 + 0))
            (Mathlib.Tactic.Ring.add_mul
              (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))
                (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))
              (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
              (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))))
        (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))))⊢ IsNormalized (qubitSICFamily ((fun i => i) ⟨0, ⋯⟩))«1»h2:√2 ^ 2 = 2 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl true))h3:√3 ^ 2 = 3 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)) (Eq.refl true))sqrt2_pos:0 < √2 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))sqrt3_pos:0 < √3 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)) (Eq.refl false))omega2_norm:‖ω ^ 2‖ = 1 := 
  Eq.mpr (id (congrArg (fun _a => _a = 1) (norm_pow ω 2)))
    (Eq.mpr (id (congrArg (fun _a => _a ^ 2 = 1) omega_norm))
      (Mathlib.Tactic.Ring.of_eq
        (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
          (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.one_pow (Nat.rawCast 2)))
            (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 1 + 0))
            (Mathlib.Tactic.Ring.add_mul
              (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))
                (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))
              (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
              (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))))
        (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))))⊢ IsNormalized (qubitSICFamily ((fun i => i) ⟨1, ⋯⟩))«2»h2:√2 ^ 2 = 2 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl true))h3:√3 ^ 2 = 3 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)) (Eq.refl true))sqrt2_pos:0 < √2 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))sqrt3_pos:0 < √3 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)) (Eq.refl false))omega2_norm:‖ω ^ 2‖ = 1 := 
  Eq.mpr (id (congrArg (fun _a => _a = 1) (norm_pow ω 2)))
    (Eq.mpr (id (congrArg (fun _a => _a ^ 2 = 1) omega_norm))
      (Mathlib.Tactic.Ring.of_eq
        (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
          (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.one_pow (Nat.rawCast 2)))
            (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 1 + 0))
            (Mathlib.Tactic.Ring.add_mul
              (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))
                (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))
              (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
              (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))))
        (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))))⊢ IsNormalized (qubitSICFamily ((fun i => i) ⟨2, ⋯⟩))«3»h2:√2 ^ 2 = 2 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl true))h3:√3 ^ 2 = 3 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)) (Eq.refl true))sqrt2_pos:0 < √2 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))sqrt3_pos:0 < √3 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)) (Eq.refl false))omega2_norm:‖ω ^ 2‖ = 1 := 
  Eq.mpr (id (congrArg (fun _a => _a = 1) (norm_pow ω 2)))
    (Eq.mpr (id (congrArg (fun _a => _a ^ 2 = 1) omega_norm))
      (Mathlib.Tactic.Ring.of_eq
        (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
          (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.one_pow (Nat.rawCast 2)))
            (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 1 + 0))
            (Mathlib.Tactic.Ring.add_mul
              (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))
                (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))
              (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
              (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))))
        (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))))⊢ IsNormalized (qubitSICFamily ((fun i => i) ⟨3, ⋯⟩)) <;>«0»h2:√2 ^ 2 = 2 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl true))h3:√3 ^ 2 = 3 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)) (Eq.refl true))sqrt2_pos:0 < √2 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))sqrt3_pos:0 < √3 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)) (Eq.refl false))omega2_norm:‖ω ^ 2‖ = 1 := 
  Eq.mpr (id (congrArg (fun _a => _a = 1) (norm_pow ω 2)))
    (Eq.mpr (id (congrArg (fun _a => _a ^ 2 = 1) omega_norm))
      (Mathlib.Tactic.Ring.of_eq
        (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
          (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.one_pow (Nat.rawCast 2)))
            (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 1 + 0))
            (Mathlib.Tactic.Ring.add_mul
              (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))
                (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))
              (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
              (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))))
        (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))))⊢ IsNormalized (qubitSICFamily ((fun i => i) ⟨0, ⋯⟩))«1»h2:√2 ^ 2 = 2 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl true))h3:√3 ^ 2 = 3 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)) (Eq.refl true))sqrt2_pos:0 < √2 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))sqrt3_pos:0 < √3 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)) (Eq.refl false))omega2_norm:‖ω ^ 2‖ = 1 := 
  Eq.mpr (id (congrArg (fun _a => _a = 1) (norm_pow ω 2)))
    (Eq.mpr (id (congrArg (fun _a => _a ^ 2 = 1) omega_norm))
      (Mathlib.Tactic.Ring.of_eq
        (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
          (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.one_pow (Nat.rawCast 2)))
            (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 1 + 0))
            (Mathlib.Tactic.Ring.add_mul
              (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))
                (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))
              (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
              (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))))
        (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))))⊢ IsNormalized (qubitSICFamily ((fun i => i) ⟨1, ⋯⟩))«2»h2:√2 ^ 2 = 2 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl true))h3:√3 ^ 2 = 3 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)) (Eq.refl true))sqrt2_pos:0 < √2 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))sqrt3_pos:0 < √3 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)) (Eq.refl false))omega2_norm:‖ω ^ 2‖ = 1 := 
  Eq.mpr (id (congrArg (fun _a => _a = 1) (norm_pow ω 2)))
    (Eq.mpr (id (congrArg (fun _a => _a ^ 2 = 1) omega_norm))
      (Mathlib.Tactic.Ring.of_eq
        (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
          (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.one_pow (Nat.rawCast 2)))
            (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 1 + 0))
            (Mathlib.Tactic.Ring.add_mul
              (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))
                (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))
              (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
              (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))))
        (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))))⊢ IsNormalized (qubitSICFamily ((fun i => i) ⟨2, ⋯⟩))«3»h2:√2 ^ 2 = 2 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl true))h3:√3 ^ 2 = 3 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)) (Eq.refl true))sqrt2_pos:0 < √2 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))sqrt3_pos:0 < √3 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)) (Eq.refl false))omega2_norm:‖ω ^ 2‖ = 1 := 
  Eq.mpr (id (congrArg (fun _a => _a = 1) (norm_pow ω 2)))
    (Eq.mpr (id (congrArg (fun _a => _a ^ 2 = 1) omega_norm))
      (Mathlib.Tactic.Ring.of_eq
        (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
          (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.one_pow (Nat.rawCast 2)))
            (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 1 + 0))
            (Mathlib.Tactic.Ring.add_mul
              (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))
                (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))
              (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
              (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))))
        (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))))⊢ IsNormalized (qubitSICFamily ((fun i => i) ⟨3, ⋯⟩))
    simp [IsNormalized, qubitSICFamily, vec2, mkStateVector,
      EuclideanSpace.norm_eq, Fin.sum_univ_two, tetraA, tetraB,
      omega_norm, omega2_norm, abs_of_pos sqrt2_pos, abs_of_pos sqrt3_pos]«3»h2:√2 ^ 2 = 2 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl true))h3:√3 ^ 2 = 3 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)) (Eq.refl true))sqrt2_pos:0 < √2 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))sqrt3_pos:0 < √3 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)) (Eq.refl false))omega2_norm:‖ω ^ 2‖ = 1 := 
  Eq.mpr (id (congrArg (fun _a => _a = 1) (norm_pow ω 2)))
    (Eq.mpr (id (congrArg (fun _a => _a ^ 2 = 1) omega_norm))
      (Mathlib.Tactic.Ring.of_eq
        (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
          (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.one_pow (Nat.rawCast 2)))
            (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 1 + 0))
            (Mathlib.Tactic.Ring.add_mul
              (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))
                (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))
              (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
              (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))))
        (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))))⊢ 3⁻¹ + (√2 / √3) ^ 2 = 1
  all_goals (try (field_simp«3»h2:√2 ^ 2 = 2 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl true))h3:√3 ^ 2 = 3 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)) (Eq.refl true))sqrt2_pos:0 < √2 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))sqrt3_pos:0 < √3 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)) (Eq.refl false))omega2_norm:‖ω ^ 2‖ = 1 := 
  Eq.mpr (id (congrArg (fun _a => _a = 1) (norm_pow ω 2)))
    (Eq.mpr (id (congrArg (fun _a => _a ^ 2 = 1) omega_norm))
      (Mathlib.Tactic.Ring.of_eq
        (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
          (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.one_pow (Nat.rawCast 2)))
            (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 1 + 0))
            (Mathlib.Tactic.Ring.add_mul
              (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))
                (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))
              (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
              (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))))
        (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))))⊢ √3 ^ 2 + 3 * √2 ^ 2 = 3 * √3 ^ 2; linarith [h2, h3]All goals completed! 🐙))

The tetrahedral qubit SIC family has the correct constant pairwise overlap.

@[category test, AMS 15 47 81]
lemma declaration uses 'sorry'qubitSICFamily_pairwise :
    HasConstantOverlapSq (sicOverlapSq 2) qubitSICFamily := by⊢ HasConstantOverlapSq (sicOverlapSq 2) qubitSICFamily sorryAll goals completed! 🐙

Dimension $2$ admits a SIC-POVM, witnessed by the tetrahedral qubit SIC.

@[category test, AMS 15 47 81]
theorem declaration uses 'sorry'hasSICPOVM_two : HasSICPOVM 2 := by⊢ HasSICPOVM 2 sorryAll goals completed! 🐙

Every vector in the Hesse qutrit SIC family is normalized.

@[category test, AMS 15 47 81]
lemma hesseFamily_normalized (i : Fin 9) :
    IsNormalized (hesseFamily i) := byi:Fin 9⊢ IsNormalized (hesseFamily i)
  have h2 : Real.sqrt 2 ^ 2 = 2 := Real.sq_sqrt (byi:Fin 9⊢ 0 ≤ 2 norm_numAll goals completed! 🐙)
  have sqrt2_pos : (0:ℝ) < Real.sqrt 2 := Real.sqrt_pos.mpr (byi:Fin 9h2:√2 ^ 2 = 2 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl true))⊢ 0 < 2 norm_numAll goals completed! 🐙)
  have omega2_norm : ‖ω ^ 2‖ = 1 := byi:Fin 9⊢ IsNormalized (hesseFamily i) rw [norm_pow, omega_norm]i:Fin 9h2:√2 ^ 2 = 2 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl true))sqrt2_pos:0 < √2 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))⊢ 1 ^ 2 = 1; ringAll goals completed! 🐙
  fin_cases i«0»h2:√2 ^ 2 = 2 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl true))sqrt2_pos:0 < √2 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))omega2_norm:‖ω ^ 2‖ = 1 := 
  Eq.mpr (id (congrArg (fun _a => _a = 1) (norm_pow ω 2)))
    (Eq.mpr (id (congrArg (fun _a => _a ^ 2 = 1) omega_norm))
      (Mathlib.Tactic.Ring.of_eq
        (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
          (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.one_pow (Nat.rawCast 2)))
            (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 1 + 0))
            (Mathlib.Tactic.Ring.add_mul
              (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))
                (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))
              (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
              (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))))
        (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))))⊢ IsNormalized (hesseFamily ((fun i => i) ⟨0, ⋯⟩))«1»h2:√2 ^ 2 = 2 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl true))sqrt2_pos:0 < √2 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))omega2_norm:‖ω ^ 2‖ = 1 := 
  Eq.mpr (id (congrArg (fun _a => _a = 1) (norm_pow ω 2)))
    (Eq.mpr (id (congrArg (fun _a => _a ^ 2 = 1) omega_norm))
      (Mathlib.Tactic.Ring.of_eq
        (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
          (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.one_pow (Nat.rawCast 2)))
            (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 1 + 0))
            (Mathlib.Tactic.Ring.add_mul
              (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))
                (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))
              (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
              (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))))
        (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))))⊢ IsNormalized (hesseFamily ((fun i => i) ⟨1, ⋯⟩))«2»h2:√2 ^ 2 = 2 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl true))sqrt2_pos:0 < √2 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))omega2_norm:‖ω ^ 2‖ = 1 := 
  Eq.mpr (id (congrArg (fun _a => _a = 1) (norm_pow ω 2)))
    (Eq.mpr (id (congrArg (fun _a => _a ^ 2 = 1) omega_norm))
      (Mathlib.Tactic.Ring.of_eq
        (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
          (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.one_pow (Nat.rawCast 2)))
            (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 1 + 0))
            (Mathlib.Tactic.Ring.add_mul
              (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))
                (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))
              (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
              (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))))
        (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))))⊢ IsNormalized (hesseFamily ((fun i => i) ⟨2, ⋯⟩))«3»h2:√2 ^ 2 = 2 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl true))sqrt2_pos:0 < √2 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))omega2_norm:‖ω ^ 2‖ = 1 := 
  Eq.mpr (id (congrArg (fun _a => _a = 1) (norm_pow ω 2)))
    (Eq.mpr (id (congrArg (fun _a => _a ^ 2 = 1) omega_norm))
      (Mathlib.Tactic.Ring.of_eq
        (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
          (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.one_pow (Nat.rawCast 2)))
            (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 1 + 0))
            (Mathlib.Tactic.Ring.add_mul
              (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))
                (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))
              (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
              (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))))
        (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))))⊢ IsNormalized (hesseFamily ((fun i => i) ⟨3, ⋯⟩))«4»h2:√2 ^ 2 = 2 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl true))sqrt2_pos:0 < √2 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))omega2_norm:‖ω ^ 2‖ = 1 := 
  Eq.mpr (id (congrArg (fun _a => _a = 1) (norm_pow ω 2)))
    (Eq.mpr (id (congrArg (fun _a => _a ^ 2 = 1) omega_norm))
      (Mathlib.Tactic.Ring.of_eq
        (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
          (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.one_pow (Nat.rawCast 2)))
            (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 1 + 0))
            (Mathlib.Tactic.Ring.add_mul
              (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))
                (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))
              (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
              (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))))
        (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))))⊢ IsNormalized (hesseFamily ((fun i => i) ⟨4, ⋯⟩))«5»h2:√2 ^ 2 = 2 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl true))sqrt2_pos:0 < √2 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))omega2_norm:‖ω ^ 2‖ = 1 := 
  Eq.mpr (id (congrArg (fun _a => _a = 1) (norm_pow ω 2)))
    (Eq.mpr (id (congrArg (fun _a => _a ^ 2 = 1) omega_norm))
      (Mathlib.Tactic.Ring.of_eq
        (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
          (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.one_pow (Nat.rawCast 2)))
            (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 1 + 0))
            (Mathlib.Tactic.Ring.add_mul
              (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))
                (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))
              (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
              (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))))
        (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))))⊢ IsNormalized (hesseFamily ((fun i => i) ⟨5, ⋯⟩))«6»h2:√2 ^ 2 = 2 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl true))sqrt2_pos:0 < √2 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))omega2_norm:‖ω ^ 2‖ = 1 := 
  Eq.mpr (id (congrArg (fun _a => _a = 1) (norm_pow ω 2)))
    (Eq.mpr (id (congrArg (fun _a => _a ^ 2 = 1) omega_norm))
      (Mathlib.Tactic.Ring.of_eq
        (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
          (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.one_pow (Nat.rawCast 2)))
            (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 1 + 0))
            (Mathlib.Tactic.Ring.add_mul
              (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))
                (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))
              (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
              (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))))
        (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))))⊢ IsNormalized (hesseFamily ((fun i => i) ⟨6, ⋯⟩))«7»h2:√2 ^ 2 = 2 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl true))sqrt2_pos:0 < √2 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))omega2_norm:‖ω ^ 2‖ = 1 := 
  Eq.mpr (id (congrArg (fun _a => _a = 1) (norm_pow ω 2)))
    (Eq.mpr (id (congrArg (fun _a => _a ^ 2 = 1) omega_norm))
      (Mathlib.Tactic.Ring.of_eq
        (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
          (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.one_pow (Nat.rawCast 2)))
            (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 1 + 0))
            (Mathlib.Tactic.Ring.add_mul
              (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))
                (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))
              (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
              (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))))
        (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))))⊢ IsNormalized (hesseFamily ((fun i => i) ⟨7, ⋯⟩))«8»h2:√2 ^ 2 = 2 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl true))sqrt2_pos:0 < √2 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))omega2_norm:‖ω ^ 2‖ = 1 := 
  Eq.mpr (id (congrArg (fun _a => _a = 1) (norm_pow ω 2)))
    (Eq.mpr (id (congrArg (fun _a => _a ^ 2 = 1) omega_norm))
      (Mathlib.Tactic.Ring.of_eq
        (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
          (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.one_pow (Nat.rawCast 2)))
            (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 1 + 0))
            (Mathlib.Tactic.Ring.add_mul
              (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))
                (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))
              (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
              (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))))
        (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))))⊢ IsNormalized (hesseFamily ((fun i => i) ⟨8, ⋯⟩)) <;>«0»h2:√2 ^ 2 = 2 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl true))sqrt2_pos:0 < √2 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))omega2_norm:‖ω ^ 2‖ = 1 := 
  Eq.mpr (id (congrArg (fun _a => _a = 1) (norm_pow ω 2)))
    (Eq.mpr (id (congrArg (fun _a => _a ^ 2 = 1) omega_norm))
      (Mathlib.Tactic.Ring.of_eq
        (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
          (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.one_pow (Nat.rawCast 2)))
            (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 1 + 0))
            (Mathlib.Tactic.Ring.add_mul
              (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))
                (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))
              (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
              (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))))
        (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))))⊢ IsNormalized (hesseFamily ((fun i => i) ⟨0, ⋯⟩))«1»h2:√2 ^ 2 = 2 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl true))sqrt2_pos:0 < √2 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))omega2_norm:‖ω ^ 2‖ = 1 := 
  Eq.mpr (id (congrArg (fun _a => _a = 1) (norm_pow ω 2)))
    (Eq.mpr (id (congrArg (fun _a => _a ^ 2 = 1) omega_norm))
      (Mathlib.Tactic.Ring.of_eq
        (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
          (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.one_pow (Nat.rawCast 2)))
            (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 1 + 0))
            (Mathlib.Tactic.Ring.add_mul
              (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))
                (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))
              (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
              (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))))
        (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))))⊢ IsNormalized (hesseFamily ((fun i => i) ⟨1, ⋯⟩))«2»h2:√2 ^ 2 = 2 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl true))sqrt2_pos:0 < √2 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))omega2_norm:‖ω ^ 2‖ = 1 := 
  Eq.mpr (id (congrArg (fun _a => _a = 1) (norm_pow ω 2)))
    (Eq.mpr (id (congrArg (fun _a => _a ^ 2 = 1) omega_norm))
      (Mathlib.Tactic.Ring.of_eq
        (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
          (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.one_pow (Nat.rawCast 2)))
            (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 1 + 0))
            (Mathlib.Tactic.Ring.add_mul
              (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))
                (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))
              (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
              (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))))
        (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))))⊢ IsNormalized (hesseFamily ((fun i => i) ⟨2, ⋯⟩))«3»h2:√2 ^ 2 = 2 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl true))sqrt2_pos:0 < √2 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))omega2_norm:‖ω ^ 2‖ = 1 := 
  Eq.mpr (id (congrArg (fun _a => _a = 1) (norm_pow ω 2)))
    (Eq.mpr (id (congrArg (fun _a => _a ^ 2 = 1) omega_norm))
      (Mathlib.Tactic.Ring.of_eq
        (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
          (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.one_pow (Nat.rawCast 2)))
            (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 1 + 0))
            (Mathlib.Tactic.Ring.add_mul
              (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))
                (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))
              (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
              (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))))
        (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))))⊢ IsNormalized (hesseFamily ((fun i => i) ⟨3, ⋯⟩))«4»h2:√2 ^ 2 = 2 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl true))sqrt2_pos:0 < √2 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))omega2_norm:‖ω ^ 2‖ = 1 := 
  Eq.mpr (id (congrArg (fun _a => _a = 1) (norm_pow ω 2)))
    (Eq.mpr (id (congrArg (fun _a => _a ^ 2 = 1) omega_norm))
      (Mathlib.Tactic.Ring.of_eq
        (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
          (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.one_pow (Nat.rawCast 2)))
            (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 1 + 0))
            (Mathlib.Tactic.Ring.add_mul
              (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))
                (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))
              (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
              (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))))
        (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))))⊢ IsNormalized (hesseFamily ((fun i => i) ⟨4, ⋯⟩))«5»h2:√2 ^ 2 = 2 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl true))sqrt2_pos:0 < √2 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))omega2_norm:‖ω ^ 2‖ = 1 := 
  Eq.mpr (id (congrArg (fun _a => _a = 1) (norm_pow ω 2)))
    (Eq.mpr (id (congrArg (fun _a => _a ^ 2 = 1) omega_norm))
      (Mathlib.Tactic.Ring.of_eq
        (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
          (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.one_pow (Nat.rawCast 2)))
            (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 1 + 0))
            (Mathlib.Tactic.Ring.add_mul
              (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))
                (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))
              (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
              (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))))
        (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))))⊢ IsNormalized (hesseFamily ((fun i => i) ⟨5, ⋯⟩))«6»h2:√2 ^ 2 = 2 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl true))sqrt2_pos:0 < √2 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))omega2_norm:‖ω ^ 2‖ = 1 := 
  Eq.mpr (id (congrArg (fun _a => _a = 1) (norm_pow ω 2)))
    (Eq.mpr (id (congrArg (fun _a => _a ^ 2 = 1) omega_norm))
      (Mathlib.Tactic.Ring.of_eq
        (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
          (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.one_pow (Nat.rawCast 2)))
            (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 1 + 0))
            (Mathlib.Tactic.Ring.add_mul
              (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))
                (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))
              (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
              (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))))
        (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))))⊢ IsNormalized (hesseFamily ((fun i => i) ⟨6, ⋯⟩))«7»h2:√2 ^ 2 = 2 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl true))sqrt2_pos:0 < √2 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))omega2_norm:‖ω ^ 2‖ = 1 := 
  Eq.mpr (id (congrArg (fun _a => _a = 1) (norm_pow ω 2)))
    (Eq.mpr (id (congrArg (fun _a => _a ^ 2 = 1) omega_norm))
      (Mathlib.Tactic.Ring.of_eq
        (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
          (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.one_pow (Nat.rawCast 2)))
            (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 1 + 0))
            (Mathlib.Tactic.Ring.add_mul
              (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))
                (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))
              (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
              (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))))
        (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))))⊢ IsNormalized (hesseFamily ((fun i => i) ⟨7, ⋯⟩))«8»h2:√2 ^ 2 = 2 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl true))sqrt2_pos:0 < √2 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))omega2_norm:‖ω ^ 2‖ = 1 := 
  Eq.mpr (id (congrArg (fun _a => _a = 1) (norm_pow ω 2)))
    (Eq.mpr (id (congrArg (fun _a => _a ^ 2 = 1) omega_norm))
      (Mathlib.Tactic.Ring.of_eq
        (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
          (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.one_pow (Nat.rawCast 2)))
            (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 1 + 0))
            (Mathlib.Tactic.Ring.add_mul
              (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))
                (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))
              (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
              (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))))
        (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))))⊢ IsNormalized (hesseFamily ((fun i => i) ⟨8, ⋯⟩))
    simp [IsNormalized, hesseFamily, vec3, mkStateVector,
      EuclideanSpace.norm_eq, Fin.sum_univ_three, hesseS,
      omega_norm, omega2_norm, abs_of_pos sqrt2_pos]«8»h2:√2 ^ 2 = 2 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl true))sqrt2_pos:0 < √2 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))omega2_norm:‖ω ^ 2‖ = 1 := 
  Eq.mpr (id (congrArg (fun _a => _a = 1) (norm_pow ω 2)))
    (Eq.mpr (id (congrArg (fun _a => _a ^ 2 = 1) omega_norm))
      (Mathlib.Tactic.Ring.of_eq
        (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
          (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.one_pow (Nat.rawCast 2)))
            (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 1 + 0))
            (Mathlib.Tactic.Ring.add_mul
              (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))
                (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))
              (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
              (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))))
        (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))))⊢ 2⁻¹ + 2⁻¹ = 1
  all_goals (try (field_simp«8»h2:√2 ^ 2 = 2 := 
  Real.sq_sqrt
    (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl true))sqrt2_pos:0 < √2 := 
  Real.sqrt_pos.mpr
    (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false))omega2_norm:‖ω ^ 2‖ = 1 := 
  Eq.mpr (id (congrArg (fun _a => _a = 1) (norm_pow ω 2)))
    (Eq.mpr (id (congrArg (fun _a => _a ^ 2 = 1) omega_norm))
      (Mathlib.Tactic.Ring.of_eq
        (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
          (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.one_pow (Nat.rawCast 2)))
            (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 1 + 0))
            (Mathlib.Tactic.Ring.add_mul
              (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))
                (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))
              (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0))
              (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))))
        (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))))⊢ 1 + 1 = 2; linarith [h2]All goals completed! 🐙))

The Hesse qutrit SIC family has the correct constant pairwise overlap.

@[category test, AMS 15 47 81]
lemma declaration uses 'sorry'hesseFamily_pairwise :
    HasConstantOverlapSq (sicOverlapSq 3) hesseFamily := by⊢ HasConstantOverlapSq (sicOverlapSq 3) hesseFamily sorryAll goals completed! 🐙

Dimension $3$ admits a SIC-POVM, witnessed by the Hesse qutrit SIC.

@[category test, AMS 15 47 81]
theorem declaration uses 'sorry'hasSICPOVM_three : HasSICPOVM 3 := by⊢ HasSICPOVM 3 sorryAll goals completed! 🐙

Every vector in the BB84 family is normalized.

@[category test, AMS 15 47 81]
lemma bb84Family_normalized (i : Fin 4) :
    IsNormalized (bb84Family i) := byi:Fin 4⊢ IsNormalized (bb84Family i)
  fin_cases i«0»⊢ IsNormalized (bb84Family ((fun i => i) ⟨0, ⋯⟩))«1»⊢ IsNormalized (bb84Family ((fun i => i) ⟨1, ⋯⟩))«2»⊢ IsNormalized (bb84Family ((fun i => i) ⟨2, ⋯⟩))«3»⊢ IsNormalized (bb84Family ((fun i => i) ⟨3, ⋯⟩)) <;>«0»⊢ IsNormalized (bb84Family ((fun i => i) ⟨0, ⋯⟩))«1»⊢ IsNormalized (bb84Family ((fun i => i) ⟨1, ⋯⟩))«2»⊢ IsNormalized (bb84Family ((fun i => i) ⟨2, ⋯⟩))«3»⊢ IsNormalized (bb84Family ((fun i => i) ⟨3, ⋯⟩)) simp [IsNormalized, bb84Family, vec2, EuclideanSpace.norm_eq, hesseS]«3»⊢ 2⁻¹ + 2⁻¹ = 1 <;>«2»⊢ 2⁻¹ + 2⁻¹ = 1«3»⊢ 2⁻¹ + 2⁻¹ = 1 grindAll goals completed! 🐙

The BB84 family has the right cardinality for a qubit SIC but fails the constant-overlap condition.

@[category test, AMS 15 47 81]
theorem bb84Family_not_isSICFamily : ¬ IsSICFamily 2 bb84Family := by⊢ ¬IsSICFamily 2 bb84Family
  intro hh:IsSICFamily 2 bb84Family⊢ False
  have h_overlap := h.2 (show 0 ≠ 1 by⊢ ¬IsSICFamily 2 bb84Family decideAll goals completed! 🐙)
  simp [Fin.sum_univ_two, bb84Family, vec2, overlapSq, sicOverlapSq_two] at h_overlapAll goals completed! 🐙

Benchmark open subproblem: existence of a SIC-POVM in dimension $56$.

@[category research open, AMS 15 47 81]
theorem declaration uses 'sorry'hasSICPOVM_56 : answer(sorry) ↔ HasSICPOVM 56 := by⊢ True ↔ HasSICPOVM 56 sorryAll goals completed! 🐙

Benchmark open subproblem: existence of a SIC-POVM in dimension $58$.

@[category research open, AMS 15 47 81]
theorem declaration uses 'sorry'hasSICPOVM_58 : answer(sorry) ↔ HasSICPOVM 58 := by⊢ True ↔ HasSICPOVM 58 sorryAll goals completed! 🐙

Benchmark open subproblem: existence of a SIC-POVM in dimension $59$.

@[category research open, AMS 15 47 81]
theorem declaration uses 'sorry'hasSICPOVM_59 : answer(sorry) ↔ HasSICPOVM 59 := by⊢ True ↔ HasSICPOVM 59 sorryAll goals completed! 🐙

Benchmark open subproblem: existence of a SIC-POVM in dimension $60$.

@[category research open, AMS 15 47 81]
theorem declaration uses 'sorry'hasSICPOVM_60 : answer(sorry) ↔ HasSICPOVM 60 := by⊢ True ↔ HasSICPOVM 60 sorryAll goals completed! 🐙

Benchmark open subproblem: existence of a SIC-POVM in dimension $64$.

@[category research open, AMS 15 47 81]
theorem declaration uses 'sorry'hasSICPOVM_64 : answer(sorry) ↔ HasSICPOVM 64 := by⊢ True ↔ HasSICPOVM 64 sorryAll goals completed! 🐙

Benchmark open subproblem: existence of a SIC-POVM in dimension $68$.

@[category research open, AMS 15 47 81]
theorem declaration uses 'sorry'hasSICPOVM_68 : answer(sorry) ↔ HasSICPOVM 68 := by⊢ True ↔ HasSICPOVM 68 sorryAll goals completed! 🐙

Benchmark open subproblem: existence of a SIC-POVM in dimension $69$.

@[category research open, AMS 15 47 81]
theorem declaration uses 'sorry'hasSICPOVM_69 : answer(sorry) ↔ HasSICPOVM 69 := by⊢ True ↔ HasSICPOVM 69 sorryAll goals completed! 🐙

Benchmark open subproblem: existence of a SIC-POVM in dimension $70$.

@[category research open, AMS 15 47 81]
theorem declaration uses 'sorry'hasSICPOVM_70 : answer(sorry) ↔ HasSICPOVM 70 := by⊢ True ↔ HasSICPOVM 70 sorryAll goals completed! 🐙

Benchmark open subproblem: existence of a SIC-POVM in dimension $71$.

@[category research open, AMS 15 47 81]
theorem declaration uses 'sorry'hasSICPOVM_71 : answer(sorry) ↔ HasSICPOVM 71 := by⊢ True ↔ HasSICPOVM 71 sorryAll goals completed! 🐙

Benchmark open subproblem: existence of a SIC-POVM in dimension $72$.

@[category research open, AMS 15 47 81]
theorem declaration uses 'sorry'hasSICPOVM_72 : answer(sorry) ↔ HasSICPOVM 72 := by⊢ True ↔ HasSICPOVM 72 sorryAll goals completed! 🐙

Benchmark open subproblem: existence of a SIC-POVM in dimension $75$.

@[category research open, AMS 15 47 81]
theorem declaration uses 'sorry'hasSICPOVM_75 : answer(sorry) ↔ HasSICPOVM 75 := by⊢ True ↔ HasSICPOVM 75 sorryAll goals completed! 🐙

Do SIC-POVMs exist in every finite dimension?

@[category research open, AMS 15 47 81]
theorem declaration uses 'sorry'sicPOVMs :
    answer(sorry) ↔ ∀ d : ℕ, 1 ≤ d → HasSICPOVM d := by⊢ True ↔ ∀ (d : ℕ), 1 ≤ d → HasSICPOVM d
  sorryAll goals completed! 🐙


end OpenQuantumProblem23