structure FusionRing (ι : Type u_1) [DecidableEq ι] [Fintype ι] : Type u_1

• unit : ι
• N : ι → ι → ι → ℕ
• star : ι → ι
• star_star (i : ι) : self.star (self.star i) = i
• unit_mul (j k : ι) : self.N self.unit j k = if j = k then 1 else 0
• mul_unit (i k : ι) : self.N i self.unit k = if i = k then 1 else 0
• duality (i j : ι) : self.N i j self.unit = if j = self.star i then 1 else 0
• assoc (i j k l : ι) : ∑ m : ι, self.N i j m * self.N m k l = ∑ m : ι, self.N j k m * self.N i m l
• N_star_transpose (i j k : ι) : self.N i j k = self.N (self.star i) k j

theorem FusionRing.star_injective {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) : Function.Injective R.star

theorem FusionRing.star_surjective {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) : Function.Surjective R.star

theorem FusionRing.star_bijective {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) : Function.Bijective R.star

theorem FusionRing.star_unit {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) : R.star R.unit = R.unit

def FusionRing.IsAntiAutomorphism {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) (ψ : ι → ι) : Prop

theorem FusionRing.star_isAntiAutomorphism {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) : R.IsAntiAutomorphism R.star

def FusionRing.IsTransitive {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) : Prop

def FusionRing.mulMatrix {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) (i : ι) : Matrix ι ι ℕ

@[simp]

theorem FusionRing.mulMatrix_apply {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) (i j k : ι) : R.mulMatrix i j k = R.N i j k

def FusionRing.IsComplexEigenvalue {ι : Type u_1} [Fintype ι] (M : Matrix ι ι ℝ) (μ : ℂ) : Prop

theorem FusionRing.perron_frobenius_spectral_dominance {ι : Type u_2} [DecidableEq ι] [Fintype ι] [Nonempty ι] (M : Matrix ι ι ℝ) (hM : ∀ (i j : ι), 0 ≤ M i j) (ev : ℝ) (evec : ι → ℝ) (hv : ∀ (i : ι), 0 < evec i) (hev : M.mulVec evec = ev • evec) (μ : ℂ) : IsComplexEigenvalue M μ → ‖μ‖ ≤ ev

structure FusionRing.FPdimData {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) : Type u_1

• d : ι → ℝ
• d_unit : self.d R.unit = 1
• d_pos (i : ι) : self.d i > 0
• d_mul (i j : ι) : self.d i * self.d j = ∑ k : ι, ↑(R.N i j k) * self.d k

structure FusionRing.PerronFrobenius {ι : Type u_1} [Fintype ι] (M : Matrix ι ι ℝ) : Type u_1

• ev : ℝ
• evec : ι → ℝ
• ev_pos : 0 < self.ev
• evec_pos (i : ι) : 0 < self.evec i
• is_eigenvec : M.mulVec self.evec = self.ev • self.evec
• unique (μ : ℝ) (w : ι → ℝ) : (∀ (i : ι), 0 < w i) → M.mulVec w = μ • w → ∃ (c : ℝ), ∀ (i : ι), w i = c * self.evec i

class FusionRing.HasPerronFrobeniusProperty (ι : Type u_2) [DecidableEq ι] [Fintype ι] [Nonempty ι] : Type u_2

• pfEigenvec (M : Matrix ι ι ℝ) : (∀ (i j : ι), 0 < M i j) → (r : ℝ) ×' (v : ι → ℝ) ×' 0 < r ∧ (∀ (i : ι), 0 < v i) ∧ M.mulVec v = r • v
• pfUnique (M : Matrix ι ι ℝ) : (∀ (i j : ι), 0 < M i j) → ∀ (r₁ r₂ : ℝ) (v w : ι → ℝ), (∀ (i : ι), 0 < v i) → M.mulVec v = r₁ • v → (∀ (i : ι), 0 < w i) → M.mulVec w = r₂ • w → ∃ (c : ℝ), ∀ (i : ι), w i = c * v i

noncomputable def FusionRing.perron_frobenius_pos_matrix {ι : Type u_1} [DecidableEq ι] [Fintype ι] [Nonempty ι] [HasPerronFrobeniusProperty ι] (M : Matrix ι ι ℝ) (hM : ∀ (i j : ι), 0 < M i j) : PerronFrobenius M

noncomputable def FusionRing.rightMulMatrix {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) : Matrix ι ι ℝ

noncomputable def FusionRing.leftMulMatrixR {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) (X : ι) : Matrix ι ι ℝ

def FusionRing.leftMulMatrixZ {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) (X : ι) : Matrix ι ι ℤ

theorem FusionRing.leftMulMatrixR_eq_map_leftMulMatrixZ {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) (X : ι) : R.leftMulMatrixR X = (R.leftMulMatrixZ X).map ⇑(algebraMap ℤ ℝ)

theorem FusionRing.sum_N_pos {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) (X j : ι) : 0 < ∑ k : ι, R.N X j k

theorem FusionRing.sum_N_pos' {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) (j k : ι) : 0 < ∑ i : ι, R.N j i k

theorem FusionRing.left_transitive {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) (X Z : ι) : ∃ (Y : ι), 0 < R.N X Y Z

theorem FusionRing.right_transitive {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) (X Z : ι) : ∃ (Y : ι), 0 < R.N Y X Z

theorem FusionRing.isTransitive {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) : R.IsTransitive

theorem FusionRing.perron_frobenius_fusion_ring {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) [Nonempty ι] [HasPerronFrobeniusProperty ι] : ∃ (d : ι → ℝ), d R.unit = 1 ∧ (∀ (i : ι), d i > 0) ∧ ∀ (i j : ι), d i * d j = ∑ k : ι, ↑(R.N i j k) * d k

theorem FusionRing.d_star_of_d_mul {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) [Nonempty ι] (d : ι → ℝ) (d_pos : ∀ (i : ι), d i > 0) (d_mul : ∀ (i j : ι), d i * d j = ∑ k : ι, ↑(R.N i j k) * d k) (i : ι) : d (R.star i) = d i

theorem FusionRing.exists_FPdimData {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) [Nonempty ι] [HasPerronFrobeniusProperty ι] : Nonempty R.FPdimData

theorem FusionRing.FPdimData.d_star {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} (fpd : R.FPdimData) [Nonempty ι] (i : ι) : fpd.d (R.star i) = fpd.d i

noncomputable def FusionRing.FPdimData.FPdim {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} (fpd : R.FPdimData) : ι → ℝ

theorem FusionRing.FPdimData.d_ge_one {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} (fpd : R.FPdimData) (i : ι) : fpd.d i ≥ 1

noncomputable def FusionRing.FPdimData.catDim {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} (fpd : R.FPdimData) : ℝ

theorem FusionRing.FPdimData.catDim_pos {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} (fpd : R.FPdimData) [Nonempty ι] : fpd.catDim > 0

theorem FusionRing.FPdimData.catDim_ge_card {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} (fpd : R.FPdimData) : fpd.catDim ≥ ↑(Fintype.card ι)

theorem FusionRing.FPdimData.fpDim_unique_character {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} (fpd : R.FPdimData) [Nonempty ι] [HasPerronFrobeniusProperty ι] (χ : ι → ℝ) (hχ_unit : χ R.unit = 1) (hχ_pos : ∀ (i : ι), χ i > 0) (hχ_mul : ∀ (i j : ι), χ i * χ j = ∑ k : ι, ↑(R.N i j k) * χ k) (i : ι) : χ i = fpd.d i

theorem FusionRing.FPdimData.d_is_eigenvalue_of_mulMatrix {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} (fpd : R.FPdimData) (i : ι) : (R.leftMulMatrixR i).mulVec fpd.d = fpd.d i • fpd.d

theorem FusionRing.FPdimData.d_right_mul {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} (fpd : R.FPdimData) (j Y : ι) : ∑ k : ι, ↑(R.N j Y k) * fpd.d k = fpd.d j * fpd.d Y

theorem FusionRing.FPdimData.d_unique_positive_eigenvector {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} (fpd : R.FPdimData) [Nonempty ι] [HasPerronFrobeniusProperty ι] (w : ι → ℝ) (hw_pos : ∀ (i : ι), 0 < w i) (r : ℝ) (hw_eig : R.rightMulMatrix.mulVec w = r • w) : ∃ (c : ℝ), ∀ (i : ι), w i = c * fpd.d i

theorem FusionRing.FPdimData.d_dominates_eigenvalues {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} (fpd : R.FPdimData) [Nonempty ι] (i : ι) (μ : ℂ) (hμ : IsComplexEigenvalue (R.leftMulMatrixR i) μ) : ‖μ‖ ≤ fpd.d i

theorem FusionRing.FPdimData.d_eq_one_invertible {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} (fpd : R.FPdimData) (i : ι) (hi : fpd.d i = 1) (k : ι) : k ≠ R.unit → R.N i (R.star i) k = 0

theorem FusionRing.FPdimData.d_eq_one_of_invertible {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} (fpd : R.FPdimData) (i : ι) (h_inv : ∀ (k : ι), k ≠ R.unit → R.N i (R.star i) k = 0) : fpd.d i = 1

theorem FusionRing.FPdimData.corollary_1_45_9 {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} (fpd : R.FPdimData) (i : ι) : fpd.d i = 1 ↔ ∀ (k : ι), k ≠ R.unit → R.N i (R.star i) k = 0

theorem FusionRing.FPdimData.proposition_1_45_5_part1 {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} (fpd : R.FPdimData) : fpd.d R.unit = 1 ∧ ∀ (i j : ι), fpd.d i * fpd.d j = ∑ k : ι, ↑(R.N i j k) * fpd.d k

theorem FusionRing.FPdimData.proposition_1_45_5_part2 {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} (fpd : R.FPdimData) [Nonempty ι] [HasPerronFrobeniusProperty ι] : (∀ (X : ι), (R.leftMulMatrixR X).mulVec fpd.d = fpd.d X • fpd.d) ∧ (∀ (i : ι), fpd.d i > 0) ∧ fpd.catDim > 0 ∧ (∀ (j Y : ι), ∑ k : ι, ↑(R.N j Y k) * fpd.d k = fpd.d j * fpd.d Y) ∧ ∀ (w : ι → ℝ) (r : ℝ), (∀ (i : ι), 0 < w i) → R.rightMulMatrix.mulVec w = r • w → ∃ (c : ℝ), ∀ (i : ι), w i = c * fpd.d i

theorem FusionRing.FPdimData.proposition_1_45_5_part3 {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} (fpd : R.FPdimData) [Nonempty ι] [HasPerronFrobeniusProperty ι] (χ : ι → ℝ) (hχ_unit : χ R.unit = 1) (hχ_nonneg : ∀ (i : ι), 0 ≤ χ i) (hχ_mul : ∀ (i j : ι), χ i * χ j = ∑ k : ι, ↑(R.N i j k) * χ k) (i : ι) : χ i = fpd.d i

theorem FusionRing.FPdimData.proposition_1_45_5_part4 {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} (fpd : R.FPdimData) (i : ι) : (R.leftMulMatrixR i).mulVec fpd.d = fpd.d i • fpd.d

theorem FusionRing.FPdimData.proposition_1_45_5 {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} (fpd : R.FPdimData) : (fpd.d R.unit = 1 ∧ ∀ (i j : ι), fpd.d i * fpd.d j = ∑ k : ι, ↑(R.N i j k) * fpd.d k) ∧ (∀ (X : ι), (R.leftMulMatrixR X).mulVec fpd.d = fpd.d X • fpd.d) ∧ ∀ (i : ι), fpd.d i > 0

theorem FusionRing.FPdimData.fpdim_antiAut_invariant {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} (fpd : R.FPdimData) (ψ : ι → ι) (hψ : R.IsAntiAutomorphism ψ) (i : ι) : fpd.d (ψ i) = fpd.d i

theorem FusionRing.FPdimData.isIntegral_d {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} (fpd : R.FPdimData) (i : ι) : IsIntegral ℤ (fpd.d i)

theorem FusionRing.FPdimData.isIntegral_d_sq {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} (fpd : R.FPdimData) (i : ι) : IsIntegral ℤ (fpd.d i ^ 2)

theorem FusionRing.FPdimData.isIntegral_catDim {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} (fpd : R.FPdimData) : IsIntegral ℤ fpd.catDim

theorem FusionRing.FPdimData.proposition_1_45_4 {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} (fpd : R.FPdimData) [Nonempty ι] (i : ι) : IsIntegral ℤ (fpd.d i) ∧ (∀ (μ : ℂ), IsComplexEigenvalue (R.leftMulMatrixR i) μ → ‖μ‖ ≤ fpd.d i) ∧ fpd.d i ≥ 1

theorem kronecker_theorem (q : ℂ) (hq_int : IsIntegral ℤ q) (hq_norm : ‖q‖ = 1) (hq_conj : ∀ (β : ℂ), (Polynomial.aeval β) (minpoly ℤ q) = 0 → ‖β‖ = 1) : ∃ (n : ℕ), 0 < n ∧ q ^ n = 1

theorem norm_eq_one_of_quadratic_bounded (β : ℂ) (μ : ℝ) (hμ : |μ| < 2) (hpoly : β ^ 2 - ↑μ * β + 1 = 0) : ‖β‖ = 1

theorem conjugate_satisfies_bounded_quadratic_of_ev_to_kronecker {ι : Type u_1} [DecidableEq ι] [Fintype ι] [Nonempty ι] (B : Matrix ι ι ℕ) (ev : ℝ) (v : ι → ℝ) (hv_pos : ∀ (i : ι), 0 < v i) (hv_eig : (B.map Nat.cast).mulVec v = ev • v) (w : ι → ℝ) (hw_pos : ∀ (i : ι), 0 < w i) (hw_eig : (B.map Nat.cast * (B.map Nat.cast).transpose).mulVec w = ev ^ 2 • w) (hPF_B : ∀ (μ : ℂ), FusionRing.IsComplexEigenvalue (B.map Nat.cast) μ → ‖μ‖ ≤ ev) (hev_pos : 0 < ev) (hev_lt : ev < 2) (q : ℂ) (hq_def : q = { re := ev / 2, im := √(1 - (ev / 2) ^ 2) }) (hq_int : IsIntegral ℤ q) (β : ℂ) (hβ : (Polynomial.aeval β) (minpoly ℤ q) = 0) : ∃ (μ : ℝ), |μ| < 2 ∧ β ^ 2 - ↑μ * β + 1 = 0

theorem ev_to_kronecker_input {ι : Type u_1} [DecidableEq ι] [Fintype ι] [Nonempty ι] (B : Matrix ι ι ℕ) (ev : ℝ) (v : ι → ℝ) (hv_pos : ∀ (i : ι), 0 < v i) (hv_eig : (B.map Nat.cast).mulVec v = ev • v) (w : ι → ℝ) (hw_pos : ∀ (i : ι), 0 < w i) (hw_eig : (B.map Nat.cast * (B.map Nat.cast).transpose).mulVec w = ev ^ 2 • w) (hPF_B : ∀ (μ : ℂ), FusionRing.IsComplexEigenvalue (B.map Nat.cast) μ → ‖μ‖ ≤ ev) (hev_pos : 0 < ev) (hev_lt : ev < 2) : ∃ (q : ℂ), IsIntegral ℤ q ∧ ‖q‖ = 1 ∧ q + q⁻¹ = ↑ev ∧ ∀ (β : ℂ), (Polynomial.aeval β) (minpoly ℤ q) = 0 → ‖β‖ = 1

theorem galois_conjugate_cosine_bound {ι : Type u_1} [DecidableEq ι] [Fintype ι] [Nonempty ι] (B : Matrix ι ι ℕ) (ev : ℝ) (v : ι → ℝ) (hv_pos : ∀ (i : ι), 0 < v i) (hv_eig : (B.map Nat.cast).mulVec v = ev • v) (hPF_B : ∀ (μ : ℂ), FusionRing.IsComplexEigenvalue (B.map Nat.cast) μ → ‖μ‖ ≤ ev) (m k : ℕ) (hm : 2 ≤ m) (hk_cop : k.Coprime m) (hk_pos : 1 ≤ k) (hk_lt : k < m) (hev_eq : ev = 2 * Real.cos (2 * Real.pi * ↑k / ↑m)) (j : ℕ) (hj_cop : j.Coprime m) : |2 * Real.cos (2 * Real.pi * ↑j / ↑m)| ≤ ev

theorem root_of_unity_cosine_extraction {ι : Type u_1} [DecidableEq ι] [Fintype ι] [Nonempty ι] (B : Matrix ι ι ℕ) (ev : ℝ) (v : ι → ℝ) (hv_pos : ∀ (i : ι), 0 < v i) (hv_eig : (B.map Nat.cast).mulVec v = ev • v) (hPF_B : ∀ (μ : ℂ), FusionRing.IsComplexEigenvalue (B.map Nat.cast) μ → ‖μ‖ ≤ ev) (hev_pos : 0 < ev) (hev_lt : ev < 2) (q : ℂ) (hq_sum : q + q⁻¹ = ↑ev) (n : ℕ) (hn : 0 < n) (hq_pow : q ^ n = 1) : ∃ (m : ℕ) (k : ℕ), 2 ≤ m ∧ k.Coprime m ∧ 1 ≤ k ∧ k < m ∧ ev = 2 * Real.cos (2 * Real.pi * ↑k / ↑m) ∧ ∀ (j : ℕ), j.Coprime m → |2 * Real.cos (2 * Real.pi * ↑j / ↑m)| ≤ ev

theorem kronecker_ev_intermediate {ι : Type u_1} [DecidableEq ι] [Fintype ι] [Nonempty ι] (B : Matrix ι ι ℕ) (ev : ℝ) (v : ι → ℝ) (hv_pos : ∀ (i : ι), 0 < v i) (hv_eig : (B.map Nat.cast).mulVec v = ev • v) (w : ι → ℝ) (hw_pos : ∀ (i : ι), 0 < w i) (hw_eig : (B.map Nat.cast * (B.map Nat.cast).transpose).mulVec w = ev ^ 2 • w) (hPF_B : ∀ (μ : ℂ), FusionRing.IsComplexEigenvalue (B.map Nat.cast) μ → ‖μ‖ ≤ ev) (hev_pos : 0 < ev) (hev_lt : ev < 2) : ∃ (m : ℕ) (k : ℕ), 2 ≤ m ∧ k.Coprime m ∧ 1 ≤ k ∧ k < m ∧ ev = 2 * Real.cos (2 * Real.pi * ↑k / ↑m) ∧ ∀ (j : ℕ), j.Coprime m → |2 * Real.cos (2 * Real.pi * ↑j / ↑m)| ≤ ev

theorem cos_two_pi_mul_div_le (m k : ℕ) (hm : 2 ≤ m) (hk1 : 1 ≤ k) (hk_lt : k < m) : Real.cos (2 * Real.pi * ↑k / ↑m) ≤ Real.cos (2 * Real.pi / ↑m)

theorem kronecker_ev_root_of_unity {ι : Type u_1} [DecidableEq ι] [Fintype ι] [Nonempty ι] (B : Matrix ι ι ℕ) (ev : ℝ) (v : ι → ℝ) (hv_pos : ∀ (i : ι), 0 < v i) (hv_eig : (B.map Nat.cast).mulVec v = ev • v) (w : ι → ℝ) (hw_pos : ∀ (i : ι), 0 < w i) (hw_eig : (B.map Nat.cast * (B.map Nat.cast).transpose).mulVec w = ev ^ 2 • w) (hPF_B : ∀ (μ : ℂ), FusionRing.IsComplexEigenvalue (B.map Nat.cast) μ → ‖μ‖ ≤ ev) (hev_pos : 0 < ev) (hev_lt : ev < 2) : ∃ (m : ℕ), 2 ≤ m ∧ ev = 2 * Real.cos (2 * Real.pi / ↑m) ∧ ∀ (j : ℕ), j.Coprime m → |2 * Real.cos (2 * Real.pi * ↑j / ↑m)| ≤ ev

theorem cos_two_pi_p_div_odd (p : ℕ) : Real.cos (2 * Real.pi * ↑p / (2 * ↑p + 1)) = -Real.cos (Real.pi / (2 * ↑p + 1))

theorem cos_pi_div_2p1_pos (p : ℕ) (hp : 1 ≤ p) : 0 < Real.cos (Real.pi / (2 * ↑p + 1))

theorem cos_pi_div_odd_lt (p : ℕ) (hp : 1 ≤ p) : Real.cos (2 * Real.pi / (2 * ↑p + 1)) < Real.cos (Real.pi / (2 * ↑p + 1))

theorem coprime_p_two_p_succ (p : ℕ) : p.Coprime (2 * p + 1)

theorem odd_m_violates_dominance (p : ℕ) (hp : 1 ≤ p) : 2 * Real.cos (2 * Real.pi / (2 * ↑p + 1)) < |2 * Real.cos (2 * Real.pi * ↑p / (2 * ↑p + 1))|

theorem ev_nonneg_of_nonneg_matrix_pos_eigvec {ι : Type u_1} [Fintype ι] [Nonempty ι] (B : Matrix ι ι ℕ) (ev : ℝ) (v : ι → ℝ) (hv_pos : ∀ (i : ι), 0 < v i) (hv_eig : (B.map Nat.cast).mulVec v = ev • v) : 0 ≤ ev

theorem kronecker_eigenvalue_cos {ι : Type u_1} [DecidableEq ι] [Fintype ι] [Nonempty ι] (B : Matrix ι ι ℕ) (ev : ℝ) (v : ι → ℝ) (hv_pos : ∀ (i : ι), 0 < v i) (hv_eig : (B.map Nat.cast).mulVec v = ev • v) (w : ι → ℝ) (hw_pos : ∀ (i : ι), 0 < w i) (hw_eig : (B.map Nat.cast * (B.map Nat.cast).transpose).mulVec w = ev ^ 2 • w) (hPF : ∀ (μ : ℂ), FusionRing.IsComplexEigenvalue (B.map Nat.cast) μ → ‖μ‖ ≤ ev) (hev_lt : ev < 2) : ∃ (n : ℕ), 2 ≤ n ∧ ev = 2 * Real.cos (Real.pi / ↑n)

theorem PerronFrobeniusGeneral.sum_pos_mul_nonneg_eq_zero_imp {ι : Type u_1} [Fintype ι] (a u : ι → ℝ) (ha : ∀ (i : ι), 0 < a i) (hu : ∀ (i : ι), 0 ≤ u i) (hsum : ∑ i : ι, a i * u i = 0) (i : ι) : u i = 0

theorem PerronFrobeniusGeneral.mulVec_diff_eq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (M : Matrix ι ι ℝ) (r s : ℝ) (v w : ι → ℝ) (c : ℝ) (hev : M.mulVec v = r • v) (hew : M.mulVec w = s • w) (k : ι) : ∑ i : ι, M k i * (w i - c * v i) = s * w k - c * r * v k

theorem PerronFrobeniusGeneral.pfUnique_general {ι : Type u_1} [DecidableEq ι] [Fintype ι] [Nonempty ι] (M : Matrix ι ι ℝ) (hM : ∀ (i j : ι), 0 < M i j) (r₁ r₂ : ℝ) (v w : ι → ℝ) (hv : ∀ (i : ι), 0 < v i) (hev : M.mulVec v = r₁ • v) (hw : ∀ (i : ι), 0 < w i) (hew : M.mulVec w = r₂ • w) : ∃ (c : ℝ), ∀ (i : ι), w i = c * v i

@[implicit_reducible]

noncomputable instance PerronFrobeniusFin1.instHasPerronFrobeniusPropertyFinOfNatNat : FusionRing.HasPerronFrobeniusProperty (Fin 1)

def PerronFrobeniusFin2.pfDiscriminant (M : Matrix (Fin 2) (Fin 2) ℝ) : ℝ

Discriminant of the characteristic polynomial of a 2×2 matrix, (M₀₀ - M₁₁)² + 4 M₀₁ M₁₀.

noncomputable def PerronFrobeniusFin2.pfEigenvalue (M : Matrix (Fin 2) (Fin 2) ℝ) : ℝ

The larger root of the characteristic polynomial of a 2×2 matrix, the candidate Perron–Frobenius eigenvalue.

noncomputable def PerronFrobeniusFin2.pfEigenvec (M : Matrix (Fin 2) (Fin 2) ℝ) : Fin 2 → ℝ

Explicit Perron–Frobenius eigenvector of a 2×2 matrix, (M 0 1, pfEigenvalue M - M 0 0).

theorem PerronFrobeniusFin2.pfDiscriminant_pos (M : Matrix (Fin 2) (Fin 2) ℝ) (hM : ∀ (i j : Fin 2), 0 < M i j) : 0 < pfDiscriminant M

The discriminant pfDiscriminant M of a strictly positive 2×2 matrix is positive.

theorem PerronFrobeniusFin2.pfEigenvalue_pos (M : Matrix (Fin 2) (Fin 2) ℝ) (hM : ∀ (i j : Fin 2), 0 < M i j) : 0 < pfEigenvalue M

The Perron–Frobenius eigenvalue of a strictly positive 2×2 matrix is positive.

theorem PerronFrobeniusFin2.sqrt_disc_gt_diff (M : Matrix (Fin 2) (Fin 2) ℝ) (hM : ∀ (i j : Fin 2), 0 < M i j) : M 0 0 - M 1 1 < √(pfDiscriminant M)

For a strictly positive 2×2 matrix, M 0 0 - M 1 1 < sqrt(pfDiscriminant M).

theorem PerronFrobeniusFin2.pfEigenvec_pos (M : Matrix (Fin 2) (Fin 2) ℝ) (hM : ∀ (i j : Fin 2), 0 < M i j) (i : Fin 2) : 0 < pfEigenvec M i

The explicit eigenvector pfEigenvec M has strictly positive entries when M does.

theorem PerronFrobeniusFin2.pfEigenvalue_char_poly (M : Matrix (Fin 2) (Fin 2) ℝ) (hM : ∀ (i j : Fin 2), 0 < M i j) : pfEigenvalue M ^ 2 - (M 0 0 + M 1 1) * pfEigenvalue M + (M 0 0 * M 1 1 - M 0 1 * M 1 0) = 0

pfEigenvalue M is a root of the characteristic polynomial of M.

theorem PerronFrobeniusFin2.pfEigenvec_is_eigenvec (M : Matrix (Fin 2) (Fin 2) ℝ) (hM : ∀ (i j : Fin 2), 0 < M i j) : M.mulVec (pfEigenvec M) = pfEigenvalue M • pfEigenvec M

pfEigenvec M is an eigenvector of M with eigenvalue pfEigenvalue M.

theorem PerronFrobeniusFin2.pfUnique_fin2 (M : Matrix (Fin 2) (Fin 2) ℝ) (hM : ∀ (i j : Fin 2), 0 < M i j) (r₁ r₂ : ℝ) (v w : Fin 2 → ℝ) (hv : ∀ (i : Fin 2), 0 < v i) (hev : M.mulVec v = r₁ • v) (hw : ∀ (i : Fin 2), 0 < w i) (hew : M.mulVec w = r₂ • w) : ∃ (c : ℝ), ∀ (i : Fin 2), w i = c * v i

Uniqueness of positive eigenvectors of a strictly positive 2×2 matrix up to scaling.

@[implicit_reducible]

noncomputable instance PerronFrobeniusFin2.instHasPerronFrobeniusPropertyFinOfNatNat : FusionRing.HasPerronFrobeniusProperty (Fin 2)

noncomputable def perronFrobeniusExistence {ι : Type u_1} [DecidableEq ι] [Fintype ι] [Nonempty ι] (M : Matrix ι ι ℝ) (hM : ∀ (i j : ι), 0 < M i j) : (r : ℝ) ×' (v : ι → ℝ) ×' 0 < r ∧ (∀ (i : ι), 0 < v i) ∧ M.mulVec v = r • v

Existence of a Perron–Frobenius eigenpair for any strictly positive matrix: a positive eigenvalue r together with a strictly positive eigenvector.

@[implicit_reducible]

noncomputable instance instHasPerronFrobeniusPropertyGeneral (ι : Type u_1) [DecidableEq ι] [Fintype ι] [Nonempty ι] : FusionRing.HasPerronFrobeniusProperty ι

General HasPerronFrobeniusProperty instance combining the existence result perronFrobeniusExistence with the uniqueness PerronFrobeniusGeneral.pfUnique_general.

noncomputable def theorem_1_44_1_existence {ι : Type u_1} [DecidableEq ι] [Fintype ι] [Nonempty ι] (M : Matrix ι ι ℝ) (hM : ∀ (i j : ι), 0 < M i j) : (r : ℝ) ×' (v : ι → ℝ) ×' 0 < r ∧ (∀ (i : ι), 0 < v i) ∧ M.mulVec v = r • v

Existence part of EGNO Theorem 1.44.1: every strictly positive matrix has a positive eigenvalue with a positive eigenvector.

theorem theorem_1_44_1_uniqueness {ι : Type u_1} [DecidableEq ι] [Fintype ι] [Nonempty ι] (M : Matrix ι ι ℝ) (hM : ∀ (i j : ι), 0 < M i j) (r₁ r₂ : ℝ) (v w : ι → ℝ) (hv : ∀ (i : ι), 0 < v i) (hev : M.mulVec v = r₁ • v) (hw : ∀ (i : ι), 0 < w i) (hew : M.mulVec w = r₂ • w) : ∃ (c : ℝ), ∀ (i : ι), w i = c * v i

Uniqueness part of EGNO Theorem 1.44.1: any two positive eigenvectors of a strictly positive matrix are scalar multiples of each other.

noncomputable def theorem_1_44_1 {ι : Type u_1} [DecidableEq ι] [Fintype ι] [Nonempty ι] (M : Matrix ι ι ℝ) (hM : ∀ (i j : ι), 0 < M i j) : FusionRing.PerronFrobenius M

EGNO Theorem 1.44.1 (Perron–Frobenius for strictly positive matrices): existence and uniqueness of a Perron–Frobenius eigenpair, bundled as a PerronFrobenius M.

theorem FusionRing.kronecker_FPdim {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) (fpd : R.FPdimData) (i : ι) (hi : fpd.d i < 2) : ∃ n ≥ 2, fpd.d i = 2 * Real.cos (Real.pi / ↑n)

Application of the Kronecker spectral extraction to the Frobenius–Perron dimension: if fpd.d i < 2 then fpd.d i = 2 cos(π/n) for some integer n ≥ 2.

theorem FusionRing.FPdimData.FPdim_lt_two_eq_cos {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} (fpd : R.FPdimData) (i : ι) (hi : fpd.d i < 2) : ∃ n ≥ 3, fpd.d i = 2 * Real.cos (Real.pi / ↑n)

EGNO Corollary 1.45.16: if fpd.d i < 2, then fpd.d i = 2 cos(π/n) for some integer n ≥ 3.

theorem proposition_1_45_4 {ι : Type u_1} [DecidableEq ι] [Fintype ι] [Nonempty ι] {R : FusionRing ι} (fpd : R.FPdimData) (i : ι) : IsIntegral ℤ (fpd.d i) ∧ (∀ (μ : ℂ), FusionRing.IsComplexEigenvalue (R.leftMulMatrixR i) μ → ‖μ‖ ≤ fpd.d i) ∧ fpd.d i ≥ 1

Top-level statement of EGNO Proposition 1.45.4 packaged as a single theorem on R.FPdimData.