Arbitrary-rank interlacing

Mickelsson operators, interlacing schedules, and canonical projected-axis witnesses.

def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathCommutator.upperPolarizationPathCommutator {r n : ℕ} (a b : Fin (r + 1)) : List (Fin (r + 1)) → PolynomialSpace r n →ₗ[ℝ] PolynomialSpace r n

The upper polarization path commutator used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.
• MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathCommutator.upperPolarizationPathCommutator a b [] = 0
• MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathCommutator.upperPolarizationPathCommutator a b [head] = 0

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathCommutator.upperPolarizationPathCommutator_nil {r n : ℕ} (a b : Fin (r + 1)) : upperPolarizationPathCommutator a b [] = 0

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathCommutator.upperPolarizationPathCommutator_singleton {r n : ℕ} (a b i : Fin (r + 1)) : upperPolarizationPathCommutator a b [i] = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathCommutator.polarization_lowerPolarizationPath_commutator {r n : ℕ} (a b : Fin (r + 1)) (path : List (Fin (r + 1))) (p : PolynomialSpace r n) : (polarization r n a b) ((AllRankArbitraryRowBranchingOperator.lowerPolarizationPath path) p) = (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath path) ((polarization r n a b) p) + (upperPolarizationPathCommutator a b path) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathCommutator.lowerPolarizationPath_append_cons_apply {r n : ℕ} (front : List (Fin (r + 1))) (middle : Fin (r + 1)) (suffix : List (Fin (r + 1))) (p : PolynomialSpace r n) : (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (front ++ middle :: suffix)) p = (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (front ++ [middle])) ((AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (middle :: suffix)) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathCommutator.upperPolarizationPathCommutator_eq_zero_of_le {r n : ℕ} (a b : Fin (r + 1)) (hab : a < b) (path : List (Fin (r + 1))) (hpath : List.Pairwise (fun (x1 x2 : Fin (r + 1)) => x1 < x2) path) (hle : ∀ i ∈ path, i ≤ a) : upperPolarizationPathCommutator a b path = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathCommutator.upperPolarizationPathCommutator_eq_zero_of_ge {r n : ℕ} (a b : Fin (r + 1)) (hab : a < b) (path : List (Fin (r + 1))) (hpath : List.Pairwise (fun (x1 x2 : Fin (r + 1)) => x1 < x2) path) (hge : ∀ i ∈ path, b ≤ i) : upperPolarizationPathCommutator a b path = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathCommutator.polarization_lowerPolarizationPath_commute_prefix {r n : ℕ} (a b : Fin (r + 1)) (hab : a < b) (path : List (Fin (r + 1))) (hpath : List.Pairwise (fun (x1 x2 : Fin (r + 1)) => x1 < x2) path) (hle : ∀ i ∈ path, i ≤ a) (p : PolynomialSpace r n) : (polarization r n a b) ((AllRankArbitraryRowBranchingOperator.lowerPolarizationPath path) p) = (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath path) ((polarization r n a b) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathCommutator.polarization_lowerPolarizationPath_commute_suffix {r n : ℕ} (a b : Fin (r + 1)) (hab : a < b) (path : List (Fin (r + 1))) (hpath : List.Pairwise (fun (x1 x2 : Fin (r + 1)) => x1 < x2) path) (hge : ∀ i ∈ path, b ≤ i) (p : PolynomialSpace r n) : (polarization r n a b) ((AllRankArbitraryRowBranchingOperator.lowerPolarizationPath path) p) = (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath path) ((polarization r n a b) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathRecurrence.polarizationPathCoefficient_insert {r : ℕ} (lam : Fin (r + 1) → ℕ) (row a : Fin (r + 1)) (S : Finset (Fin (r + 1))) (ha : a < row) (haS : a ∉ S) : AllRankArbitraryRowBranchingOperator.polarizationPathCoefficient lam row S = -AllRankArbitraryRowBranchingOperator.shiftedRowGap lam row a * AllRankArbitraryRowBranchingOperator.polarizationPathCoefficient lam row (insert a S)

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathRecurrence.shiftedRowGap_sub_adjacent {r : ℕ} (lam : Fin (r + 1) → ℕ) (row a b : Fin (r + 1)) (hab : ↑a + 1 = ↑b) (hbrow : b < row) (hweight : lam b ≤ lam a) (hlow : lam row ≤ lam b) : AllRankArbitraryRowBranchingOperator.shiftedRowGap lam row a - AllRankArbitraryRowBranchingOperator.shiftedRowGap lam row b = ↑(lam a - lam b) + 1

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowFourStateSubsetSorting.sort_union_of_forall_lt {α : Type u_1} [LinearOrder α] (L U : Finset α) (hsep : ∀ i ∈ L, ∀ j ∈ U, i < j) : ((L ∪ U).sort fun (x1 x2 : α) => x1 ≤ x2) = (L.sort fun (x1 x2 : α) => x1 ≤ x2) ++ U.sort fun (x1 x2 : α) => x1 ≤ x2

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowFourStateSubsetSorting.adjacent_subset_filter_union {r : ℕ} (a b : Fin (r + 1)) (hab : ↑a + 1 = ↑b) (T : Finset (Fin (r + 1))) (haT : a ∉ T) (hbT : b ∉ T) : T = {i ∈ T | i < a} ∪ {i ∈ T | b < i}

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowFourStateSubsetSorting.sorted_subset_neither {r : ℕ} (a b : Fin (r + 1)) (hab : ↑a + 1 = ↑b) (T : Finset (Fin (r + 1))) (haT : a ∉ T) (hbT : b ∉ T) : (T.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) = ({i ∈ T | i < a}.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ {i ∈ T | b < i}.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowFourStateSubsetSorting.sorted_subset_first {r : ℕ} (a b : Fin (r + 1)) (hab : ↑a + 1 = ↑b) (T : Finset (Fin (r + 1))) (haT : a ∉ T) (hbT : b ∉ T) : ((insert a T).sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) = ({i ∈ T | i < a}.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ a :: {i ∈ T | b < i}.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowFourStateSubsetSorting.sorted_subset_second {r : ℕ} (a b : Fin (r + 1)) (hab : ↑a + 1 = ↑b) (T : Finset (Fin (r + 1))) (haT : a ∉ T) (hbT : b ∉ T) : ((insert b T).sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) = ({i ∈ T | i < a}.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ b :: {i ∈ T | b < i}.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowFourStateSubsetSorting.sorted_subset_both {r : ℕ} (a b : Fin (r + 1)) (hab : ↑a + 1 = ↑b) (T : Finset (Fin (r + 1))) (haT : a ∉ T) (hbT : b ∉ T) : ((insert a (insert b T)).sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) = ({i ∈ T | i < a}.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ a :: b :: {i ∈ T | b < i}.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathToggle.simpleRoot_suffix_highest {r n : ℕ} (a b j : Fin (r + 1)) (hab : a < b) (tail : List (Fin (r + 1))) (hordered : List.Pairwise (fun (x1 x2 : Fin (r + 1)) => x1 < x2) (j :: tail)) (hafter : ∀ z ∈ j :: tail, b ≤ z) (p : PolynomialSpace r n) (hp : (polarization r n a b) p = 0) : (polarization r n a b) ((AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (j :: tail)) p) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathToggle.lowerPolarizationPath_toggle_neither_factor {r n : ℕ} (front : List (Fin (r + 1))) (i j : Fin (r + 1)) (tail : List (Fin (r + 1))) (p : PolynomialSpace r n) : (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (front ++ i :: j :: tail)) p = (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (front ++ [i])) ((polarization r n j i) ((AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (j :: tail)) p))

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathToggle.lowerPolarizationPath_toggle_first_factor {r n : ℕ} (front : List (Fin (r + 1))) (i a j : Fin (r + 1)) (tail : List (Fin (r + 1))) (p : PolynomialSpace r n) : (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (front ++ i :: a :: j :: tail)) p = (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (front ++ [i])) ((polarization r n a i) ((polarization r n j a) ((AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (j :: tail)) p)))

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathToggle.lowerPolarizationPath_toggle_second_factor {r n : ℕ} (front : List (Fin (r + 1))) (i b j : Fin (r + 1)) (tail : List (Fin (r + 1))) (p : PolynomialSpace r n) : (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (front ++ i :: b :: j :: tail)) p = (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (front ++ [i])) ((polarization r n b i) ((polarization r n j b) ((AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (j :: tail)) p)))

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathToggle.lowerPolarizationPath_toggle_both_factor {r n : ℕ} (front : List (Fin (r + 1))) (i a b j : Fin (r + 1)) (tail : List (Fin (r + 1))) (p : PolynomialSpace r n) : (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (front ++ i :: a :: b :: j :: tail)) p = (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (front ++ [i])) ((polarization r n a i) ((polarization r n b a) ((polarization r n j b) ((AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (j :: tail)) p))))

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathToggle.simpleRoot_polarization_path_neither {r n : ℕ} (front : List (Fin (r + 1))) (i a b j : Fin (r + 1)) (tail : List (Fin (r + 1))) (hia : i < a) (hab : a < b) (hbj : b < j) (hfront : List.Pairwise (fun (x1 x2 : Fin (r + 1)) => x1 < x2) (front ++ [i])) (hbefore : ∀ z ∈ front ++ [i], z ≤ a) (htail : List.Pairwise (fun (x1 x2 : Fin (r + 1)) => x1 < x2) (j :: tail)) (hafter : ∀ z ∈ j :: tail, b ≤ z) (p : PolynomialSpace r n) (hp : (polarization r n a b) p = 0) : (polarization r n a b) ((AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (front ++ i :: j :: tail)) p) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathToggle.simpleRoot_polarization_path_first {r n : ℕ} (front : List (Fin (r + 1))) (i a b j : Fin (r + 1)) (tail : List (Fin (r + 1))) (hia : i < a) (hab : a < b) (hbj : b < j) (hfront : List.Pairwise (fun (x1 x2 : Fin (r + 1)) => x1 < x2) (front ++ [i])) (hbefore : ∀ z ∈ front ++ [i], z ≤ a) (htail : List.Pairwise (fun (x1 x2 : Fin (r + 1)) => x1 < x2) (j :: tail)) (hafter : ∀ z ∈ j :: tail, b ≤ z) (p : PolynomialSpace r n) (hp : (polarization r n a b) p = 0) : (polarization r n a b) ((AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (front ++ i :: a :: j :: tail)) p) = -MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathToggle.simpleRootToggleBridge✝ front i a b j tail p

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathToggle.simpleRoot_polarization_path_second {r n : ℕ} (front : List (Fin (r + 1))) (i a b j : Fin (r + 1)) (tail : List (Fin (r + 1))) (hia : i < a) (hab : a < b) (hbj : b < j) (hfront : List.Pairwise (fun (x1 x2 : Fin (r + 1)) => x1 < x2) (front ++ [i])) (hbefore : ∀ z ∈ front ++ [i], z ≤ a) (htail : List.Pairwise (fun (x1 x2 : Fin (r + 1)) => x1 < x2) (j :: tail)) (hafter : ∀ z ∈ j :: tail, b ≤ z) (p : PolynomialSpace r n) (hp : (polarization r n a b) p = 0) : (polarization r n a b) ((AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (front ++ i :: b :: j :: tail)) p) = MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathToggle.simpleRootToggleBridge✝ front i a b j tail p

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathToggle.simpleRoot_polarization_path_both {r n : ℕ} (front : List (Fin (r + 1))) (i a b j : Fin (r + 1)) (tail : List (Fin (r + 1))) (hia : i < a) (hab : a < b) (hbj : b < j) (hfront : List.Pairwise (fun (x1 x2 : Fin (r + 1)) => x1 < x2) (front ++ [i])) (hbefore : ∀ z ∈ front ++ [i], z ≤ a) (htail : List.Pairwise (fun (x1 x2 : Fin (r + 1)) => x1 < x2) (j :: tail)) (hafter : ∀ z ∈ j :: tail, b ≤ z) (p : PolynomialSpace r n) (A B : ℝ) (hp : (polarization r n a b) p = 0) (ha : (rowEuler r n a) ((AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (j :: tail)) p) = A • (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (j :: tail)) p) (hb : (rowEuler r n b) ((AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (j :: tail)) p) = B • (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (j :: tail)) p) : (polarization r n a b) ((AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (front ++ i :: a :: b :: j :: tail)) p) = (A - B + 1) • MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathToggle.simpleRootToggleBridge✝ front i a b j tail p

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathToggleCoordinate.simpleRoot_coordinate_mul_of_earlier {r n : ℕ} (a b start : Fin (r + 1)) (k : Fin n) (hstart : start < a) (hab : a < b) (q : PolynomialSpace r n) : (polarization r n a b) (MvPolynomial.X (variableIndex start k) * q) = MvPolynomial.X (variableIndex start k) * (polarization r n a b) q

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathToggleCoordinate.simpleRoot_coordinate_path_neither {r n : ℕ} (front : List (Fin (r + 1))) (start i a b j : Fin (r + 1)) (k : Fin n) (tail : List (Fin (r + 1))) (hstart : start < a) (hia : i < a) (hab : a < b) (hbj : b < j) (hfront : List.Pairwise (fun (x1 x2 : Fin (r + 1)) => x1 < x2) (front ++ [i])) (hbefore : ∀ z ∈ front ++ [i], z ≤ a) (htail : List.Pairwise (fun (x1 x2 : Fin (r + 1)) => x1 < x2) (j :: tail)) (hafter : ∀ z ∈ j :: tail, b ≤ z) (p : PolynomialSpace r n) (hp : (polarization r n a b) p = 0) : (polarization r n a b) (MvPolynomial.X (variableIndex start k) * (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (front ++ i :: j :: tail)) p) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathToggleCoordinate.simpleRoot_coordinate_path_first {r n : ℕ} (front : List (Fin (r + 1))) (start i a b j : Fin (r + 1)) (k : Fin n) (tail : List (Fin (r + 1))) (hstart : start < a) (hia : i < a) (hab : a < b) (hbj : b < j) (hfront : List.Pairwise (fun (x1 x2 : Fin (r + 1)) => x1 < x2) (front ++ [i])) (hbefore : ∀ z ∈ front ++ [i], z ≤ a) (htail : List.Pairwise (fun (x1 x2 : Fin (r + 1)) => x1 < x2) (j :: tail)) (hafter : ∀ z ∈ j :: tail, b ≤ z) (p : PolynomialSpace r n) (hp : (polarization r n a b) p = 0) : (polarization r n a b) (MvPolynomial.X (variableIndex start k) * (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (front ++ i :: a :: j :: tail)) p) = -MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathToggleCoordinate.coordinateToggleBridge✝ start k front i a b j tail p

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathToggleCoordinate.simpleRoot_coordinate_path_second {r n : ℕ} (front : List (Fin (r + 1))) (start i a b j : Fin (r + 1)) (k : Fin n) (tail : List (Fin (r + 1))) (hstart : start < a) (hia : i < a) (hab : a < b) (hbj : b < j) (hfront : List.Pairwise (fun (x1 x2 : Fin (r + 1)) => x1 < x2) (front ++ [i])) (hbefore : ∀ z ∈ front ++ [i], z ≤ a) (htail : List.Pairwise (fun (x1 x2 : Fin (r + 1)) => x1 < x2) (j :: tail)) (hafter : ∀ z ∈ j :: tail, b ≤ z) (p : PolynomialSpace r n) (hp : (polarization r n a b) p = 0) : (polarization r n a b) (MvPolynomial.X (variableIndex start k) * (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (front ++ i :: b :: j :: tail)) p) = MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathToggleCoordinate.coordinateToggleBridge✝ start k front i a b j tail p

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathToggleCoordinate.simpleRoot_coordinate_path_both {r n : ℕ} (front : List (Fin (r + 1))) (start i a b j : Fin (r + 1)) (k : Fin n) (tail : List (Fin (r + 1))) (hstart : start < a) (hia : i < a) (hab : a < b) (hbj : b < j) (hfront : List.Pairwise (fun (x1 x2 : Fin (r + 1)) => x1 < x2) (front ++ [i])) (hbefore : ∀ z ∈ front ++ [i], z ≤ a) (htail : List.Pairwise (fun (x1 x2 : Fin (r + 1)) => x1 < x2) (j :: tail)) (hafter : ∀ z ∈ j :: tail, b ≤ z) (p : PolynomialSpace r n) (A B : ℝ) (hp : (polarization r n a b) p = 0) (ha : (rowEuler r n a) ((AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (j :: tail)) p) = A • (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (j :: tail)) p) (hb : (rowEuler r n b) ((AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (j :: tail)) p) = B • (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (j :: tail)) p) : (polarization r n a b) (MvPolynomial.X (variableIndex start k) * (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (front ++ i :: a :: b :: j :: tail)) p) = (A - B + 1) • MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathToggleCoordinate.coordinateToggleBridge✝ start k front i a b j tail p

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathToggleCoordinate.simpleRoot_coordinate_path_four_states {r n : ℕ} (front : List (Fin (r + 1))) (start i a b j : Fin (r + 1)) (k : Fin n) (tail : List (Fin (r + 1))) (hstart : start < a) (hia : i < a) (hab : a < b) (hbj : b < j) (hfront : List.Pairwise (fun (x1 x2 : Fin (r + 1)) => x1 < x2) (front ++ [i])) (hbefore : ∀ z ∈ front ++ [i], z ≤ a) (htail : List.Pairwise (fun (x1 x2 : Fin (r + 1)) => x1 < x2) (j :: tail)) (hafter : ∀ z ∈ j :: tail, b ≤ z) (p : PolynomialSpace r n) (A B : ℝ) (hp : (polarization r n a b) p = 0) (ha : (rowEuler r n a) ((AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (j :: tail)) p) = A • (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (j :: tail)) p) (hb : (rowEuler r n b) ((AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (j :: tail)) p) = B • (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (j :: tail)) p) : (polarization r n a b) (MvPolynomial.X (variableIndex start k) * (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (front ++ i :: j :: tail)) p) = 0 ∧ (polarization r n a b) (MvPolynomial.X (variableIndex start k) * (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (front ++ i :: a :: j :: tail)) p) = -MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathToggleCoordinate.coordinateToggleBridge✝ start k front i a b j tail p ∧ (polarization r n a b) (MvPolynomial.X (variableIndex start k) * (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (front ++ i :: b :: j :: tail)) p) = MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathToggleCoordinate.coordinateToggleBridge✝ start k front i a b j tail p ∧ (polarization r n a b) (MvPolynomial.X (variableIndex start k) * (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (front ++ i :: a :: b :: j :: tail)) p) = (A - B + 1) • MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathToggleCoordinate.coordinateToggleBridge✝ start k front i a b j tail p

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathToggleCoordinate.simpleRoot_coordinate_path_neither_noFront {r n : ℕ} (a b j : Fin (r + 1)) (k : Fin n) (tail : List (Fin (r + 1))) (hab : a < b) (hbj : b < j) (htail : List.Pairwise (fun (x1 x2 : Fin (r + 1)) => x1 < x2) (j :: tail)) (hafter : ∀ z ∈ j :: tail, b ≤ z) (p : PolynomialSpace r n) (hp : (polarization r n a b) p = 0) : (polarization r n a b) (MvPolynomial.X (variableIndex j k) * (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (j :: tail)) p) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathToggleCoordinate.simpleRoot_coordinate_path_first_noFront {r n : ℕ} (a b j : Fin (r + 1)) (k : Fin n) (tail : List (Fin (r + 1))) (hab : a < b) (hbj : b < j) (htail : List.Pairwise (fun (x1 x2 : Fin (r + 1)) => x1 < x2) (j :: tail)) (hafter : ∀ z ∈ j :: tail, b ≤ z) (p : PolynomialSpace r n) (hp : (polarization r n a b) p = 0) : (polarization r n a b) (MvPolynomial.X (variableIndex a k) * (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (a :: j :: tail)) p) = -MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathToggleCoordinate.coordinateToggleBridgeNoFront✝ a b j k tail p

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathToggleCoordinate.simpleRoot_coordinate_path_second_noFront {r n : ℕ} (a b j : Fin (r + 1)) (k : Fin n) (tail : List (Fin (r + 1))) (hab : a < b) (hbj : b < j) (htail : List.Pairwise (fun (x1 x2 : Fin (r + 1)) => x1 < x2) (j :: tail)) (hafter : ∀ z ∈ j :: tail, b ≤ z) (p : PolynomialSpace r n) (hp : (polarization r n a b) p = 0) : (polarization r n a b) (MvPolynomial.X (variableIndex b k) * (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (b :: j :: tail)) p) = MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathToggleCoordinate.coordinateToggleBridgeNoFront✝ a b j k tail p

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathToggleCoordinate.simpleRoot_coordinate_path_both_noFront {r n : ℕ} (a b j : Fin (r + 1)) (k : Fin n) (tail : List (Fin (r + 1))) (hab : a < b) (hbj : b < j) (htail : List.Pairwise (fun (x1 x2 : Fin (r + 1)) => x1 < x2) (j :: tail)) (hafter : ∀ z ∈ j :: tail, b ≤ z) (p : PolynomialSpace r n) (A B : ℝ) (hp : (polarization r n a b) p = 0) (ha : (rowEuler r n a) ((AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (j :: tail)) p) = A • (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (j :: tail)) p) (hb : (rowEuler r n b) ((AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (j :: tail)) p) = B • (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (j :: tail)) p) : (polarization r n a b) (MvPolynomial.X (variableIndex a k) * (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (a :: b :: j :: tail)) p) = (A - B + 1) • MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathToggleCoordinate.coordinateToggleBridgeNoFront✝ a b j k tail p

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathToggleCoordinate.simpleRoot_coordinate_path_four_states_noFront {r n : ℕ} (a b j : Fin (r + 1)) (k : Fin n) (tail : List (Fin (r + 1))) (hab : a < b) (hbj : b < j) (htail : List.Pairwise (fun (x1 x2 : Fin (r + 1)) => x1 < x2) (j :: tail)) (hafter : ∀ z ∈ j :: tail, b ≤ z) (p : PolynomialSpace r n) (A B : ℝ) (hp : (polarization r n a b) p = 0) (ha : (rowEuler r n a) ((AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (j :: tail)) p) = A • (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (j :: tail)) p) (hb : (rowEuler r n b) ((AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (j :: tail)) p) = B • (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (j :: tail)) p) : (polarization r n a b) (MvPolynomial.X (variableIndex j k) * (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (j :: tail)) p) = 0 ∧ (polarization r n a b) (MvPolynomial.X (variableIndex a k) * (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (a :: j :: tail)) p) = -MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathToggleCoordinate.coordinateToggleBridgeNoFront✝ a b j k tail p ∧ (polarization r n a b) (MvPolynomial.X (variableIndex b k) * (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (b :: j :: tail)) p) = MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathToggleCoordinate.coordinateToggleBridgeNoFront✝ a b j k tail p ∧ (polarization r n a b) (MvPolynomial.X (variableIndex a k) * (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (a :: b :: j :: tail)) p) = (A - B + 1) • MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonPathToggleCoordinate.coordinateToggleBridgeNoFront✝ a b j k tail p

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonFourStatePathExtraction.rowEuler_lowerPolarizationPath_suffix_of_ne {r n : ℕ} (a target : Fin (r + 1)) (rows : List (Fin (r + 1))) (p : PolynomialSpace r n) (c : ℝ) (hp : (rowEuler r n a) p = c • p) (hatarget : a ≠ target) (hastart : a ≠ rows.headD target) : (rowEuler r n a) ((AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (rows ++ [target])) p) = c • (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (rows ++ [target])) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonFourStatePathExtraction.polarizationPathStart_eq_sort_headD {r : ℕ} (row : Fin (r + 1)) (S : Finset (Fin (r + 1))) : AllRankArbitraryRowBranchingOperator.polarizationPathStart row S = (S.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2).headD row

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonFourStatePathExtraction.arbitraryRowMickelssonPathTerm_four_states {r n : ℕ} (lam : Fin (r + 1) → ℕ) (row a b : Fin (r + 1)) (k : Fin n) (p : PolynomialSpace r n) (habadj : ↑a + 1 = ↑b) (hbrow : b < row) (hdom : lam b ≤ lam a) (hweight : ∀ (i : Fin (r + 1)), (rowEuler r n i) p = ↑(lam i) • p) (hhighest : (polarization r n a b) p = 0) (T : Finset (Fin (r + 1))) (hT : T ∈ (((AllRankArbitraryRowBranchingOperator.precedingRows row).erase a).erase b).powerset) : ∃ (z : PolynomialSpace r n), (polarization r n a b) (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonFourStatePathExtraction.actualMickelssonPathTerm✝ row k T p) = 0 ∧ (polarization r n a b) (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonFourStatePathExtraction.actualMickelssonPathTerm✝ row k (insert a T) p) = -z ∧ (polarization r n a b) (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonFourStatePathExtraction.actualMickelssonPathTerm✝ row k (insert b T) p) = z ∧ (polarization r n a b) (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonFourStatePathExtraction.actualMickelssonPathTerm✝ row k (insert a (insert b T)) p) = (↑(lam a - lam b) + 1) • z

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonLastRoot.precedingRows_succ {r : ℕ} (a : Fin r) : AllRankArbitraryRowBranchingOperator.precedingRows a.succ = insert a.castSucc (AllRankArbitraryRowBranchingOperator.precedingRows a.castSucc)

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonLastRoot.shiftedRowGap_succ_castSucc {r : ℕ} (lam : Fin (r + 1) → ℕ) (a : Fin r) : AllRankArbitraryRowBranchingOperator.shiftedRowGap lam a.succ a.castSucc = ↑(lam a.castSucc - lam a.succ)

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonLastRoot.sort_insert_last_of_preceding {r : ℕ} (a : Fin r) (S : Finset (Fin (r + 1))) (hS : S ⊆ AllRankArbitraryRowBranchingOperator.precedingRows a.castSucc) : ((insert a.castSucc S).sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) = (S.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ [a.castSucc]

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonLastRoot.polarizationPathStart_insert_last {r : ℕ} (a : Fin r) (S : Finset (Fin (r + 1))) (hS : S.Nonempty) (hsub : S ⊆ AllRankArbitraryRowBranchingOperator.precedingRows a.castSucc) : AllRankArbitraryRowBranchingOperator.polarizationPathStart a.succ (insert a.castSucc S) = AllRankArbitraryRowBranchingOperator.polarizationPathStart a.succ S

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonLastRoot.polarization_lastRoot_lowerPath_without {r n : ℕ} (a : Fin r) (L : List (Fin (r + 1))) (hL : ∀ i ∈ L, i < a.castSucc) (hne : L ≠ []) (p : PolynomialSpace r n) (hp : (polarization r n a.castSucc a.succ) p = 0) : (polarization r n a.castSucc a.succ) ((AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (L ++ [a.succ])) p) = (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (L ++ [a.castSucc])) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonLastRoot.polarization_lastRoot_lowerPath_with {r n : ℕ} (lam : Fin (r + 1) → ℕ) (a : Fin r) (L : List (Fin (r + 1))) (hL : ∀ i ∈ L, i < a.castSucc) (hdom : lam a.succ ≤ lam a.castSucc) (p : PolynomialSpace r n) (hweight : ∀ (i : Fin (r + 1)), (rowEuler r n i) p = ↑(lam i) • p) (hp : (polarization r n a.castSucc a.succ) p = 0) : (polarization r n a.castSucc a.succ) ((AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (L ++ [a.castSucc, a.succ])) p) = ↑(lam a.castSucc - lam a.succ) • (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (L ++ [a.castSucc])) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonLastRoot.polarization_lastRoot_pathTerm_without {r n : ℕ} (a : Fin r) (k : Fin n) (S : Finset (Fin (r + 1))) (hsub : S ⊆ AllRankArbitraryRowBranchingOperator.precedingRows a.castSucc) (p : PolynomialSpace r n) (hp : (polarization r n a.castSucc a.succ) p = 0) : (polarization r n a.castSucc a.succ) (MvPolynomial.X (variableIndex (AllRankArbitraryRowBranchingOperator.polarizationPathStart a.succ S) k) * (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath ((S.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ [a.succ])) p) = MvPolynomial.X (variableIndex (AllRankArbitraryRowBranchingOperator.polarizationPathStart a.succ (insert a.castSucc S)) k) * (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath ((S.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ [a.castSucc])) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonLastRoot.polarization_lastRoot_pathTerm_with {r n : ℕ} (lam : Fin (r + 1) → ℕ) (a : Fin r) (k : Fin n) (S : Finset (Fin (r + 1))) (hsub : S ⊆ AllRankArbitraryRowBranchingOperator.precedingRows a.castSucc) (hdom : lam a.succ ≤ lam a.castSucc) (p : PolynomialSpace r n) (hweight : ∀ (i : Fin (r + 1)), (rowEuler r n i) p = ↑(lam i) • p) (hp : (polarization r n a.castSucc a.succ) p = 0) : (polarization r n a.castSucc a.succ) (MvPolynomial.X (variableIndex (AllRankArbitraryRowBranchingOperator.polarizationPathStart a.succ (insert a.castSucc S)) k) * (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (((insert a.castSucc S).sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ [a.succ])) p) = ↑(lam a.castSucc - lam a.succ) • (MvPolynomial.X (variableIndex (AllRankArbitraryRowBranchingOperator.polarizationPathStart a.succ (insert a.castSucc S)) k) * (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath ((S.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ [a.castSucc])) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonLastRoot.polarization_lastRoot_paired_terms {r n : ℕ} (lam : Fin (r + 1) → ℕ) (a : Fin r) (k : Fin n) (S : Finset (Fin (r + 1))) (hsub : S ⊆ AllRankArbitraryRowBranchingOperator.precedingRows a.castSucc) (hdom : lam a.succ ≤ lam a.castSucc) (p : PolynomialSpace r n) (hweight : ∀ (i : Fin (r + 1)), (rowEuler r n i) p = ↑(lam i) • p) (hp : (polarization r n a.castSucc a.succ) p = 0) : (polarization r n a.castSucc a.succ) (AllRankArbitraryRowBranchingOperator.polarizationPathCoefficient lam a.succ S • (MvPolynomial.X (variableIndex (AllRankArbitraryRowBranchingOperator.polarizationPathStart a.succ S) k) * (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath ((S.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ [a.succ])) p)) + (polarization r n a.castSucc a.succ) (AllRankArbitraryRowBranchingOperator.polarizationPathCoefficient lam a.succ (insert a.castSucc S) • (MvPolynomial.X (variableIndex (AllRankArbitraryRowBranchingOperator.polarizationPathStart a.succ (insert a.castSucc S)) k) * (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (((insert a.castSucc S).sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ [a.succ])) p)) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonLastRoot.arbitraryRowAxialRaise_polarization_lastRoot {r n : ℕ} (lam : Fin (r + 1) → ℕ) (a : Fin r) (k : Fin n) (hdom : lam a.succ ≤ lam a.castSucc) (p : PolynomialSpace r n) (hweight : ∀ (i : Fin (r + 1)), (rowEuler r n i) p = ↑(lam i) • p) (hhighest : ∀ (i j : Fin (r + 1)), i < j → (polarization r n i j) p = 0) : (polarization r n a.castSucc a.succ) ((AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam a.succ k) p) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSimpleRootPathCancellation.sum_powerset_pair {α : Type u_1} {M : Type u_2} [DecidableEq α] [AddCommMonoid M] (s : Finset α) (a b : α) (ha : a ∈ s) (hb : b ∈ s) (hab : a ≠ b) (f : Finset α → M) : ∑ t ∈ s.powerset, f t = ∑ t ∈ ((s.erase a).erase b).powerset, (f t + f (insert b t) + f (insert a t) + f (insert a (insert b t)))

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSimpleRootPathCancellation.sum_powerset_eq_zero_of_pair_states {α : Type u_1} {M : Type u_2} [DecidableEq α] [AddCommMonoid M] (s : Finset α) (a b : α) (ha : a ∈ s) (hb : b ∈ s) (hab : a ≠ b) (f : Finset α → M) (hstates : ∀ t ∈ ((s.erase a).erase b).powerset, f t + f (insert b t) + f (insert a t) + f (insert a (insert b t)) = 0) : ∑ t ∈ s.powerset, f t = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSimpleRootPathCancellation.arbitraryRowAxialRaise_eq_sum_pathTerm {r n : ℕ} (lam : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (k : Fin n) (p : PolynomialSpace r n) : (AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam row k) p = ∑ S ∈ (AllRankArbitraryRowBranchingOperator.precedingRows row).powerset, AllRankArbitraryRowBranchingOperator.polarizationPathCoefficient lam row S • MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSimpleRootPathCancellation.arbitraryRowMickelssonPathTerm✝ row k S p

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSimpleRootPathCancellation.arbitraryRowAxialRaise_polarization_initial_simpleRoot_of_states {r n : ℕ} (lam : Fin (r + 1) → ℕ) (row a b : Fin (r + 1)) (k : Fin n) (p : PolynomialSpace r n) (habadj : ↑a + 1 = ↑b) (hbrow : b < row) (hweight : lam b ≤ lam a) (hlow : lam row ≤ lam b) (hstates : ∀ T ∈ (((AllRankArbitraryRowBranchingOperator.precedingRows row).erase a).erase b).powerset, ∃ (z : PolynomialSpace r n), (polarization r n a b) (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSimpleRootPathCancellation.arbitraryRowMickelssonPathTerm✝ row k T p) = 0 ∧ (polarization r n a b) (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSimpleRootPathCancellation.arbitraryRowMickelssonPathTerm✝ row k (insert a T) p) = -z ∧ (polarization r n a b) (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSimpleRootPathCancellation.arbitraryRowMickelssonPathTerm✝ row k (insert b T) p) = z ∧ (polarization r n a b) (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSimpleRootPathCancellation.arbitraryRowMickelssonPathTerm✝ row k (insert a (insert b T)) p) = (↑(lam a - lam b) + 1) • z) : (polarization r n a b) ((AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam row k) p) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSimpleRootPathCancellation.arbitraryRowAxialRaise_polarization_of_initial_pathStates {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (row : Fin (r + 1)) (k : Fin n) (p : PolynomialSpace r n) (hweight : ∀ (a : Fin (r + 1)), (rowEuler r n a) p = ↑(lam a) • p) (hhighest : ∀ (a b : Fin (r + 1)), a < b → (polarization r n a b) p = 0) (hstates : ∀ (a : Fin r), a.succ < row → ∀ T ∈ (((AllRankArbitraryRowBranchingOperator.precedingRows row).erase a.castSucc).erase a.succ).powerset, ∃ (z : PolynomialSpace r n), (polarization r n a.castSucc a.succ) (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSimpleRootPathCancellation.arbitraryRowMickelssonPathTerm✝ row k T p) = 0 ∧ (polarization r n a.castSucc a.succ) (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSimpleRootPathCancellation.arbitraryRowMickelssonPathTerm✝ row k (insert a.castSucc T) p) = -z ∧ (polarization r n a.castSucc a.succ) (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSimpleRootPathCancellation.arbitraryRowMickelssonPathTerm✝ row k (insert a.succ T) p) = z ∧ (polarization r n a.castSucc a.succ) (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSimpleRootPathCancellation.arbitraryRowMickelssonPathTerm✝ row k (insert a.castSucc (insert a.succ T)) p) = (↑(lam a.castSucc - lam a.succ) + 1) • z) (a b : Fin (r + 1)) (hab : a < b) : (polarization r n a b) ((AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam row k) p) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSimpleRootPathCancellation.arbitraryRowAxialRaise_polarization {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (row : Fin (r + 1)) (k : Fin n) (p : PolynomialSpace r n) (hweight : ∀ (c : Fin (r + 1)), (rowEuler r n c) p = ↑(lam c) • p) (hhighest : ∀ (c d : Fin (r + 1)), c < d → (polarization r n c d) p = 0) (a b : Fin (r + 1)) (hab : a < b) : (polarization r n a b) ((AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam row k) p) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankInterlacingHighestWeightSeed.dominantAxialSchedule_tail {r : ℕ} (lam : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (rows : List (Fin (r + 1))) (hlegal : MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankInterlacingHighestWeightSeed.DominantAxialSchedule✝ lam (row :: rows)) : MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankInterlacingHighestWeightSeed.DominantAxialSchedule✝ (HigherChannel.raiseWeight lam row) rows

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankInterlacingHighestWeightSeed.dominantAxialSchedule_initial {r : ℕ} (lam : Fin (r + 1) → ℕ) (rows : List (Fin (r + 1))) (hlegal : MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankInterlacingHighestWeightSeed.DominantAxialSchedule✝ lam rows) : Antitone lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankInterlacingHighestWeightSeed.iteratedArbitraryRowAxialRaise_polarization_of_dominantSchedule {r n : ℕ} (lam : Fin (r + 1) → ℕ) (k : Fin n) (rows : List (Fin (r + 1))) (hlegal : MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankInterlacingHighestWeightSeed.DominantAxialSchedule✝ lam rows) (p : PolynomialSpace r n) (hweight : ∀ (i : Fin (r + 1)), (rowEuler r n i) p = ↑(lam i) • p) (hhighest : ∀ (i j : Fin (r + 1)), i < j → (polarization r n i j) p = 0) (a b : Fin (r + 1)) (hab : a < b) : (polarization r n a b) ((ArbitraryRowMickelssonGramIdeal.iteratedArbitraryRowAxialRaise lam k rows) p) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankInterlacingHighestWeightSeed.reverseInterlacingRowSchedule_dominantAxialSchedule {r : ℕ} {lam : Fin (r + 2) → ℕ} {mu : Fin (r + 1) → ℕ} (h : HigherRepresentationGraph.Interlaces lam mu) : MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankInterlacingHighestWeightSeed.DominantAxialSchedule✝ (ThreeRowYoungBranching.appendZeroWeight mu) (HigherYoungArbitraryRankInterlacingLegalSchedule.reverseInterlacingRowSchedule lam mu)

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankInterlacingHighestWeightSeed.reverseInterlacingPolynomialSeed_polarization {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (p : ↥(HarmonicYoungSpace mu)) (a b : Fin (r + 2)) (hab : a < b) : (polarization (r + 1) (n + 1) a b) ((ArbitraryRankReverseInterlacingPolynomialSeed.reverseInterlacingPolynomialSeed lam mu) p) = 0

theorem MetricCodes.Spherical.HigherYoungArbitraryRowAxialFiltrationIdeal.axisPolynomial_mem_lowerAxisIdeal {r n : ℕ} (k : Fin n) (row i : Fin (r + 1)) (hi : i < row) : MvPolynomial.X (HigherHarmonicYoung.variableIndex i k) ∈ MetricCodes.Spherical.HigherYoungArbitraryRowAxialFiltrationIdeal.lowerAxisIdeal✝ k row

theorem MetricCodes.Spherical.HigherYoungArbitraryRowAxialFiltrationIdeal.gram_le_lowerAxisGramIdeal {r n : ℕ} (k : Fin n) (row : Fin (r + 1)) : HigherHarmonicYoung.youngGramRadialIdeal r n ≤ MetricCodes.Spherical.HigherYoungArbitraryRowAxialFiltrationIdeal.lowerAxisGramIdeal✝ k row

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowAxialLeadingOrder.nonemptyMickelssonPathTerm_mem_lowerAxisIdeal {r n : ℕ} (row : Fin (r + 1)) (k : Fin n) (S : Finset (Fin (r + 1))) (hS : S.Nonempty) (hsub : S ⊆ AllRankArbitraryRowBranchingOperator.precedingRows row) (p : PolynomialSpace r n) : MvPolynomial.X (variableIndex (AllRankArbitraryRowBranchingOperator.polarizationPathStart row S) k) * (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath ((S.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ [row])) p ∈ MetricCodes.Spherical.HigherYoungArbitraryRowAxialFiltrationIdeal.lowerAxisIdeal✝ k row

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowAxialLeadingOrder.nonemptyMickelssonWeightedPathTerm_mem_lowerAxisIdeal {r n : ℕ} (lam : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (k : Fin n) (S : Finset (Fin (r + 1))) (hS : S.Nonempty) (hsub : S ⊆ AllRankArbitraryRowBranchingOperator.precedingRows row) (p : PolynomialSpace r n) : AllRankArbitraryRowBranchingOperator.polarizationPathCoefficient lam row S • (MvPolynomial.X (variableIndex (AllRankArbitraryRowBranchingOperator.polarizationPathStart row S) k) * (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath ((S.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ [row])) p) ∈ MetricCodes.Spherical.HigherYoungArbitraryRowAxialFiltrationIdeal.lowerAxisIdeal✝ k row

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowAxialLeadingOrder.emptyMickelssonPathTerm_eq_leading {r n : ℕ} (lam : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (k : Fin n) (p : PolynomialSpace r n) : AllRankArbitraryRowBranchingOperator.polarizationPathCoefficient lam row ∅ • (MvPolynomial.X (variableIndex (AllRankArbitraryRowBranchingOperator.polarizationPathStart row ∅) k) * (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath ((∅.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ [row])) p) = MvPolynomial.C (AllRankArbitraryRowBranchingOperator.arbitraryRowLeadingScalar lam row) * (MvPolynomial.X (variableIndex row k) * p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowAxialLeadingOrder.arbitraryRowAxialRaise_sub_leading_mul_mem_lowerAxisIdeal {r n : ℕ} (lam : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (k : Fin n) (p : PolynomialSpace r n) : (AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam row k) p - MvPolynomial.C (AllRankArbitraryRowBranchingOperator.arbitraryRowLeadingScalar lam row) * (MvPolynomial.X (variableIndex row k) * p) ∈ MetricCodes.Spherical.HigherYoungArbitraryRowAxialFiltrationIdeal.lowerAxisIdeal✝ k row

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowAxialLeadingOrder.arbitraryRowAxialRaise_sub_leading_mul_mem_lowerAxisGramIdeal {r n : ℕ} (lam : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (k : Fin n) (p : PolynomialSpace r n) : (AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam row k) p - MvPolynomial.C (AllRankArbitraryRowBranchingOperator.arbitraryRowLeadingScalar lam row) * (MvPolynomial.X (variableIndex row k) * p) ∈ MetricCodes.Spherical.HigherYoungArbitraryRowAxialFiltrationIdeal.lowerAxisGramIdeal✝ k row

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankGelfandTsetlinTriangularNormalForm.lowerAxisIdeal_mono {r n : ℕ} (k : Fin n) {i j : Fin (r + 1)} (hij : i ≤ j) : MetricCodes.Spherical.HigherYoungArbitraryRowAxialFiltrationIdeal.lowerAxisIdeal✝ k i ≤ MetricCodes.Spherical.HigherYoungArbitraryRowAxialFiltrationIdeal.lowerAxisIdeal✝ k j

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankGelfandTsetlinTriangularNormalForm.lowerAxisGramIdeal_mono {r n : ℕ} (k : Fin n) {i j : Fin (r + 1)} (hij : i ≤ j) : MetricCodes.Spherical.HigherYoungArbitraryRowAxialFiltrationIdeal.lowerAxisGramIdeal✝ k i ≤ MetricCodes.Spherical.HigherYoungArbitraryRowAxialFiltrationIdeal.lowerAxisGramIdeal✝ k j

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankGelfandTsetlinTriangularNormalForm.C_mul_mem_ideal_iff {r n : ℕ} (I : Ideal (PolynomialSpace r n)) {c : ℝ} (hc : c ≠ 0) (p : PolynomialSpace r n) : MvPolynomial.C c * p ∈ I ↔ p ∈ I

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankGelfandTsetlinTriangularNormalForm.arbitraryRowAxialRaise_not_mem_lowerAxisGramIdeal {r n : ℕ} (lam : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (k : Fin n) (hpositive : 0 < AllRankArbitraryRowBranchingOperator.arbitraryRowLeadingScalar lam row) (hregular : ∀ (q : PolynomialSpace r n), MvPolynomial.X (variableIndex row k) * q ∈ MetricCodes.Spherical.HigherYoungArbitraryRowAxialFiltrationIdeal.lowerAxisGramIdeal✝ k row ↔ q ∈ MetricCodes.Spherical.HigherYoungArbitraryRowAxialFiltrationIdeal.lowerAxisGramIdeal✝ k row) (p : PolynomialSpace r n) (hp : p ∉ MetricCodes.Spherical.HigherYoungArbitraryRowAxialFiltrationIdeal.lowerAxisGramIdeal✝ k row) : (AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam row k) p ∉ MetricCodes.Spherical.HigherYoungArbitraryRowAxialFiltrationIdeal.lowerAxisGramIdeal✝ k row

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankGelfandTsetlinTriangularNormalForm.iteratedArbitraryRowAxialRaise_not_mem_youngGramRadialIdeal_of_descending {r n : ℕ} (lam : Fin (r + 1) → ℕ) (k : Fin n) (rows : List (Fin (r + 1))) (bound : Fin (r + 1)) (hdescending : List.Pairwise (fun (x1 x2 : Fin (r + 1)) => x1 ≥ x2) rows) (hbounded : ∀ row ∈ rows, row ≤ bound) (hpositive : MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankGelfandTsetlinTriangularNormalForm.positiveLeadingAxialSchedule✝ lam rows) (hregular : ∀ (row : Fin (r + 1)) (q : PolynomialSpace r n), MvPolynomial.X (variableIndex row k) * q ∈ MetricCodes.Spherical.HigherYoungArbitraryRowAxialFiltrationIdeal.lowerAxisGramIdeal✝ k row ↔ q ∈ MetricCodes.Spherical.HigherYoungArbitraryRowAxialFiltrationIdeal.lowerAxisGramIdeal✝ k row) (p : PolynomialSpace r n) (hp : p ∉ MetricCodes.Spherical.HigherYoungArbitraryRowAxialFiltrationIdeal.lowerAxisGramIdeal✝ k bound) : (ArbitraryRowMickelssonGramIdeal.iteratedArbitraryRowAxialRaise lam k rows) p ∉ youngGramRadialIdeal r n

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonGramQuotient.rowAxis_not_mem_gramPair_weighted_leading_support_allRank {r n : ℕ} (hn : 2 * r < n) (row : Fin (r + 1)) (z : ArbitraryRankMixedTraceRegularity.UpperGramPair r) : variableIndex row (Fin.last n) ∉ ((weightedMonomialOrder (ArbitraryRankMixedTraceRegularity.gramVariableNatWeight r (n + 1))).degree (ArbitraryRankMixedTraceRegularity.gramPairPolynomial (n + 1) z)).support

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonGramQuotient.rowAxis_not_mem_gramQuadraticList_weighted_leading_support_allRank {r n : ℕ} (hn : 2 * r < n) (row : Fin (r + 1)) (g : PolynomialSpace r (n + 1)) (hg : g ∈ ArbitraryRankMixedTraceRegularity.gramQuadraticList r (n + 1)) : variableIndex row (Fin.last n) ∉ ((weightedMonomialOrder (ArbitraryRankMixedTraceRegularity.gramVariableNatWeight r (n + 1))).degree g).support

theorem MetricCodes.Spherical.HigherYoungArbitraryRankAxialAssociatedGraded.mem_lowerAxisPolynomialList_iff {r n : ℕ} (k : Fin n) (row : Fin (r + 1)) (p : HigherHarmonicYoung.PolynomialSpace r n) : p ∈ MetricCodes.Spherical.HigherYoungArbitraryRankAxialAssociatedGraded.lowerAxisPolynomialList✝ k row ↔ ∃ i < row, p = MvPolynomial.X (HigherHarmonicYoung.variableIndex i k)

theorem MetricCodes.Spherical.HigherYoungArbitraryRankAxialAssociatedGraded.lowerAxisPolynomialList_ideal {r n : ℕ} (k : Fin n) (row : Fin (r + 1)) : Ideal.ofList (MetricCodes.Spherical.HigherYoungArbitraryRankAxialAssociatedGraded.lowerAxisPolynomialList✝ k row) = MetricCodes.Spherical.HigherYoungArbitraryRowAxialFiltrationIdeal.lowerAxisIdeal✝ k row

theorem MetricCodes.Spherical.HigherYoungArbitraryRankAxialAssociatedGraded.lowerAxisGramPolynomialList_ideal {r n : ℕ} (k : Fin n) (row : Fin (r + 1)) : Ideal.ofList (MetricCodes.Spherical.HigherYoungArbitraryRankAxialAssociatedGraded.lowerAxisGramPolynomialList✝ k row) = MetricCodes.Spherical.HigherYoungArbitraryRowAxialFiltrationIdeal.lowerAxisGramIdeal✝ k row

theorem MetricCodes.Spherical.HigherYoungArbitraryRankAxialAssociatedGraded.lowerAxisGramPolynomialList_weighted_monic {r n : ℕ} (hn : 2 * r < n) (k : Fin n) (row : Fin (r + 1)) (p : HigherHarmonicYoung.PolynomialSpace r n) (hp : p ∈ MetricCodes.Spherical.HigherYoungArbitraryRankAxialAssociatedGraded.lowerAxisGramPolynomialList✝ k row) : (HigherHarmonicYoung.weightedMonomialOrder (HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramVariableNatWeight r n)).Monic p

theorem MetricCodes.Spherical.HigherYoungArbitraryRankAxialAssociatedGraded.lowerAxisPolynomialList_weighted_degree_pairwise_disjoint {r n : ℕ} (k : Fin n) (row : Fin (r + 1)) : List.Pairwise (fun (p q : MvPolynomial (Fin ((r + 1) * n)) ℝ) => Disjoint ((HigherHarmonicYoung.weightedMonomialOrder (HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramVariableNatWeight r n)).degree p).support ((HigherHarmonicYoung.weightedMonomialOrder (HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramVariableNatWeight r n)).degree q).support) (MetricCodes.Spherical.HigherYoungArbitraryRankAxialAssociatedGraded.lowerAxisPolynomialList✝ k row)

theorem MetricCodes.Spherical.HigherYoungArbitraryRankAxialAssociatedGraded.gramPairPolynomial_lowerAxis_weighted_degree_disjoint {r n : ℕ} (hn : 2 * r < n) (axisRow : Fin (r + 1)) (z : HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.UpperGramPair r) : Disjoint ((HigherHarmonicYoung.weightedMonomialOrder (HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramVariableNatWeight r (n + 1))).degree (HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramPairPolynomial (n + 1) z)).support ((HigherHarmonicYoung.weightedMonomialOrder (HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramVariableNatWeight r (n + 1))).degree (MvPolynomial.X (HigherHarmonicYoung.variableIndex axisRow (Fin.last n)))).support

theorem MetricCodes.Spherical.HigherYoungArbitraryRankAxialAssociatedGraded.lowerAxisGramPolynomialList_weighted_degree_pairwise_disjoint {r n : ℕ} (hn : 2 * r < n) (row : Fin (r + 1)) : List.Pairwise (fun (p q : MvPolynomial (Fin ((r + 1) * (n + 1))) ℝ) => Disjoint ((HigherHarmonicYoung.weightedMonomialOrder (HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramVariableNatWeight r (n + 1))).degree p).support ((HigherHarmonicYoung.weightedMonomialOrder (HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramVariableNatWeight r (n + 1))).degree q).support) (MetricCodes.Spherical.HigherYoungArbitraryRankAxialAssociatedGraded.lowerAxisGramPolynomialList✝ (Fin.last n) row)

theorem MetricCodes.Spherical.HigherYoungArbitraryRankAxialAssociatedGraded.selectedAxis_not_mem_lowerAxisGramPolynomialList_leading_support {r n : ℕ} (hn : 2 * r < n) (row : Fin (r + 1)) (p : HigherHarmonicYoung.PolynomialSpace r (n + 1)) (hp : p ∈ MetricCodes.Spherical.HigherYoungArbitraryRankAxialAssociatedGraded.lowerAxisGramPolynomialList✝ (Fin.last n) row) : HigherHarmonicYoung.variableIndex row (Fin.last n) ∉ ((HigherHarmonicYoung.weightedMonomialOrder (HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramVariableNatWeight r (n + 1))).degree p).support

theorem MetricCodes.Spherical.HigherYoungArbitraryRankAxialAssociatedGraded.lowerAxisGramIdeal_axis_mul_mem_iff {r n : ℕ} (hn : 2 * r < n) (row : Fin (r + 1)) (p : HigherHarmonicYoung.PolynomialSpace r (n + 1)) : MvPolynomial.X (HigherHarmonicYoung.variableIndex row (Fin.last n)) * p ∈ MetricCodes.Spherical.HigherYoungArbitraryRowAxialFiltrationIdeal.lowerAxisGramIdeal✝ (Fin.last n) row ↔ p ∈ MetricCodes.Spherical.HigherYoungArbitraryRowAxialFiltrationIdeal.lowerAxisGramIdeal✝ (Fin.last n) row

theorem MetricCodes.Spherical.HigherYoungIteratedAxialProjectionSemigroup.simultaneousHarmonicProjection_residual_mem_gram_of_two_le {r n m : ℕ} (hm : 2 ≤ m) (p : ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) m)) : ↑p - ↑↑((HigherHarmonicYoung.simultaneousHarmonicProjection r n m) p) ∈ HigherHarmonicYoung.youngGramRadialIdeal r n

theorem MetricCodes.Spherical.HigherYoungIteratedAxialProjectionSemigroup.harmonicYoung_eq_zero_of_mem_youngGramRadialIdeal {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (hp : ↑p ∈ HigherHarmonicYoung.youngGramRadialIdeal r n) : p = 0

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAxialTransverseRetraction.axialTransverseRetraction_X_castSucc {r n : ℕ} (i : Fin (r + 1)) (j : Fin n) : MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAxialTransverseRetraction.axialTransverseRetraction✝ (MvPolynomial.X (variableIndex i.castSucc j.castSucc)) = MvPolynomial.X (variableIndex i j)

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAxialTransverseRetraction.axialTransverseRetraction_X_lastCoordinate {r n : ℕ} (i : Fin (r + 2)) : MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAxialTransverseRetraction.axialTransverseRetraction✝ (MvPolynomial.X (variableIndex i (Fin.last n))) = 0

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAxialTransverseRetraction.axialTransverseRetraction_X_lastRow {r n : ℕ} (j : Fin (n + 1)) : MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAxialTransverseRetraction.axialTransverseRetraction✝ (MvPolynomial.X (variableIndex (Fin.last (r + 1)) j)) = 0

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAxialTransverseRetraction.axialTransverseRetraction_transversePolynomial {r n : ℕ} (p : PolynomialSpace r n) : MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAxialTransverseRetraction.axialTransverseRetraction✝ ((ThreeRowYoungBranching.transversePolynomial n) p) = p

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAxialTransverseRetraction.axialTransverseRetraction_terminalZeroSelectedBranch {r n : ℕ} (mu : Fin (r + 1) → ℕ) (p : ↥(HarmonicYoungSpace mu)) : MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAxialTransverseRetraction.axialTransverseRetraction✝ ↑((ArbitraryRankBranching.terminalZeroSelectedBranchIsometry mu) p) = ↑p

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAxialRetractionGramImage.axialTransverseRetraction_rowPairingPolynomial_castSucc {r n : ℕ} (i j : Fin (r + 1)) : MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAxialTransverseRetraction.axialTransverseRetraction✝ (rowPairingPolynomial i.castSucc j.castSucc) = rowPairingPolynomial i j

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAxialRetractionGramImage.axialTransverseRetraction_rowPairingPolynomial_last_left {r n : ℕ} (j : Fin (r + 2)) : MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAxialTransverseRetraction.axialTransverseRetraction✝ (rowPairingPolynomial (Fin.last (r + 1)) j) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAxialRetractionGramImage.axialTransverseRetraction_rowPairingPolynomial_last_right {r n : ℕ} (i : Fin (r + 2)) : MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAxialTransverseRetraction.axialTransverseRetraction✝ (rowPairingPolynomial i (Fin.last (r + 1))) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAxialRetractionGramImage.axialTransverseRetraction_rowPairingPolynomial_mem {r n : ℕ} (i j : Fin (r + 2)) : MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAxialTransverseRetraction.axialTransverseRetraction✝ (rowPairingPolynomial i j) ∈ youngGramRadialIdeal r n

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAxialRetractionGramImage.map_axialTransverseRetraction_youngGramRadialIdeal_le {r n : ℕ} : Ideal.map MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAxialTransverseRetraction.axialTransverseRetraction✝ (youngGramRadialIdeal (r + 1) (n + 1)) ≤ youngGramRadialIdeal r n

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAxialRetractionLowerIdeal.map_axialTransverseRetraction_lowerAxisIdeal_eq_bot {r n : ℕ} (row : Fin (r + 2)) : Ideal.map MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAxialTransverseRetraction.axialTransverseRetraction✝ (MetricCodes.Spherical.HigherYoungArbitraryRowAxialFiltrationIdeal.lowerAxisIdeal✝ (Fin.last n) row) = ⊥

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAxialRetractionLowerIdeal.map_axialTransverseRetraction_lowerAxisGramIdeal_le {r n : ℕ} (row : Fin (r + 2)) : Ideal.map MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAxialTransverseRetraction.axialTransverseRetraction✝ (MetricCodes.Spherical.HigherYoungArbitraryRowAxialFiltrationIdeal.lowerAxisGramIdeal✝ (Fin.last n) row) ≤ youngGramRadialIdeal r n

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAxialRetractionLowerIdeal.axialTransverseRetraction_mem_lowerAxisGramIdeal {r n : ℕ} (row : Fin (r + 2)) {p : PolynomialSpace (r + 1) (n + 1)} (hp : p ∈ MetricCodes.Spherical.HigherYoungArbitraryRowAxialFiltrationIdeal.lowerAxisGramIdeal✝ (Fin.last n) row) : MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAxialTransverseRetraction.axialTransverseRetraction✝ p ∈ youngGramRadialIdeal r n

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAxialTransverseSeedNonvanishing.terminalZeroSelectedBranch_not_mem_lowerAxisGramIdeal {r n : ℕ} (mu : Fin (r + 1) → ℕ) (row : Fin (r + 2)) (p : ↥(HarmonicYoungSpace mu)) (hp : p ≠ 0) : ↑((ArbitraryRankBranching.terminalZeroSelectedBranchIsometry mu) p) ∉ MetricCodes.Spherical.HigherYoungArbitraryRowAxialFiltrationIdeal.lowerAxisGramIdeal✝ (Fin.last n) row

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankInterlacingTriangularCoefficient.interlacingRowSchedule_pairwise_le {r : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) : List.Pairwise (fun (x1 x2 : Fin (r + 2)) => x1 ≤ x2) (HigherYoungArbitraryRankInterlacingGapSchedule.interlacingRowSchedule lam mu)

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankInterlacingTriangularCoefficient.reverseInterlacingRowSchedule_pairwise_ge {r : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) : List.Pairwise (fun (x1 x2 : Fin (r + 2)) => x1 ≥ x2) (HigherYoungArbitraryRankInterlacingLegalSchedule.reverseInterlacingRowSchedule lam mu)

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankInterlacingTriangularCoefficient.reverseInterlacingRowSchedule_prefix_count_le {r : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (pref suffix : List (Fin (r + 2))) (hdecomp : pref ++ suffix = HigherYoungArbitraryRankInterlacingLegalSchedule.reverseInterlacingRowSchedule lam mu) (row : Fin (r + 2)) : List.count row pref ≤ HigherYoungArbitraryRankInterlacingGapSchedule.interlacingGap lam mu row

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankInterlacingTriangularCoefficient.reverseInterlacingRowSchedule_prefix_leadingScalar_pos {r : ℕ} {lam : Fin (r + 2) → ℕ} {mu : Fin (r + 1) → ℕ} (h : HigherRepresentationGraph.Interlaces lam mu) (pref suffix : List (Fin (r + 2))) (row : Fin (r + 2)) (hdecomp : pref ++ row :: suffix = HigherYoungArbitraryRankInterlacingLegalSchedule.reverseInterlacingRowSchedule lam mu) : 0 < AllRankArbitraryRowBranchingOperator.arbitraryRowLeadingScalar (ArbitraryRowMickelssonGramIdeal.arbitraryRowPathWeight (ThreeRowYoungBranching.appendZeroWeight mu) pref) row

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankInterlacingTriangularCoefficient.reverseInterlacingRowSchedule_positiveLeading {r : ℕ} {lam : Fin (r + 2) → ℕ} {mu : Fin (r + 1) → ℕ} (h : HigherRepresentationGraph.Interlaces lam mu) : MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankGelfandTsetlinTriangularNormalForm.positiveLeadingAxialSchedule✝ (ThreeRowYoungBranching.appendZeroWeight mu) (HigherYoungArbitraryRankInterlacingLegalSchedule.reverseInterlacingRowSchedule lam mu)

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankInterlacingTriangularCoefficient.reverseInterlacingPolynomialSeed_not_mem_youngGramRadialIdeal {r n : ℕ} (hn : 2 * (r + 1) < n) {lam : Fin (r + 2) → ℕ} {mu : Fin (r + 1) → ℕ} (h : HigherRepresentationGraph.Interlaces lam mu) (p : ↥(HarmonicYoungSpace mu)) (hp : p ≠ 0) : (ArbitraryRankReverseInterlacingPolynomialSeed.reverseInterlacingPolynomialSeed lam mu) p ∉ youngGramRadialIdeal (r + 1) (n + 1)

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankHarmonicBranch.young_pderiv_eq_zero_of_isHomogeneous_zero {r n : ℕ} (x : Fin ((r + 1) * n)) (p : PolynomialSpace r n) (hp : MvPolynomial.IsHomogeneous p 0) : (MvPolynomial.pderiv x) p = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankHarmonicBranch.traceOperator_eq_zero_of_isHomogeneous_degree_lt_two {r n d : ℕ} (hd : d < 2) (p : PolynomialSpace r n) (hp : MvPolynomial.IsHomogeneous p d) (i j : Fin (r + 1)) : (traceOperator r n i j) p = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankHarmonicBranch.homogeneous_mem_youngGramRadialIdeal_eq_zero_of_degree_lt_two {r n d : ℕ} (hd : d < 2) (p : ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) d)) (hp : ↑p ∈ youngGramRadialIdeal r n) : p = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankHarmonicBranch.simultaneousHarmonicProjection_eq_zero_iff_gramIdeal_all_degree {r n d : ℕ} (p : ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) d)) : (simultaneousHarmonicProjection r n d) p = 0 ↔ ↑p ∈ youngGramRadialIdeal r n

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankHarmonicBranch.youngHarmonicLift_eq_zero_iff_gramIdeal_all_degree {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p : ↥(homogeneousYoungHighestWeightSubmodule lam)) : (youngHarmonicLift lam) p = 0 ↔ ↑↑p ∈ youngGramRadialIdeal r n

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankHarmonicBranch.harmonicBranchOfHighestWeightSeed_injective_iff_gramIdeal_all_degree {E : Type u_1} [AddCommGroup E] [Module ℝ E] {r n : ℕ} (lam : Fin (r + 1) → ℕ) (seed : E →ₗ[ℝ] ↥(homogeneousYoungHighestWeightSubmodule lam)) : Function.Injective ⇑(harmonicBranchOfHighestWeightSeed lam seed) ↔ ∀ (p : E), ↑↑(seed p) ∈ youngGramRadialIdeal r n → p = 0

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) : ↥(HarmonicYoungSpace mu) →ₗ[ℝ] ↥(HarmonicYoungSpace lam)

The reverse interlacing harmonic branch used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch_injective_iff_gramIdeal {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) : Function.Injective ⇑(reverseInterlacingHarmonicBranch lam mu h) ↔ ∀ (p : ↥(HarmonicYoungSpace mu)), (ArbitraryRankReverseInterlacingPolynomialSeed.reverseInterlacingPolynomialSeed lam mu) p ∈ youngGramRadialIdeal (r + 1) (n + 1) → p = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch_injective_of_not_mem {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hnonzero : ∀ (p : ↥(HarmonicYoungSpace mu)), p ≠ 0 → (ArbitraryRankReverseInterlacingPolynomialSeed.reverseInterlacingPolynomialSeed lam mu) p ∉ youngGramRadialIdeal (r + 1) (n + 1)) : Function.Injective ⇑(reverseInterlacingHarmonicBranch lam mu h)

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch_injective {r n : ℕ} (hn : 2 * (r + 1) < n) (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) : Function.Injective ⇑(reverseInterlacingHarmonicBranch lam mu h)

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGelfandTsetlinFibreNormalization.normalizedGelfandTsetlinFibre_apply {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (c : ℝ) (hc : 0 < c) (hgram : ∀ (p q : ↥(HarmonicYoungSpace mu)), inner ℝ ((ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch lam mu h) p) ((ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch lam mu h) q) = c * inner ℝ p q) (p : ↥(HarmonicYoungSpace mu)) : (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGelfandTsetlinFibreNormalization.normalizedGelfandTsetlinFibre✝ lam mu h c hc hgram) p = (√c)⁻¹ • (ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch lam mu h) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGelfandTsetlinFibreNormalization.normalizedGelfandTsetlinFibre_phase_pos {c : ℝ} (hc : 0 < c) : 0 < (√c)⁻¹

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGelfandTsetlinFibreNormalization.normalizedGelfandTsetlinFibre_channel_apply {r n : ℕ} (source target : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (hsource : HigherRepresentationGraph.Interlaces source mu) (htarget : HigherRepresentationGraph.Interlaces target mu) (sourceGram targetGram : ℝ) (hsourceGram : 0 < sourceGram) (htargetGram : 0 < targetGram) (hsourceInner : ∀ (p q : ↥(HarmonicYoungSpace mu)), inner ℝ ((ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch source mu hsource) p) ((ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch source mu hsource) q) = sourceGram * inner ℝ p q) (htargetInner : ∀ (p q : ↥(HarmonicYoungSpace mu)), inner ℝ ((ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch target mu htarget) p) ((ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch target mu htarget) q) = targetGram * inner ℝ p q) (channel : ↥(HarmonicYoungSpace source) →ₗ[ℝ] ↥(HarmonicYoungSpace target)) (coefficient : ℝ) (haxis : ∀ (p : ↥(HarmonicYoungSpace mu)), channel ((ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch source mu hsource) p) = coefficient • (ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch target mu htarget) p) (p : ↥(HarmonicYoungSpace mu)) : channel ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGelfandTsetlinFibreNormalization.normalizedGelfandTsetlinFibre✝ source mu hsource sourceGram hsourceGram hsourceInner) p) = (coefficient * √targetGram / √sourceGram) • (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGelfandTsetlinFibreNormalization.normalizedGelfandTsetlinFibre✝ target mu htarget targetGram htargetGram htargetInner) p

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.ambientCoordinateDerivation {r n : ℕ} (a b : Fin n) : Derivation ℝ (PolynomialSpace r n) (PolynomialSpace r n)

The ambient coordinate derivation used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.ambientCoordinateDerivation_apply {r n : ℕ} (a b : Fin n) (p : PolynomialSpace r n) : (ambientCoordinateDerivation a b) p = ∑ i : Fin (r + 1), MvPolynomial.X (variableIndex i a) * (MvPolynomial.pderiv (variableIndex i b)) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.ambientCoordinateDerivation_X {r n : ℕ} (a b c : Fin n) (i : Fin (r + 1)) : (ambientCoordinateDerivation a b) (MvPolynomial.X (variableIndex i c)) = if b = c then MvPolynomial.X (variableIndex i a) else 0

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.ambientRotation {r n : ℕ} (a b : Fin n) : Derivation ℝ (PolynomialSpace r n) (PolynomialSpace r n)

The ambient rotation used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.ambientRotation_apply {r n : ℕ} (a b : Fin n) (p : PolynomialSpace r n) : (ambientRotation a b) p = (ambientCoordinateDerivation a b) p - (ambientCoordinateDerivation b a) p

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.rowPolarizationDerivation_apply {r n : ℕ} (i j : Fin (r + 1)) (p : PolynomialSpace r n) : (MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.rowPolarizationDerivation✝ i j) p = (polarization r n i j) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.rowPolarizationDerivation_X {r n : ℕ} (i j k : Fin (r + 1)) (a : Fin n) : (MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.rowPolarizationDerivation✝ i j) (MvPolynomial.X (variableIndex k a)) = if j = k then MvPolynomial.X (variableIndex i a) else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.ambientCoordinateDerivation_rowPolarization_commutator {r n : ℕ} (a b : Fin n) (i j : Fin (r + 1)) : ⁅ambientCoordinateDerivation a b, MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.rowPolarizationDerivation✝ i j⁆ = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.ambientCoordinateDerivation_polarization_comm {r n : ℕ} (a b : Fin n) (i j : Fin (r + 1)) (p : PolynomialSpace r n) : (ambientCoordinateDerivation a b) ((polarization r n i j) p) = (polarization r n i j) ((ambientCoordinateDerivation a b) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.ambientRotation_polarization_comm {r n : ℕ} (a b : Fin n) (i j : Fin (r + 1)) (p : PolynomialSpace r n) : (ambientRotation a b) ((polarization r n i j) p) = (polarization r n i j) ((ambientRotation a b) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.ambientRotation_rowEuler_comm {r n : ℕ} (a b : Fin n) (i : Fin (r + 1)) (p : PolynomialSpace r n) : (ambientRotation a b) ((rowEuler r n i) p) = (rowEuler r n i) ((ambientRotation a b) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.traceOperator_ambientCoordinateDerivation {r n : ℕ} (i j : Fin (r + 1)) (a b : Fin n) (p : PolynomialSpace r n) : (traceOperator r n i j) ((ambientCoordinateDerivation a b) p) = (ambientCoordinateDerivation a b) ((traceOperator r n i j) p) + (MvPolynomial.pderiv (variableIndex j a)) ((MvPolynomial.pderiv (variableIndex i b)) p) + (MvPolynomial.pderiv (variableIndex i a)) ((MvPolynomial.pderiv (variableIndex j b)) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.ambientRotation_traceOperator_comm {r n : ℕ} (a b : Fin n) (i j : Fin (r + 1)) (p : PolynomialSpace r n) : (traceOperator r n i j) ((ambientRotation a b) p) = (ambientRotation a b) ((traceOperator r n i j) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.ambientRotation_mem_harmonicYoungSubmodule {r n : ℕ} (lam : Fin (r + 1) → ℕ) (a b : Fin n) {p : PolynomialSpace r n} (hp : p ∈ harmonicYoungSubmodule lam) : (ambientRotation a b) p ∈ harmonicYoungSubmodule lam

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.youngAmbientRotation {r n : ℕ} (lam : Fin (r + 1) → ℕ) (a b : Fin n) : ↥(HarmonicYoungSpace lam) →ₗ[ℝ] ↥(HarmonicYoungSpace lam)

The young ambient rotation used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.youngAmbientRotation_apply_coe {r n : ℕ} (lam : Fin (r + 1) → ℕ) (a b : Fin n) (p : ↥(HarmonicYoungSpace lam)) : ↑((youngAmbientRotation lam a b) p) = (ambientRotation a b) ↑p

theorem MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.ambientCoordinateDerivation_polynomialInner {r n : ℕ} (a b : Fin n) (p q : PolynomialSpace r n) : SpherePacking.Fischer.polynomialInner ((r + 1) * n) ((ambientCoordinateDerivation a b) p) q = SpherePacking.Fischer.polynomialInner ((r + 1) * n) p ((ambientCoordinateDerivation b a) q)

theorem MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.youngAmbientRotation_inner {r n : ℕ} (lam : Fin (r + 1) → ℕ) (a b : Fin n) (p q : ↥(HarmonicYoungSpace lam)) : inner ℝ ((youngAmbientRotation lam a b) p) q = -inner ℝ p ((youngAmbientRotation lam a b) q)

theorem MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.youngAmbientRotation_adjoint {r n : ℕ} (lam : Fin (r + 1) → ℕ) (a b : Fin n) : LinearMap.adjoint (youngAmbientRotation lam a b) = -youngAmbientRotation lam a b

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngClebschLower_adjoint_tmul {r n : ℕ} (mu lam : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), lam i = ∑ i : Fin (r + 1), mu i + 1) (row : Fin (r + 1)) (v : SpherePacking.Euclidean n) (q : ↥(HarmonicYoungSpace mu)) : (LinearMap.adjoint (youngClebschLower mu lam hdeg row)) (v ⊗ₜ[ℝ] q) = (projectedCoordinateRaise lam mu hdeg row v) q

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.ClebschRotation.euclideanAmbientRotation {n : ℕ} (a b : Fin n) : SpherePacking.Euclidean n →ₗ[ℝ] SpherePacking.Euclidean n

The euclidean ambient rotation used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.ClebschRotation.euclideanAmbientRotation_apply {n : ℕ} (a b : Fin n) (v : SpherePacking.Euclidean n) : (euclideanAmbientRotation a b) v = v.ofLp b • (EuclideanSpace.basisFun (Fin n) ℝ) a - v.ofLp a • (EuclideanSpace.basisFun (Fin n) ℝ) b

theorem MetricCodes.Spherical.HigherHarmonicYoung.ClebschRotation.euclideanAmbientRotation_inner {n : ℕ} (a b : Fin n) (v w : SpherePacking.Euclidean n) : inner ℝ ((euclideanAmbientRotation a b) v) w = -inner ℝ v ((euclideanAmbientRotation a b) w)

theorem MetricCodes.Spherical.HigherHarmonicYoung.ClebschRotation.euclideanAmbientRotation_adjoint {n : ℕ} (a b : Fin n) : LinearMap.adjoint (euclideanAmbientRotation a b) = -euclideanAmbientRotation a b

theorem MetricCodes.Spherical.HigherHarmonicYoung.ClebschRotation.ambientRotation_polynomialInner {r n : ℕ} (a b : Fin n) (p q : PolynomialSpace r n) : SpherePacking.Fischer.polynomialInner ((r + 1) * n) ((MixedSignature.ambientRotation a b) p) q = -SpherePacking.Fischer.polynomialInner ((r + 1) * n) p ((MixedSignature.ambientRotation a b) q)

theorem MetricCodes.Spherical.HigherHarmonicYoung.ClebschRotation.ambientRotation_rowAxisPolynomial {r n : ℕ} (a b : Fin n) (row : Fin (r + 1)) (v : SpherePacking.Euclidean n) : (MixedSignature.ambientRotation a b) (rowAxisPolynomial row v) = rowAxisPolynomial row ((euclideanAmbientRotation a b) v)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.ClebschRotation.tensorAmbientRotation {r n : ℕ} (mu : Fin (r + 1) → ℕ) (a b : Fin n) : TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace mu) →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace mu)

The tensor ambient rotation used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.ClebschRotation.tensorAmbientRotation_tmul {r n : ℕ} (mu : Fin (r + 1) → ℕ) (a b : Fin n) (v : SpherePacking.Euclidean n) (p : ↥(HarmonicYoungSpace mu)) : (tensorAmbientRotation mu a b) (v ⊗ₜ[ℝ] p) = (euclideanAmbientRotation a b) v ⊗ₜ[ℝ] p + v ⊗ₜ[ℝ] (MixedSignature.youngAmbientRotation mu a b) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.ClebschRotation.tensorAmbientRotation_adjoint {r n : ℕ} (mu : Fin (r + 1) → ℕ) (a b : Fin n) : LinearMap.adjoint (tensorAmbientRotation mu a b) = -tensorAmbientRotation mu a b

theorem MetricCodes.Spherical.HigherHarmonicYoung.ClebschRotation.projectedCoordinateRaise_rotation {r n : ℕ} (mu lam : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), mu i = ∑ i : Fin (r + 1), lam i + 1) (row : Fin (r + 1)) (a b : Fin n) (v : SpherePacking.Euclidean n) (p : ↥(HarmonicYoungSpace lam)) : (MixedSignature.youngAmbientRotation mu a b) ((projectedCoordinateRaise mu lam hdeg row v) p) = (projectedCoordinateRaise mu lam hdeg row ((euclideanAmbientRotation a b) v)) p + (projectedCoordinateRaise mu lam hdeg row v) ((MixedSignature.youngAmbientRotation lam a b) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.ClebschRotation.projectedCoordinateLower_rotation {r n : ℕ} (mu lam : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), lam i = ∑ i : Fin (r + 1), mu i + 1) (row : Fin (r + 1)) (a b : Fin n) (v : SpherePacking.Euclidean n) (p : ↥(HarmonicYoungSpace lam)) : (MixedSignature.youngAmbientRotation mu a b) ((projectedCoordinateLower mu lam hdeg row v) p) = (projectedCoordinateLower mu lam hdeg row ((euclideanAmbientRotation a b) v)) p + (projectedCoordinateLower mu lam hdeg row v) ((MixedSignature.youngAmbientRotation lam a b) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.ClebschRotation.channel_rotation_intertwine_of_adjoint {r n : ℕ} (mu lam : Fin (r + 1) → ℕ) (T : ↥(HarmonicYoungSpace lam) →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace mu)) (a b : Fin n) (hT : ∀ (v : SpherePacking.Euclidean n) (q : ↥(HarmonicYoungSpace mu)), (MixedSignature.youngAmbientRotation lam a b) ((LinearMap.adjoint T) (v ⊗ₜ[ℝ] q)) = (LinearMap.adjoint T) ((tensorAmbientRotation mu a b) (v ⊗ₜ[ℝ] q))) : T ∘ₗ MixedSignature.youngAmbientRotation lam a b = tensorAmbientRotation mu a b ∘ₗ T

theorem MetricCodes.Spherical.HigherHarmonicYoung.ClebschRotation.youngClebschRaise_rotation_intertwine {r n : ℕ} (mu lam : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), mu i = ∑ i : Fin (r + 1), lam i + 1) (row : Fin (r + 1)) (a b : Fin n) : youngClebschRaise mu lam hdeg row ∘ₗ MixedSignature.youngAmbientRotation lam a b = tensorAmbientRotation mu a b ∘ₗ youngClebschRaise mu lam hdeg row

theorem MetricCodes.Spherical.HigherHarmonicYoung.ClebschRotation.youngClebschLower_rotation_intertwine {r n : ℕ} (mu lam : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), lam i = ∑ i : Fin (r + 1), mu i + 1) (row : Fin (r + 1)) (a b : Fin n) : youngClebschLower mu lam hdeg row ∘ₗ MixedSignature.youngAmbientRotation lam a b = tensorAmbientRotation mu a b ∘ₗ youngClebschLower mu lam hdeg row

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.TwoRowAxisChannelCoherence.phaseNegatedChannel_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (A : E →ₗᵢ[ℝ] F) (x : E) : (MetricCodes.Spherical.HigherHarmonicYoung.TwoRowAxisChannelCoherence.phaseNegatedChannel✝ A) x = -A x

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.TwoRowAxisChannelCoherence.phaseNegatedChannel_toLinearMap {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (A : E →ₗᵢ[ℝ] F) : (MetricCodes.Spherical.HigherHarmonicYoung.TwoRowAxisChannelCoherence.phaseNegatedChannel✝ A).toLinearMap = -1 • A.toLinearMap

theorem MetricCodes.Spherical.HigherHarmonicYoung.TwoRowAxisChannelCoherence.phaseNegatedChannel_adjoint_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] (A : E →ₗᵢ[ℝ] F) (y : F) : (LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.TwoRowAxisChannelCoherence.phaseNegatedChannel✝ A).toLinearMap) y = -(LinearMap.adjoint A.toLinearMap) y

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.youngAmbientCasimir {r n : ℕ} (lam : Fin (r + 1) → ℕ) : ↥(HarmonicYoungSpace lam) →ₗ[ℝ] ↥(HarmonicYoungSpace lam)

The young ambient casimir used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.youngAmbientCasimir_apply_coe {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p : ↥(HarmonicYoungSpace lam)) : ↑((youngAmbientCasimir lam) p) = MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.ambientCasimirPolynomial✝ ↑p

theorem MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.ambientCasimirPolynomial_eq_coordinateDerivations {r n : ℕ} (p : PolynomialSpace r n) : MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.ambientCasimirPolynomial✝ p = ∑ a : Fin n, ∑ b : Fin n, (ambientCoordinateDerivation a b) ((ambientCoordinateDerivation b a) p) - ∑ a : Fin n, ∑ b : Fin n, (ambientCoordinateDerivation a b) ((ambientCoordinateDerivation a b) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.ambientCoordinateDerivation_comp_apply_diagonal {r n : ℕ} (a b c d : Fin n) (p : PolynomialSpace r n) : (ambientCoordinateDerivation a b) ((ambientCoordinateDerivation c d) p) = (if b = c then (ambientCoordinateDerivation a d) p else 0) + ∑ i : Fin (r + 1), ∑ j : Fin (r + 1), MvPolynomial.X (variableIndex i a) * MvPolynomial.X (variableIndex j c) * (MvPolynomial.pderiv (variableIndex i b)) ((MvPolynomial.pderiv (variableIndex j d)) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.ambientCoordinateDerivation_sum_same {r n : ℕ} (p : PolynomialSpace r n) : ∑ a : Fin n, ∑ b : Fin n, (ambientCoordinateDerivation a b) ((ambientCoordinateDerivation a b) p) = ∑ i : Fin (r + 1), (rowEuler r n i) p + ∑ i : Fin (r + 1), ∑ j : Fin (r + 1), rowPairingPolynomial i j * (traceOperator r n i j) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.polarization_cross_square_expand {r n : ℕ} (i j : Fin (r + 1)) (p : PolynomialSpace r n) : (polarization r n i j) ((polarization r n j i) p) = (rowEuler r n i) p + ∑ a : Fin n, MvPolynomial.X (variableIndex i a) * (polarization r n j i) ((MvPolynomial.pderiv (variableIndex j a)) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.ambientCoordinateCrossPair {r n : ℕ} (i j : Fin (r + 1)) (p : PolynomialSpace r n) : ∑ a : Fin n, ∑ b : Fin n, MvPolynomial.X (variableIndex i a) * (MvPolynomial.pderiv (variableIndex i b)) (MvPolynomial.X (variableIndex j b) * (MvPolynomial.pderiv (variableIndex j a)) p) = (if i = j then ↑n • (rowEuler r n i) p else 0) + (polarization r n i j) ((polarization r n j i) p) - (rowEuler r n i) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.ambientCoordinateDerivation_sum_swap_eq_rowPolarizations {r n : ℕ} (p : PolynomialSpace r n) : ∑ a : Fin n, ∑ b : Fin n, (ambientCoordinateDerivation a b) ((ambientCoordinateDerivation b a) p) = ∑ i : Fin (r + 1), ∑ j : Fin (r + 1), ((if i = j then ↑n • (rowEuler r n i) p else 0) + (polarization r n i j) ((polarization r n j i) p) - (rowEuler r n i) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.ambientCasimirPolynomial_eq_rowHowe {r n : ℕ} (p : PolynomialSpace r n) : MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.ambientCasimirPolynomial✝ p = (↑n - ↑r - 2) • ∑ i : Fin (r + 1), (rowEuler r n i) p + ∑ i : Fin (r + 1), ∑ j : Fin (r + 1), (polarization r n i j) ((polarization r n j i) p) - ∑ i : Fin (r + 1), ∑ j : Fin (r + 1), rowPairingPolynomial i j * (traceOperator r n i j) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.youngAmbientRotationIntertwiner_square {r n : ℕ} (lam mu : Fin (r + 1) → ℕ) (A : ↥(HarmonicYoungSpace lam) →ₗ[ℝ] ↥(HarmonicYoungSpace mu)) (hA : MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.IsYoungAmbientRotationIntertwiner✝ lam mu A) (a b : Fin n) : A ∘ₗ youngAmbientRotation lam a b ∘ₗ youngAmbientRotation lam a b = (youngAmbientRotation mu a b ∘ₗ youngAmbientRotation mu a b) ∘ₗ A

theorem MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.linearMap_eq_zero_of_distinct_scalar_intertwining {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (A : E →ₗ[ℝ] F) (B : E →ₗ[ℝ] E) (C : F →ₗ[ℝ] F) (c d : ℝ) (hcomm : A ∘ₗ B = C ∘ₗ A) (hB : B = c • LinearMap.id) (hC : C = d • LinearMap.id) (hne : c ≠ d) : A = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.CrossGram.adjoint_intertwines_of_skew {E : Type u_1} {G : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup G] [InnerProductSpace ℝ G] [FiniteDimensional ℝ G] (A : E →ₗ[ℝ] G) (R : E →ₗ[ℝ] E) (S : G →ₗ[ℝ] G) (hR : LinearMap.adjoint R = -R) (hS : LinearMap.adjoint S = -S) (hA : A ∘ₗ R = S ∘ₗ A) : LinearMap.adjoint A ∘ₗ S = R ∘ₗ LinearMap.adjoint A

theorem MetricCodes.Spherical.HigherHarmonicYoung.CrossGram.crossGram_intertwines_of_skew {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [NormedAddCommGroup G] [InnerProductSpace ℝ G] [FiniteDimensional ℝ G] (A : E →ₗ[ℝ] G) (B : F →ₗ[ℝ] G) (R : E →ₗ[ℝ] E) (T : F →ₗ[ℝ] F) (S : G →ₗ[ℝ] G) (hR : LinearMap.adjoint R = -R) (hS : LinearMap.adjoint S = -S) (hA : A ∘ₗ R = S ∘ₗ A) (hB : B ∘ₗ T = S ∘ₗ B) : (LinearMap.adjoint A ∘ₗ B) ∘ₗ T = R ∘ₗ LinearMap.adjoint A ∘ₗ B

theorem MetricCodes.Spherical.HigherHarmonicYoung.CrossGram.young_crossGram_rotation_intertwine {r n : ℕ} (lam nu mu : Fin (r + 1) → ℕ) (A : ↥(HarmonicYoungSpace lam) →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace mu)) (B : ↥(HarmonicYoungSpace nu) →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace mu)) (S : Fin n → Fin n → TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace mu) →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace mu)) (hS : ∀ (a b : Fin n), LinearMap.adjoint (S a b) = -S a b) (hA : ∀ (a b : Fin n), A ∘ₗ MixedSignature.youngAmbientRotation lam a b = S a b ∘ₗ A) (hB : ∀ (a b : Fin n), B ∘ₗ MixedSignature.youngAmbientRotation nu a b = S a b ∘ₗ B) (a b : Fin n) : (LinearMap.adjoint A ∘ₗ B) ∘ₗ MixedSignature.youngAmbientRotation nu a b = MixedSignature.youngAmbientRotation lam a b ∘ₗ LinearMap.adjoint A ∘ₗ B

theorem MetricCodes.Spherical.HigherHarmonicYoung.boundaryYoungRotationIntertwiner_casimir {r n : ℕ} (lam mu : Fin (r + 1) → ℕ) (A : ↥(HarmonicYoungSpace lam) →ₗ[ℝ] ↥(HarmonicYoungSpace mu)) (hA : MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.IsYoungAmbientRotationIntertwiner✝ lam mu A) : A ∘ₗ MixedSignature.youngAmbientCasimir lam = MixedSignature.youngAmbientCasimir mu ∘ₗ A

theorem MetricCodes.Spherical.HigherHarmonicYoung.boundaryYoungRotationIntertwiner_eq_zero_of_distinctCasimir {r n : ℕ} (lam mu : Fin (r + 1) → ℕ) (A : ↥(HarmonicYoungSpace lam) →ₗ[ℝ] ↥(HarmonicYoungSpace mu)) (hA : MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.IsYoungAmbientRotationIntertwiner✝ lam mu A) (c d : ℝ) (hcasimirLam : MixedSignature.youngAmbientCasimir lam = c • LinearMap.id) (hcasimirMu : MixedSignature.youngAmbientCasimir mu = d • LinearMap.id) (hdistinct : c ≠ d) : A = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.boundaryYoungChannel_crossGram_eq_zero_of_distinctCasimir {r n : ℕ} (lam nu mu : Fin (r + 1) → ℕ) (A : ↥(HarmonicYoungSpace lam) →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace mu)) (B : ↥(HarmonicYoungSpace nu) →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace mu)) (S : Fin n → Fin n → TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace mu) →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace mu)) (hS : ∀ (a b : Fin n), LinearMap.adjoint (S a b) = -S a b) (hA : ∀ (a b : Fin n), A ∘ₗ MixedSignature.youngAmbientRotation lam a b = S a b ∘ₗ A) (hB : ∀ (a b : Fin n), B ∘ₗ MixedSignature.youngAmbientRotation nu a b = S a b ∘ₗ B) (c d : ℝ) (hcasimirLam : MixedSignature.youngAmbientCasimir lam = c • LinearMap.id) (hcasimirNu : MixedSignature.youngAmbientCasimir nu = d • LinearMap.id) (hdistinct : c ≠ d) : LinearMap.adjoint A ∘ₗ B = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.boundaryYoungChannel_smul_rotation_intertwine {r n : ℕ} (lam mu : Fin (r + 1) → ℕ) (A : ↥(HarmonicYoungSpace lam) →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace mu)) (S : Fin n → Fin n → TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace mu) →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace mu)) (hA : ∀ (a b : Fin n), A ∘ₗ MixedSignature.youngAmbientRotation lam a b = S a b ∘ₗ A) (c : ℝ) (a b : Fin n) : (c • A) ∘ₗ MixedSignature.youngAmbientRotation lam a b = S a b ∘ₗ (c • A)

theorem MetricCodes.Spherical.HigherHarmonicYoung.boundaryNormalizedYoungClebschRaise_rotation_intertwine {r n : ℕ} (mu lam : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), mu i = ∑ i : Fin (r + 1), lam i + 1) (row : Fin (r + 1)) (c : ℝ) (hc : 0 < c) (hgram : ∀ (p q : ↥(HarmonicYoungSpace lam)), inner ℝ ((youngClebschRaise mu lam hdeg row) p) ((youngClebschRaise mu lam hdeg row) q) = c * inner ℝ p q) (a b : Fin n) : (normalizedYoungClebschRaise mu lam hdeg row c hc hgram).toLinearMap ∘ₗ MixedSignature.youngAmbientRotation lam a b = ClebschRotation.tensorAmbientRotation mu a b ∘ₗ (normalizedYoungClebschRaise mu lam hdeg row c hc hgram).toLinearMap

theorem MetricCodes.Spherical.HigherHarmonicYoung.boundaryNormalizedYoungClebschLower_rotation_intertwine {r n : ℕ} (mu lam : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), lam i = ∑ i : Fin (r + 1), mu i + 1) (row : Fin (r + 1)) (c : ℝ) (hc : 0 < c) (hgram : ∀ (p q : ↥(HarmonicYoungSpace lam)), inner ℝ ((youngClebschLower mu lam hdeg row) p) ((youngClebschLower mu lam hdeg row) q) = c * inner ℝ p q) (a b : Fin n) : (normalizedYoungClebschLower mu lam hdeg row c hc hgram).toLinearMap ∘ₗ MixedSignature.youngAmbientRotation lam a b = ClebschRotation.tensorAmbientRotation mu a b ∘ₗ (normalizedYoungClebschLower mu lam hdeg row c hc hgram).toLinearMap

def MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.allRankCasimirEigenvalue {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) : ℝ

The all rank casimir eigenvalue used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.allRankCasimirEigenvalue n lam = ∑ i : Fin (r + 1), ↑(lam i) * (↑(lam i) + ↑n - 2 - 2 * ↑↑i)

theorem MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.polarization_opposite_on_harmonicYoung {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p : ↥(HarmonicYoungSpace lam)) (i j : Fin (r + 1)) : (polarization r n i j) ((polarization r n j i) ↑p) = (if i = j then ↑(lam i) ^ 2 else if i < j then ↑(lam i) - ↑(lam j) else 0) • ↑p

theorem MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.sum_upper_row_differences {r : ℕ} (f : Fin (r + 1) → ℝ) : (∑ i : Fin (r + 1), ∑ j : Fin (r + 1), if i < j then f i - f j else 0) = ∑ i : Fin (r + 1), (↑r - 2 * ↑↑i) * f i

theorem MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.polarization_opposite_sum_on_harmonicYoung {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p : ↥(HarmonicYoungSpace lam)) : ∑ i : Fin (r + 1), ∑ j : Fin (r + 1), (polarization r n i j) ((polarization r n j i) ↑p) = (∑ i : Fin (r + 1), (↑(lam i) ^ 2 + (↑r - 2 * ↑↑i) * ↑(lam i))) • ↑p

theorem MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.youngAmbientCasimir_allRank_eq_smul_id {r n : ℕ} (lam : Fin (r + 1) → ℕ) : youngAmbientCasimir lam = allRankCasimirEigenvalue n lam • LinearMap.id

def MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.adjacentCasimirEigenvalue {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) : ℝ

The adjacent casimir eigenvalue used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.adjacentCasimirEigenvalue n lam = ∑ row : Fin (r + 1), ↑(lam row) * (↑(lam row) + ↑n - 2 - 2 * ↑↑row)

theorem MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.adjacentCasimirEigenvalue_raiseWeight {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (row : Fin (r + 1)) : adjacentCasimirEigenvalue n (HigherChannel.raiseWeight lam row) = adjacentCasimirEigenvalue n lam + (2 * ↑(lam row) + ↑n - 1 - 2 * ↑↑row)

def MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.IsAllRankOneBoxNeighbor {r : ℕ} (target source : Fin (r + 1) → ℕ) : Prop

The predicate asserting all rank one box neighbor.

Equations

• One or more equations did not get rendered due to their size.

theorem MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.adjacentCasimirEigenvalue_raiseWeight_lt {r n : ℕ} (target : Fin (r + 1) → ℕ) (hdominant : Antitone target) (i j : Fin (r + 1)) (hij : i < j) : adjacentCasimirEigenvalue n (HigherChannel.raiseWeight target j) < adjacentCasimirEigenvalue n (HigherChannel.raiseWeight target i)

theorem MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.adjacentCasimirEigenvalue_raiseWeight_ne {r n : ℕ} (target : Fin (r + 1) → ℕ) (hdominant : Antitone target) (i j : Fin (r + 1)) (hij : i ≠ j) : adjacentCasimirEigenvalue n (HigherChannel.raiseWeight target i) ≠ adjacentCasimirEigenvalue n (HigherChannel.raiseWeight target j)

theorem MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.raiseWeight_injective_fixed_row {r : ℕ} (row : Fin (r + 1)) : Function.Injective fun (lam : Fin (r + 1) → ℕ) => HigherChannel.raiseWeight lam row

theorem MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.adjacentCasimirEigenvalue_lowerWeight_lt {r n : ℕ} (target source source' : Fin (r + 1) → ℕ) (hdominant : Antitone target) (i j : Fin (r + 1)) (hij : i < j) (hi : target = HigherChannel.raiseWeight source i) (hj : target = HigherChannel.raiseWeight source' j) : adjacentCasimirEigenvalue n source < adjacentCasimirEigenvalue n source'

theorem MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.adjacentCasimirEigenvalue_lower_lt_raise {r n : ℕ} (hn : 2 * r + 2 ≤ n) (target source : Fin (r + 1) → ℕ) (i j : Fin (r + 1)) (hsource : target = HigherChannel.raiseWeight source j) : adjacentCasimirEigenvalue n source < adjacentCasimirEigenvalue n (HigherChannel.raiseWeight target i)

theorem MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.adjacentCasimirEigenvalue_ne_of_distinct_oneBox_neighbors {r n : ℕ} (hn : 2 * r + 2 ≤ n) (target source source' : Fin (r + 1) → ℕ) (hdominant : Antitone target) (hsource : IsAllRankOneBoxNeighbor target source) (hsource' : IsAllRankOneBoxNeighbor target source') (hne : source ≠ source') : adjacentCasimirEigenvalue n source ≠ adjacentCasimirEigenvalue n source'

theorem MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.allRankYoungChannel_crossGram_eq_zero_of_oneBoxNeighbors {r n : ℕ} (hn : 2 * r + 2 ≤ n) (target source source' : Fin (r + 1) → ℕ) (hdominant : Antitone target) (hsource : IsAllRankOneBoxNeighbor target source) (hsource' : IsAllRankOneBoxNeighbor target source') (hne : source ≠ source') (A : ↥(HarmonicYoungSpace source) →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace target)) (B : ↥(HarmonicYoungSpace source') →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace target)) (hA : ∀ (a b : Fin n), A ∘ₗ youngAmbientRotation source a b = ClebschRotation.tensorAmbientRotation target a b ∘ₗ A) (hB : ∀ (a b : Fin n), B ∘ₗ youngAmbientRotation source' a b = ClebschRotation.tensorAmbientRotation target a b ∘ₗ B) : LinearMap.adjoint A ∘ₗ B = 0

theorem MetricCodes.Spherical.HigherYoungAllRankBoxSignatureNeighbors.boxSignature_injective {r m n : ℕ} (a : Fin (r + 1) → ℝ) : Function.Injective (HigherYoungActualGraphAssembly.boxSignature a n)

theorem MetricCodes.Spherical.HigherYoungAllRankBoxSignatureNeighbors.boxSignature_ne_of_ne {r m n : ℕ} (a : Fin (r + 1) → ℝ) {source source' : HigherYoungActualGraphAssembly.BoxIndex r m} (hne : source ≠ source') : HigherYoungActualGraphAssembly.boxSignature a n source ≠ HigherYoungActualGraphAssembly.boxSignature a n source'

theorem MetricCodes.Spherical.HigherYoungAllRankBoxSignatureNeighbors.boxProbability_positive_signature_oneBox {r m n : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (target source : HigherYoungActualGraphAssembly.BoxIndex r m) (hpositive : 0 < HigherHierarchyActualBoxSufficiency.boxProbability a b n target source) : ∃ (row : Fin (r + 1)), HigherYoungActualGraphAssembly.boxSignature a n source = HigherChannel.raiseWeight (HigherYoungActualGraphAssembly.boxSignature a n target) row ∨ HigherYoungActualGraphAssembly.boxSignature a n target = HigherChannel.raiseWeight (HigherYoungActualGraphAssembly.boxSignature a n source) row

theorem MetricCodes.Spherical.HigherYoungAllRankBoxSignatureNeighbors.boxSignature_antitone_of_finiteInterlacing {r m n : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (hstable : ∀ (v : HigherHierarchy.RectangularVertices.Vertex r m), HigherChannel.FiniteInterlacing n (HigherHierarchy.RectangularVertices.signature a n v) (HigherChannel.flooredCoordinates b n)) (target : HigherYoungActualGraphAssembly.BoxIndex r m) : Antitone (HigherYoungActualGraphAssembly.boxSignature a n target)

theorem MetricCodes.Spherical.HigherYoungAllRankBoxChannelOrthogonality.boxChannel_crossGram_eq_zero {r m n : ℕ} (a : Fin (r + 2) → ℝ) (b : Fin (r + 1) → ℝ) (hstable : ∀ (v : HigherHierarchy.RectangularVertices.Vertex (r + 1) m), HigherChannel.FiniteInterlacing n (HigherHierarchy.RectangularVertices.signature a n v) (HigherChannel.flooredCoordinates b n)) (target source source' : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) (h : 0 < HigherHierarchyActualBoxSufficiency.boxProbability a b n target source) (h' : 0 < HigherHierarchyActualBoxSufficiency.boxProbability a b n target source') (hne : source ≠ source') (A : HigherYoungMovingFibres.YoungVertex (HigherYoungActualGraphAssembly.boxSignature a n) source →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) (HigherYoungMovingFibres.YoungVertex (HigherYoungActualGraphAssembly.boxSignature a n) target)) (B : HigherYoungMovingFibres.YoungVertex (HigherYoungActualGraphAssembly.boxSignature a n) source' →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) (HigherYoungMovingFibres.YoungVertex (HigherYoungActualGraphAssembly.boxSignature a n) target)) (hA : ∀ (i j : Fin n), A ∘ₗ HigherHarmonicYoung.MixedSignature.youngAmbientRotation (HigherYoungActualGraphAssembly.boxSignature a n source) i j = HigherHarmonicYoung.ClebschRotation.tensorAmbientRotation (HigherYoungActualGraphAssembly.boxSignature a n target) i j ∘ₗ A) (hB : ∀ (i j : Fin n), B ∘ₗ HigherHarmonicYoung.MixedSignature.youngAmbientRotation (HigherYoungActualGraphAssembly.boxSignature a n source') i j = HigherHarmonicYoung.ClebschRotation.tensorAmbientRotation (HigherYoungActualGraphAssembly.boxSignature a n target) i j ∘ₗ B) : LinearMap.adjoint A ∘ₗ B = 0

theorem MetricCodes.Spherical.HigherYoungAllRankActualBoxInstantiation.boxSignature_interlaces {r m n : ℕ} (a : Fin (r + 2) → ℝ) (b : Fin (r + 1) → ℝ) (hstable : ∀ (v : HigherHierarchy.RectangularVertices.Vertex (r + 1) m), HigherChannel.FiniteInterlacing n (HigherHierarchy.RectangularVertices.signature a n v) (HigherChannel.flooredCoordinates b n)) (i : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) : HigherRepresentationGraph.Interlaces (HigherYoungActualGraphAssembly.boxSignature a n i) (HigherHierarchy.Weyl.flooredWeight b n)

theorem MetricCodes.Spherical.HigherYoungAllRankActualBoxInstantiation.boxVertex_eq_nextVertex_of_signature_raise {r m n : ℕ} (a : Fin (r + 1) → ℝ) (target source : HigherYoungActualGraphAssembly.BoxIndex r m) (row : Fin (r + 1)) (hrow : HigherYoungActualGraphAssembly.boxSignature a n source = HigherChannel.raiseWeight (HigherYoungActualGraphAssembly.boxSignature a n target) row) : ∃ (hstep : ↑((Fintype.equivFin (HigherHierarchy.RectangularVertices.Vertex r m)).symm target row) < m), (Fintype.equivFin (HigherHierarchy.RectangularVertices.Vertex r m)).symm source = HigherHierarchy.RectangularVertices.nextVertex ((Fintype.equivFin (HigherHierarchy.RectangularVertices.Vertex r m)).symm target) row hstep

theorem MetricCodes.Spherical.HigherYoungAllRankActualBoxInstantiation.boxProbability_eq_plus_of_signature_raise {r m n : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (target source : HigherYoungActualGraphAssembly.BoxIndex r m) (row : Fin (r + 1)) (hrow : HigherYoungActualGraphAssembly.boxSignature a n source = HigherChannel.raiseWeight (HigherYoungActualGraphAssembly.boxSignature a n target) row) : HigherHierarchyActualBoxSufficiency.boxProbability a b n target source = HigherChannel.plusProbability n (HigherYoungActualGraphAssembly.boxSignature a n target) (HigherChannel.flooredCoordinates b n) row

theorem MetricCodes.Spherical.HigherYoungAllRankActualBoxInstantiation.boxProbability_eq_minus_of_signature_raise {r m n : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (target source : HigherYoungActualGraphAssembly.BoxIndex r m) (row : Fin (r + 1)) (hrow : HigherYoungActualGraphAssembly.boxSignature a n target = HigherChannel.raiseWeight (HigherYoungActualGraphAssembly.boxSignature a n source) row) : HigherHierarchyActualBoxSufficiency.boxProbability a b n target source = HigherChannel.minusProbability n (HigherYoungActualGraphAssembly.boxSignature a n target) (HigherChannel.flooredCoordinates b n) row

theorem MetricCodes.Spherical.HigherYoungAllRankActualBoxInstantiation.box_stableRange {r m n : ℕ} (a : Fin (r + 2) → ℝ) (b : Fin (r + 1) → ℝ) (hstable : ∀ (v : HigherHierarchy.RectangularVertices.Vertex (r + 1) m), HigherChannel.FiniteInterlacing n (HigherHierarchy.RectangularVertices.signature a n v) (HigherChannel.flooredCoordinates b n)) : 2 * (r + 1) + 4 ≤ n

theorem MetricCodes.Spherical.HigherYoungAllRankActualBoxInstantiation.boxStabilizer_finrank_pos {r m n : ℕ} (a : Fin (r + 2) → ℝ) (b : Fin (r + 1) → ℝ) (hstable : ∀ (v : HigherHierarchy.RectangularVertices.Vertex (r + 1) m), HigherChannel.FiniteInterlacing n (HigherHierarchy.RectangularVertices.signature a n v) (HigherChannel.flooredCoordinates b n)) : 0 < Module.finrank ℝ ↥(HigherHierarchyActualBoxSufficiency.BoxStabilizer n b)

theorem MetricCodes.Spherical.HigherYoungAllRankActualBoxInstantiation.boxWeylDimensions_of_actualWeyl {r m n : ℕ} (a : Fin (r + 2) → ℝ) (b : Fin (r + 1) → ℝ) (hstable : ∀ (v : HigherHierarchy.RectangularVertices.Vertex (r + 1) m), HigherChannel.FiniteInterlacing n (HigherHierarchy.RectangularVertices.signature a n v) (HigherChannel.flooredCoordinates b n)) (hweyl : ∀ {k d : ℕ} (lam : Fin (k + 1) → ℕ), 2 * k + 4 ≤ d → Antitone lam → HigherHierarchy.Weyl.dimension d lam = ↑(Module.finrank ℝ ↥(HigherHarmonicYoung.HarmonicYoungSpace lam))) : HigherHierarchy.Weyl.dimension (n - 1) (HigherHierarchy.Weyl.flooredWeight b n) = ↑(Module.finrank ℝ ↥(HigherHierarchyActualBoxSufficiency.BoxStabilizer n b)) ∧ ∀ (i : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m), HigherHierarchy.Weyl.dimension n (HigherYoungActualGraphAssembly.boxSignature a n i) = ↑(Module.finrank ℝ (HigherYoungMovingFibres.YoungVertex (HigherYoungActualGraphAssembly.boxSignature a n) i))

noncomputable def MetricCodes.Spherical.HigherYoungAllRankActualBoxInstantiation.boxAxis (n : ℕ) (hn : 0 < n) : HigherProjectionInstantiation.SpherePoint n

The box axis used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

theorem MetricCodes.Spherical.HigherYoungAllRankActualBoxInstantiation.phaseCorrectedYoungChannel_adjoint_eq_sqrt {E : Type u_1} {G : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup G] [InnerProductSpace ℝ G] [FiniteDimensional ℝ G] (A : E →ₗᵢ[ℝ] G) (c p : ℝ) (hp : 0 ≤ p) (hc : c ^ 2 = p) (z : G) (v : E) (haxis : (LinearMap.adjoint A.toLinearMap) z = c • v) : (LinearMap.adjoint (MetricCodes.Spherical.HigherYoungAllRankActualBoxInstantiation.phaseCorrectedYoungChannel✝ A c).toLinearMap) z = √p • v

theorem MetricCodes.Spherical.HigherYoungAllRankActualBoxInstantiation.phaseCorrectedYoungChannel_rotation {r n : ℕ} (lam mu : Fin (r + 1) → ℕ) (A : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam) →ₗᵢ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HigherHarmonicYoung.HarmonicYoungSpace mu)) (c : ℝ) (hA : ∀ (a b : Fin n), A.toLinearMap ∘ₗ HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam a b = HigherHarmonicYoung.ClebschRotation.tensorAmbientRotation mu a b ∘ₗ A.toLinearMap) (a b : Fin n) : (MetricCodes.Spherical.HigherYoungAllRankActualBoxInstantiation.phaseCorrectedYoungChannel✝ A c).toLinearMap ∘ₗ HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam a b = HigherHarmonicYoung.ClebschRotation.tensorAmbientRotation mu a b ∘ₗ (MetricCodes.Spherical.HigherYoungAllRankActualBoxInstantiation.phaseCorrectedYoungChannel✝ A c).toLinearMap

structure MetricCodes.Spherical.HigherYoungAllRankActualBoxInstantiation.CoherentBoxSectorData {r m n : ℕ} (a : Fin (r + 2) → ℝ) (b : Fin (r + 1) → ℝ) (o : HigherProjectionInstantiation.SpherePoint n) (fibre : (i : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) → ↥(HigherHierarchyActualBoxSufficiency.BoxStabilizer n b) →ₗᵢ[ℝ] HigherYoungMovingFibres.YoungVertex (HigherYoungActualGraphAssembly.boxSignature a n) i) (target source : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) (h : 0 < HigherHierarchyActualBoxSufficiency.boxProbability a b n target source) : Type

Data encoding the coherent box sector construction.

• channel : HigherYoungMovingFibres.YoungVertex (HigherYoungActualGraphAssembly.boxSignature a n) source →ₗᵢ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) (HigherYoungMovingFibres.YoungVertex (HigherYoungActualGraphAssembly.boxSignature a n) target)

  The channel component.

• rotation (c d : Fin n) : self.channel.toLinearMap ∘ₗ HigherHarmonicYoung.MixedSignature.youngAmbientRotation (HigherYoungActualGraphAssembly.boxSignature a n source) c d = HigherHarmonicYoung.ClebschRotation.tensorAmbientRotation (HigherYoungActualGraphAssembly.boxSignature a n target) c d ∘ₗ self.channel.toLinearMap
• coefficient : ℝ

  The coefficient component.

• coefficient_sq : self.coefficient ^ 2 = HigherHierarchyActualBoxSufficiency.boxProbability a b n target source
• axis (x : HigherProjectionInstantiation.SpherePoint n) (v : ↥(HigherHierarchyActualBoxSufficiency.BoxStabilizer n b)) : (LinearMap.adjoint self.channel.toLinearMap) (↑x ⊗ₜ[ℝ] (HigherYoungMovingFibres.movingYoungFibre (HigherYoungActualGraphAssembly.boxSignature a n target) o (fibre target) x) v) = self.coefficient • (HigherYoungMovingFibres.movingYoungFibre (HigherYoungActualGraphAssembly.boxSignature a n source) o (fibre source) x) v

theorem MetricCodes.Spherical.HigherYoungAllRankActualBoxInstantiation.coherentBoxSector_phaseCorrected_axis {r m n : ℕ} (a : Fin (r + 2) → ℝ) (b : Fin (r + 1) → ℝ) (o : HigherProjectionInstantiation.SpherePoint n) (fibre : (i : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) → ↥(HigherHierarchyActualBoxSufficiency.BoxStabilizer n b) →ₗᵢ[ℝ] HigherYoungMovingFibres.YoungVertex (HigherYoungActualGraphAssembly.boxSignature a n) i) (target source : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) (h : 0 < HigherHierarchyActualBoxSufficiency.boxProbability a b n target source) (S : CoherentBoxSectorData a b o fibre target source h) (x : HigherProjectionInstantiation.SpherePoint n) (v : ↥(HigherHierarchyActualBoxSufficiency.BoxStabilizer n b)) : (LinearMap.adjoint (MetricCodes.Spherical.HigherYoungAllRankActualBoxInstantiation.phaseCorrectedYoungChannel✝ S.channel S.coefficient).toLinearMap) (↑x ⊗ₜ[ℝ] (HigherYoungMovingFibres.movingYoungFibre (HigherYoungActualGraphAssembly.boxSignature a n target) o (fibre target) x) v) = √(HigherHierarchyActualBoxSufficiency.boxProbability a b n target source) • (HigherYoungMovingFibres.movingYoungFibre (HigherYoungActualGraphAssembly.boxSignature a n source) o (fibre source) x) v

structure MetricCodes.Spherical.HigherYoungAllRankActualBoxInstantiation.BoxLoweringProjectedAxisWitness {r m n : ℕ} (a : Fin (r + 2) → ℝ) (b : Fin (r + 1) → ℝ) (o : HigherProjectionInstantiation.SpherePoint n) (fibre : (i : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) → ↥(HigherHierarchyActualBoxSufficiency.BoxStabilizer n b) →ₗᵢ[ℝ] HigherYoungMovingFibres.YoungVertex (HigherYoungActualGraphAssembly.boxSignature a n) i) (target source : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) (h : 0 < HigherHierarchyActualBoxSufficiency.boxProbability a b n target source) (row : Fin (r + 2)) (hdeg : ∑ i : Fin (r + 1 + 1), HigherYoungActualGraphAssembly.boxSignature a n source i = ∑ i : Fin (r + 1 + 1), HigherYoungActualGraphAssembly.boxSignature a n target i + 1) : Type

Data encoding the box lowering projected axis witness construction.

• gram : ℝ

  The gram component.

• gram_pos : 0 < self.gram
• gram_inner (p q : HigherYoungMovingFibres.YoungVertex (HigherYoungActualGraphAssembly.boxSignature a n) source) : inner ℝ ((HigherHarmonicYoung.youngClebschLower (HigherYoungActualGraphAssembly.boxSignature a n target) (HigherYoungActualGraphAssembly.boxSignature a n source) hdeg row) p) ((HigherHarmonicYoung.youngClebschLower (HigherYoungActualGraphAssembly.boxSignature a n target) (HigherYoungActualGraphAssembly.boxSignature a n source) hdeg row) q) = self.gram * inner ℝ p q
• coefficient : ℝ

  The coefficient component.

• coefficient_sq : self.coefficient ^ 2 = self.gram * HigherHierarchyActualBoxSufficiency.boxProbability a b n target source
• projected_axis (v : ↥(HigherHierarchyActualBoxSufficiency.BoxStabilizer n b)) : (HigherHarmonicYoung.projectedCoordinateRaise (HigherYoungActualGraphAssembly.boxSignature a n source) (HigherYoungActualGraphAssembly.boxSignature a n target) hdeg row ↑o) ((fibre target) v) = self.coefficient • (fibre source) v

structure MetricCodes.Spherical.HigherYoungAllRankActualBoxInstantiation.BoxRaisingProjectedAxisWitness {r m n : ℕ} (a : Fin (r + 2) → ℝ) (b : Fin (r + 1) → ℝ) (o : HigherProjectionInstantiation.SpherePoint n) (fibre : (i : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) → ↥(HigherHierarchyActualBoxSufficiency.BoxStabilizer n b) →ₗᵢ[ℝ] HigherYoungMovingFibres.YoungVertex (HigherYoungActualGraphAssembly.boxSignature a n) i) (target source : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) (h : 0 < HigherHierarchyActualBoxSufficiency.boxProbability a b n target source) (row : Fin (r + 2)) (hdeg : ∑ i : Fin (r + 1 + 1), HigherYoungActualGraphAssembly.boxSignature a n target i = ∑ i : Fin (r + 1 + 1), HigherYoungActualGraphAssembly.boxSignature a n source i + 1) : Type

Data encoding the box raising projected axis witness construction.

• gram : ℝ

  The gram component.

• gram_pos : 0 < self.gram
• gram_inner (p q : HigherYoungMovingFibres.YoungVertex (HigherYoungActualGraphAssembly.boxSignature a n) source) : inner ℝ ((HigherHarmonicYoung.youngClebschRaise (HigherYoungActualGraphAssembly.boxSignature a n target) (HigherYoungActualGraphAssembly.boxSignature a n source) hdeg row) p) ((HigherHarmonicYoung.youngClebschRaise (HigherYoungActualGraphAssembly.boxSignature a n target) (HigherYoungActualGraphAssembly.boxSignature a n source) hdeg row) q) = self.gram * inner ℝ p q
• coefficient : ℝ

  The coefficient component.

• coefficient_sq : self.coefficient ^ 2 = self.gram * HigherHierarchyActualBoxSufficiency.boxProbability a b n target source
• projected_axis (v : ↥(HigherHierarchyActualBoxSufficiency.BoxStabilizer n b)) : (HigherHarmonicYoung.projectedCoordinateLower (HigherYoungActualGraphAssembly.boxSignature a n source) (HigherYoungActualGraphAssembly.boxSignature a n target) hdeg row ↑o) ((fibre target) v) = self.coefficient • (fibre source) v

inductive MetricCodes.Spherical.HigherYoungAllRankActualBoxInstantiation.BoxProjectedAxisWitness {r m n : ℕ} (a : Fin (r + 2) → ℝ) (b : Fin (r + 1) → ℝ) (o : HigherProjectionInstantiation.SpherePoint n) (fibre : (i : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) → ↥(HigherHierarchyActualBoxSufficiency.BoxStabilizer n b) →ₗᵢ[ℝ] HigherYoungMovingFibres.YoungVertex (HigherYoungActualGraphAssembly.boxSignature a n) i) (target source : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) (h : 0 < HigherHierarchyActualBoxSufficiency.boxProbability a b n target source) : Type

Data encoding the box projected axis witness construction.

• lower {r m n : ℕ} {a : Fin (r + 2) → ℝ} {b : Fin (r + 1) → ℝ} {o : HigherProjectionInstantiation.SpherePoint n} {fibre : (i : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) → ↥(HigherHierarchyActualBoxSufficiency.BoxStabilizer n b) →ₗᵢ[ℝ] HigherYoungMovingFibres.YoungVertex (HigherYoungActualGraphAssembly.boxSignature a n) i} {target source : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m} {h : 0 < HigherHierarchyActualBoxSufficiency.boxProbability a b n target source} (row : Fin (r + 2)) (hdeg : ∑ i : Fin (r + 1 + 1), HigherYoungActualGraphAssembly.boxSignature a n source i = ∑ i : Fin (r + 1 + 1), HigherYoungActualGraphAssembly.boxSignature a n target i + 1) (data : BoxLoweringProjectedAxisWitness a b o fibre target source h row hdeg) : BoxProjectedAxisWitness a b o fibre target source h
• raise {r m n : ℕ} {a : Fin (r + 2) → ℝ} {b : Fin (r + 1) → ℝ} {o : HigherProjectionInstantiation.SpherePoint n} {fibre : (i : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) → ↥(HigherHierarchyActualBoxSufficiency.BoxStabilizer n b) →ₗᵢ[ℝ] HigherYoungMovingFibres.YoungVertex (HigherYoungActualGraphAssembly.boxSignature a n) i} {target source : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m} {h : 0 < HigherHierarchyActualBoxSufficiency.boxProbability a b n target source} (row : Fin (r + 2)) (hdeg : ∑ i : Fin (r + 1 + 1), HigherYoungActualGraphAssembly.boxSignature a n target i = ∑ i : Fin (r + 1 + 1), HigherYoungActualGraphAssembly.boxSignature a n source i + 1) (data : BoxRaisingProjectedAxisWitness a b o fibre target source h row hdeg) : BoxProjectedAxisWitness a b o fibre target source h

noncomputable def MetricCodes.Spherical.HigherYoungAllRankActualBoxInstantiation.boxRepresentationDataOfProjectedAxisWitnesses {r m n : ℕ} (a : Fin (r + 2) → ℝ) (b : Fin (r + 1) → ℝ) (hstable : ∀ (v : HigherHierarchy.RectangularVertices.Vertex (r + 1) m), HigherChannel.FiniteInterlacing n (HigherHierarchy.RectangularVertices.signature a n v) (HigherChannel.flooredCoordinates b n)) (hweyl : ∀ {k d : ℕ} (lam : Fin (k + 1) → ℕ), 2 * k + 4 ≤ d → Antitone lam → HigherHierarchy.Weyl.dimension d lam = ↑(Module.finrank ℝ ↥(HigherHarmonicYoung.HarmonicYoungSpace lam))) (o : HigherProjectionInstantiation.SpherePoint n) (fibre : (i : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) → ↥(HigherHierarchyActualBoxSufficiency.BoxStabilizer n b) →ₗᵢ[ℝ] HigherYoungMovingFibres.YoungVertex (HigherYoungActualGraphAssembly.boxSignature a n) i) (witness : (target source : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) → (h : 0 < HigherHierarchyActualBoxSufficiency.boxProbability a b n target source) → BoxProjectedAxisWitness a b o fibre target source h) : HigherHierarchyActualBoxSufficiency.BoxRepresentationData a b

The box representation data of projected axis witnesses used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.AllRankGelfandTsetlinAdjacentFibrePhase.adjacentNormalizedAxisCoefficient (sourceGram targetGram coefficient : ℝ) : ℝ

The adjacent normalized axis coefficient used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.AllRankGelfandTsetlinAdjacentFibrePhase.adjacentNormalizedAxisCoefficient sourceGram targetGram coefficient = coefficient * √targetGram / √sourceGram

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngHarmonicLift_fischer_inner {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p : ↥(homogeneousYoungHighestWeightSubmodule lam)) (q : ↥(HarmonicYoungSpace lam)) : inner ℝ ((youngHarmonicLift lam) p) q = SpherePacking.Fischer.polynomialInner ((r + 1) * n) ↑↑p ↑q

theorem MetricCodes.Spherical.HigherYoungMixedGapStabilizerRotationIntertwining.ambientRotation_addedAxisVariable {r n : ℕ} (a b : Fin n) (i : Fin (r + 1)) : (HigherHarmonicYoung.MixedSignature.ambientRotation a.castSucc b.castSucc) (MvPolynomial.X (HigherHarmonicYoung.variableIndex i (Fin.last n))) = 0

theorem MetricCodes.Spherical.HigherYoungArbitraryRankReverseInterlacingRotationIntertwining.ambientCoordinateDerivation_transversePolynomial {r n : ℕ} (a b : Fin n) (p : HigherHarmonicYoung.PolynomialSpace r n) : (HigherHarmonicYoung.MixedSignature.ambientCoordinateDerivation a.castSucc b.castSucc) ((ThreeRowYoungBranching.transversePolynomial n) p) = (ThreeRowYoungBranching.transversePolynomial n) ((HigherHarmonicYoung.MixedSignature.ambientCoordinateDerivation a b) p)

theorem MetricCodes.Spherical.HigherYoungArbitraryRankReverseInterlacingRotationIntertwining.ambientRotation_transversePolynomial {r n : ℕ} (a b : Fin n) (p : HigherHarmonicYoung.PolynomialSpace r n) : (HigherHarmonicYoung.MixedSignature.ambientRotation a.castSucc b.castSucc) ((ThreeRowYoungBranching.transversePolynomial n) p) = (ThreeRowYoungBranching.transversePolynomial n) ((HigherHarmonicYoung.MixedSignature.ambientRotation a b) p)

theorem MetricCodes.Spherical.HigherYoungArbitraryRankReverseInterlacingRotationIntertwining.ambientRotation_lowerPolarizationPath {r n : ℕ} (a b : Fin n) (path : List (Fin (r + 1))) (p : HigherHarmonicYoung.PolynomialSpace r n) : (HigherHarmonicYoung.MixedSignature.ambientRotation a b) ((HigherHarmonicYoung.AllRankArbitraryRowBranchingOperator.lowerPolarizationPath path) p) = (HigherHarmonicYoung.AllRankArbitraryRowBranchingOperator.lowerPolarizationPath path) ((HigherHarmonicYoung.MixedSignature.ambientRotation a b) p)

theorem MetricCodes.Spherical.HigherYoungArbitraryRankReverseInterlacingRotationIntertwining.ambientRotation_arbitraryRowAxialRaise {r n : ℕ} (lam : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (a b : Fin n) (p : HigherHarmonicYoung.PolynomialSpace r (n + 1)) : (HigherHarmonicYoung.MixedSignature.ambientRotation a.castSucc b.castSucc) ((HigherHarmonicYoung.AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam row (Fin.last n)) p) = (HigherHarmonicYoung.AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam row (Fin.last n)) ((HigherHarmonicYoung.MixedSignature.ambientRotation a.castSucc b.castSucc) p)

theorem MetricCodes.Spherical.HigherYoungArbitraryRankReverseInterlacingRotationIntertwining.ambientRotation_iteratedArbitraryRowAxialRaise {r n : ℕ} (lam : Fin (r + 1) → ℕ) (rows : List (Fin (r + 1))) (a b : Fin n) (p : HigherHarmonicYoung.PolynomialSpace r (n + 1)) : (HigherHarmonicYoung.MixedSignature.ambientRotation a.castSucc b.castSucc) ((HigherHarmonicYoung.ArbitraryRowMickelssonGramIdeal.iteratedArbitraryRowAxialRaise lam (Fin.last n) rows) p) = (HigherHarmonicYoung.ArbitraryRowMickelssonGramIdeal.iteratedArbitraryRowAxialRaise lam (Fin.last n) rows) ((HigherHarmonicYoung.MixedSignature.ambientRotation a.castSucc b.castSucc) p)

theorem MetricCodes.Spherical.HigherYoungArbitraryRankReverseInterlacingRotationIntertwining.reverseInterlacingPolynomialSeed_rotation_intertwine {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (a b : Fin n) (p : ↥(HigherHarmonicYoung.HarmonicYoungSpace mu)) : (HigherHarmonicYoung.MixedSignature.ambientRotation a.castSucc b.castSucc) ((HigherHarmonicYoung.ArbitraryRankReverseInterlacingPolynomialSeed.reverseInterlacingPolynomialSeed lam mu) p) = (HigherHarmonicYoung.ArbitraryRankReverseInterlacingPolynomialSeed.reverseInterlacingPolynomialSeed lam mu) ((HigherHarmonicYoung.MixedSignature.youngAmbientRotation mu a b) p)

def MetricCodes.Spherical.HigherYoungMixedGapLieGram.IsRotationInvariant {V : Type u_1} {I : Type u_2} [AddCommGroup V] [Module ℝ V] (R : I → V →ₗ[ℝ] V) (W : Submodule ℝ V) : Prop

The predicate asserting rotation invariant.

Equations

• MetricCodes.Spherical.HigherYoungMixedGapLieGram.IsRotationInvariant R W = ∀ (i : I), ∀ v ∈ W, (R i) v ∈ W

theorem MetricCodes.Spherical.HigherYoungMixedGapLieGram.rotationInvariant_orthogonal {V : Type u_1} {I : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (R : I → V →ₗ[ℝ] V) (hskew : ∀ (i : I) (v w : V), inner ℝ ((R i) v) w = -inner ℝ v ((R i) w)) (W : Submodule ℝ V) (hW : IsRotationInvariant R W) : IsRotationInvariant R Wᗮ

theorem MetricCodes.Spherical.HigherYoungMixedGapLieGram.rotationIntertwiner_eigenspace_invariant {V : Type u_1} {I : Type u_2} [AddCommGroup V] [Module ℝ V] (R : I → V →ₗ[ℝ] V) (A : V →ₗ[ℝ] V) (hA : ∀ (i : I), A ∘ₗ R i = R i ∘ₗ A) (c : ℝ) : IsRotationInvariant R (Module.End.eigenspace A c)

theorem MetricCodes.Spherical.HigherYoungMixedGapLieGram.symmetricRotationIntertwiner_eq_smul_id {V : Type u_1} {I : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] (R : I → V →ₗ[ℝ] V) (hirred : ∀ (W : Submodule ℝ V), IsRotationInvariant R W → W = ⊥ ∨ W = ⊤) (A : V →ₗ[ℝ] V) (hsymmetric : A.IsSymmetric) (hA : ∀ (i : I), A ∘ₗ R i = R i ∘ₗ A) : ∃ (c : ℝ), A = c • LinearMap.id

noncomputable def MetricCodes.Spherical.HigherYoungMixedGapLieGram.youngRotationFamily {r n : ℕ} (lam : Fin (r + 1) → ℕ) : Fin n × Fin n → ↥(HigherHarmonicYoung.HarmonicYoungSpace lam) →ₗ[ℝ] ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)

The young rotation family used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherYoungMixedGapLieGram.youngRotationFamily lam ab = MetricCodes.Spherical.HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam ab.1 ab.2

theorem MetricCodes.Spherical.HigherYoungMixedGapLieGram.youngRotationFamily_inner {r n : ℕ} (lam : Fin (r + 1) → ℕ) (ab : Fin n × Fin n) (p q : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) : inner ℝ ((youngRotationFamily lam ab) p) q = -inner ℝ p ((youngRotationFamily lam ab) q)

theorem MetricCodes.Spherical.HigherYoungAllRankGelfandTsetlinGramRotationCommutation.reverseInterlacingHarmonicBranchGram_rotation_commute {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (a b : Fin n) (hbranch : HigherHarmonicYoung.ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch lam mu h ∘ₗ HigherHarmonicYoung.MixedSignature.youngAmbientRotation mu a b = HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam a.castSucc b.castSucc ∘ₗ HigherHarmonicYoung.ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch lam mu h) : MetricCodes.Spherical.HigherYoungAllRankGelfandTsetlinGramRotationCommutation.reverseInterlacingHarmonicBranchGram✝ lam mu h ∘ₗ HigherHarmonicYoung.MixedSignature.youngAmbientRotation mu a b = HigherHarmonicYoung.MixedSignature.youngAmbientRotation mu a b ∘ₗ MetricCodes.Spherical.HigherYoungAllRankGelfandTsetlinGramRotationCommutation.reverseInterlacingHarmonicBranchGram✝ lam mu h

theorem MetricCodes.Spherical.HigherYoungAllRankGelfandTsetlinGramRotationCommutation.reverseInterlacingHarmonicBranchGram_isSymmetric {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) : (MetricCodes.Spherical.HigherYoungAllRankGelfandTsetlinGramRotationCommutation.reverseInterlacingHarmonicBranchGram✝ lam mu h).IsSymmetric

theorem MetricCodes.Spherical.HigherYoungAllRankGelfandTsetlinGramRotationCommutation.reverseInterlacingHarmonicBranchGram_inner_self {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (p : ↥(HigherHarmonicYoung.HarmonicYoungSpace mu)) : inner ℝ ((MetricCodes.Spherical.HigherYoungAllRankGelfandTsetlinGramRotationCommutation.reverseInterlacingHarmonicBranchGram✝ lam mu h) p) p = inner ℝ ((HigherHarmonicYoung.ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch lam mu h) p) ((HigherHarmonicYoung.ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch lam mu h) p)

theorem MetricCodes.Spherical.HigherYoungAllRankGelfandTsetlinGramRotationCommutation.reverseInterlacingHarmonicBranchGram_inner_self_pos {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hinjective : Function.Injective ⇑(HigherHarmonicYoung.ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch lam mu h)) (p : ↥(HigherHarmonicYoung.HarmonicYoungSpace mu)) (hp : p ≠ 0) : 0 < inner ℝ ((MetricCodes.Spherical.HigherYoungAllRankGelfandTsetlinGramRotationCommutation.reverseInterlacingHarmonicBranchGram✝ lam mu h) p) p

theorem MetricCodes.Spherical.HigherYoungAllRankGelfandTsetlinGramRotationCommutation.reverseInterlacingHarmonicBranchGram_eq_smul_id_of_irreducible {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hirred : ∀ (W : Submodule ℝ ↥(HigherHarmonicYoung.HarmonicYoungSpace mu)), HigherYoungMixedGapLieGram.IsRotationInvariant (HigherYoungMixedGapLieGram.youngRotationFamily mu) W → W = ⊥ ∨ W = ⊤) (hbranch : ∀ (a b : Fin n), HigherHarmonicYoung.ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch lam mu h ∘ₗ HigherHarmonicYoung.MixedSignature.youngAmbientRotation mu a b = HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam a.castSucc b.castSucc ∘ₗ HigherHarmonicYoung.ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch lam mu h) : ∃ (c : ℝ), MetricCodes.Spherical.HigherYoungAllRankGelfandTsetlinGramRotationCommutation.reverseInterlacingHarmonicBranchGram✝ lam mu h = c • LinearMap.id

theorem MetricCodes.Spherical.HigherYoungAllRankGelfandTsetlinGramRotationCommutation.reverseInterlacingHarmonicBranchGram_scalar_pos {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hinjective : Function.Injective ⇑(HigherHarmonicYoung.ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch lam mu h)) (p : ↥(HigherHarmonicYoung.HarmonicYoungSpace mu)) (hp : p ≠ 0) (c : ℝ) (hc : MetricCodes.Spherical.HigherYoungAllRankGelfandTsetlinGramRotationCommutation.reverseInterlacingHarmonicBranchGram✝ lam mu h = c • LinearMap.id) : 0 < c

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankHarmonicBranchRotationIntertwining.harmonicBranchOfHighestWeightSeed_rotation_intertwine {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (seed : ↥(HarmonicYoungSpace mu) →ₗ[ℝ] ↥(homogeneousYoungHighestWeightSubmodule lam)) (a b : Fin n) (hseed : ∀ (p : ↥(HarmonicYoungSpace mu)), (MixedSignature.ambientRotation a.castSucc b.castSucc) ↑↑(seed p) = ↑↑(seed ((MixedSignature.youngAmbientRotation mu a b) p))) : ArbitraryRankHarmonicBranch.harmonicBranchOfHighestWeightSeed lam seed ∘ₗ MixedSignature.youngAmbientRotation mu a b = MixedSignature.youngAmbientRotation lam a.castSucc b.castSucc ∘ₗ ArbitraryRankHarmonicBranch.harmonicBranchOfHighestWeightSeed lam seed

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankHarmonicBranchRotationIntertwining.reverseInterlacingHarmonicBranch_rotation_intertwine {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (a b : Fin n) : ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch lam mu h ∘ₗ MixedSignature.youngAmbientRotation mu a b = MixedSignature.youngAmbientRotation lam a.castSucc b.castSucc ∘ₗ ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch lam mu h

def MetricCodes.Spherical.HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) : Prop

The positive gelfand tsetlin fischer gram used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFischerGram {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : PositiveGelfandTsetlinFischerGram lam mu h) : ℝ

The canonical gelfand tsetlin fischer gram used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFischerGram lam mu h hgram = Classical.choose hgram

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFischerGram_pos {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : PositiveGelfandTsetlinFischerGram lam mu h) : 0 < canonicalGelfandTsetlinFischerGram lam mu h hgram

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFischerGram_inner {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : PositiveGelfandTsetlinFischerGram lam mu h) (p q : ↥(HarmonicYoungSpace mu)) : inner ℝ ((ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch lam mu h) p) ((ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch lam mu h) q) = canonicalGelfandTsetlinFischerGram lam mu h hgram * inner ℝ p q

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.positiveGelfandTsetlinFischerGram_of_irreducible {r n : ℕ} (hn : 2 * (r + 1) < n) (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hirred : ∀ (W : Submodule ℝ ↥(HarmonicYoungSpace mu)), HigherYoungMixedGapLieGram.IsRotationInvariant (HigherYoungMixedGapLieGram.youngRotationFamily mu) W → W = ⊥ ∨ W = ⊤) : PositiveGelfandTsetlinFischerGram lam mu h

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFibre {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : PositiveGelfandTsetlinFischerGram lam mu h) : ↥(HarmonicYoungSpace mu) →ₗᵢ[ℝ] ↥(HarmonicYoungSpace lam)

The canonical gelfand tsetlin fibre used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFibre_apply {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : PositiveGelfandTsetlinFischerGram lam mu h) (p : ↥(HarmonicYoungSpace mu)) : (canonicalGelfandTsetlinFibre lam mu h hgram) p = (√(canonicalGelfandTsetlinFischerGram lam mu h hgram))⁻¹ • (ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch lam mu h) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFibre_phase_pos {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : PositiveGelfandTsetlinFischerGram lam mu h) : 0 < (√(canonicalGelfandTsetlinFischerGram lam mu h hgram))⁻¹

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFibre_rotation_intertwine {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : PositiveGelfandTsetlinFischerGram lam mu h) (a b : Fin n) : (canonicalGelfandTsetlinFibre lam mu h hgram).toLinearMap ∘ₗ MixedSignature.youngAmbientRotation mu a b = MixedSignature.youngAmbientRotation lam a.castSucc b.castSucc ∘ₗ (canonicalGelfandTsetlinFibre lam mu h hgram).toLinearMap

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFibre_channel_apply {r n : ℕ} (source target : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (hsource : HigherRepresentationGraph.Interlaces source mu) (htarget : HigherRepresentationGraph.Interlaces target mu) (hsourceGram : PositiveGelfandTsetlinFischerGram source mu hsource) (htargetGram : PositiveGelfandTsetlinFischerGram target mu htarget) (channel : ↥(HarmonicYoungSpace source) →ₗ[ℝ] ↥(HarmonicYoungSpace target)) (coefficient : ℝ) (haxis : ∀ (p : ↥(HarmonicYoungSpace mu)), channel ((ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch source mu hsource) p) = coefficient • (ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch target mu htarget) p) (p : ↥(HarmonicYoungSpace mu)) : channel ((canonicalGelfandTsetlinFibre source mu hsource hsourceGram) p) = AllRankGelfandTsetlinAdjacentFibrePhase.adjacentNormalizedAxisCoefficient (canonicalGelfandTsetlinFischerGram source mu hsource hsourceGram) (canonicalGelfandTsetlinFischerGram target mu htarget htargetGram) coefficient • (canonicalGelfandTsetlinFibre target mu htarget htargetGram) p

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.canonicalBoxGelfandTsetlinFibre {r m n : ℕ} (a : Fin (r + 2) → ℝ) (b : Fin (r + 1) → ℝ) (hstable : ∀ (v : HigherHierarchy.RectangularVertices.Vertex (r + 1) m), HigherChannel.FiniteInterlacing n (HigherHierarchy.RectangularVertices.signature a n v) (HigherChannel.flooredCoordinates b n)) (hgram : ∀ (i : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m), PositiveGelfandTsetlinFischerGram (HigherYoungActualGraphAssembly.boxSignature a n i) (HigherHierarchy.Weyl.flooredWeight b n) ⋯) (i : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) : ↥(HigherHierarchyActualBoxSufficiency.BoxStabilizer n b) →ₗᵢ[ℝ] HigherYoungMovingFibres.YoungVertex (HigherYoungActualGraphAssembly.boxSignature a n) i

The canonical box gelfand tsetlin fibre used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankReverseProjectedFibreCoefficient.projectedCoordinateLower_fibre_inner_of_forward {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {r n : ℕ} (high low : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), high i = ∑ i : Fin (r + 1), low i + 1) (row : Fin (r + 1)) (axis : SpherePacking.Euclidean n) (lowFibre : E →ₗᵢ[ℝ] ↥(HarmonicYoungSpace low)) (highFibre : E →ₗᵢ[ℝ] ↥(HarmonicYoungSpace high)) (coefficient : ℝ) (hforward : ∀ (p : E), (projectedCoordinateRaise high low hdeg row axis) (lowFibre p) = coefficient • highFibre p) (p q : E) : inner ℝ (lowFibre p) ((projectedCoordinateLower low high hdeg row axis) (highFibre q)) = coefficient * inner ℝ p q

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankReverseProjectedFibreCoefficient.projectedCoordinateLower_fibre_eq_of_forward_of_mem_range {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {r n : ℕ} (high low : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), high i = ∑ i : Fin (r + 1), low i + 1) (row : Fin (r + 1)) (axis : SpherePacking.Euclidean n) (lowFibre : E →ₗᵢ[ℝ] ↥(HarmonicYoungSpace low)) (highFibre : E →ₗᵢ[ℝ] ↥(HarmonicYoungSpace high)) (coefficient : ℝ) (hforward : ∀ (p : E), (projectedCoordinateRaise high low hdeg row axis) (lowFibre p) = coefficient • highFibre p) (hrange : ∀ (q : E), (projectedCoordinateLower low high hdeg row axis) (highFibre q) ∈ lowFibre.range) (q : E) : (projectedCoordinateLower low high hdeg row axis) (highFibre q) = coefficient • lowFibre q

theorem MetricCodes.Spherical.HigherHarmonicYoung.BGGRootComplex.polarization_polarization_commutator {r n : ℕ} (a b c d : Fin (r + 1)) (p : PolynomialSpace r n) : (polarization r n a b) ((polarization r n c d) p) = ((polarization r n c d) ((polarization r n a b) p) + if b = c then (polarization r n a d) p else 0) - if d = a then (polarization r n c b) p else 0

theorem MetricCodes.Spherical.HigherYoungInternalRowPolarizationDescent.upperPolarization_internalRowDerivative {r n : ℕ} (lam : Fin (r + 1) → ℕ) (a b : Fin (r + 1)) (hab : a < b) (p : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (k : Fin n) : (HigherHarmonicYoung.polarization r n a b) ((MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a k)) ↑p) = -(MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex b k)) ↑p

def MetricCodes.Spherical.HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight {r : ℕ} (lam : Fin (r + 1) → ℕ) (a : Fin (r + 1)) : Fin (r + 1) → ℕ

The lowered internal young weight used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight lam a = Function.update lam a (lam a - 1)

@[simp]

theorem MetricCodes.Spherical.HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight_self {r : ℕ} (lam : Fin (r + 1) → ℕ) (a : Fin (r + 1)) : loweredInternalYoungWeight lam a a = lam a - 1

@[simp]

theorem MetricCodes.Spherical.HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight_of_ne {r : ℕ} (lam : Fin (r + 1) → ℕ) (a c : Fin (r + 1)) (hca : c ≠ a) : loweredInternalYoungWeight lam a c = lam c

theorem MetricCodes.Spherical.HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight_sum_add_one {r : ℕ} (lam : Fin (r + 1) → ℕ) (a : Fin (r + 1)) (ha : 0 < lam a) : ∑ c : Fin (r + 1), lam c = ∑ c : Fin (r + 1), loweredInternalYoungWeight lam a c + 1

theorem MetricCodes.Spherical.HigherYoungPenultimateRowProjectedLower.internalRowDerivative_mem_traceFree {r n : ℕ} (lam : Fin (r + 1) → ℕ) (a : Fin (r + 1)) (p : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (k : Fin n) : (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a k)) ↑p ∈ HigherHarmonicYoung.traceFreeSubmodule r n

@[simp]

theorem MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamShift_self {r : ℕ} (lam : Fin (r + 1) → ℕ) (a : Fin (r + 1)) : MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamShift✝ lam a a = 0

theorem MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamShift_pos {r : ℕ} (lam : Fin (r + 1) → ℕ) (a i : Fin (r + 1)) (hai : a < i) (hdom : lam i ≤ lam a) : 0 < MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamShift✝ lam a i

theorem MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamShift_ne_zero {r : ℕ} (lam : Fin (r + 1) → ℕ) (a i : Fin (r + 1)) (hai : a < i) (hdom : lam i ≤ lam a) : MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamShift✝ lam a i ≠ 0

theorem MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamCorrectedDerivative_eq {r n : ℕ} (lam : Fin (r + 1) → ℕ) (a : Fin (r + 1)) (p : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (k : Fin n) (i : Fin (r + 1)) : MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamCorrectedDerivative✝ lam a p k i = (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex i k)) ↑p + ∑ j : Fin (r + 1), if _h : i < j then (MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamShift✝ lam a j)⁻¹ • (HigherHarmonicYoung.polarization r n j i) (MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamCorrectedDerivative✝ lam a p k j) else 0

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankInternalRowLowerGram.mem_downstreamRows {r : ℕ} (row q : Fin (r + 1)) : q ∈ MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankInternalRowLowerGram.downstreamRows✝ row ↔ row < q

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankInternalRowLowerGram.internalRowLowerGramScalar {r : ℕ} (lam : Fin (r + 1) → ℕ) (row : Fin (r + 1)) : ℝ

The internal row lower gram scalar used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankInternalRowLowerGram.downstreamDenominator_pos {r : ℕ} (lam : Fin (r + 1) → ℕ) (row q : Fin (r + 1)) (hq : row < q) : 0 < MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankInternalRowLowerGram.downstreamDenominator✝ lam row q

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankInternalRowLowerGram.downstreamNumerator_pos {r : ℕ} (lam : Fin (r + 1) → ℕ) (row q : Fin (r + 1)) (hq : row < q) (hstrict : ∀ (j : Fin (r + 1)), ↑j = ↑row + 1 → lam j < lam row) : 0 < MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankInternalRowLowerGram.downstreamNumerator✝ lam row q

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankInternalRowLowerGram.internalRowLowerGramScalar_pos {r : ℕ} (lam : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hrow : 0 < lam row) (hstrict : ∀ (j : Fin (r + 1)), ↑j = ↑row + 1 → lam j < lam row) : 0 < internalRowLowerGramScalar lam row

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankInternalRowLowerGram.downstreamRows_last {r : ℕ} : MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankInternalRowLowerGram.downstreamRows✝ (Fin.last r) = ∅

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowProjectedLowerOperator.lowerPolarizationPath_fischer_adjoint {r n : ℕ} (path : List (Fin (r + 1))) (p q : PolynomialSpace r n) : SpherePacking.Fischer.polynomialInner ((r + 1) * n) ((AllRankArbitraryRowBranchingOperator.lowerPolarizationPath path) p) q = SpherePacking.Fischer.polynomialInner ((r + 1) * n) p ((MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowProjectedLowerOperator.upperPolarizationPath✝ path) q)

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowProjectedLowerOperator.arbitraryRowAxialLower_apply {r n : ℕ} (lam : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (k : Fin n) (q : PolynomialSpace r n) : (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowProjectedLowerOperator.arbitraryRowAxialLower✝ lam row k) q = ∑ S ∈ (AllRankArbitraryRowBranchingOperator.precedingRows row).powerset, AllRankArbitraryRowBranchingOperator.polarizationPathCoefficient lam row S • (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowProjectedLowerOperator.upperPolarizationPath✝ ((S.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ [row])) ((MvPolynomial.pderiv (variableIndex (AllRankArbitraryRowBranchingOperator.polarizationPathStart row S) k)) q)

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowProjectedLowerOperator.arbitraryRowAxialRaise_fischer_adjoint {r n : ℕ} (lam : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (k : Fin n) (p q : PolynomialSpace r n) : SpherePacking.Fischer.polynomialInner ((r + 1) * n) ((AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam row k) p) q = SpherePacking.Fischer.polynomialInner ((r + 1) * n) p ((MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowProjectedLowerOperator.arbitraryRowAxialLower✝ lam row k) q)

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowProjectedLowerOperator.upperPolarization_pderiv_of_highest {r n : ℕ} (i j : Fin (r + 1)) (hij : i < j) (k : Fin n) (q : PolynomialSpace r n) (hhighest : ∀ (a b : Fin (r + 1)), a < b → (polarization r n a b) q = 0) : (polarization r n i j) ((MvPolynomial.pderiv (variableIndex i k)) q) = -(MvPolynomial.pderiv (variableIndex j k)) q

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowProjectedLowerOperator.upperPolarizationPath_pderiv_of_highest {r n : ℕ} (row : Fin (r + 1)) (front : List (Fin (r + 1))) (k : Fin n) (q : PolynomialSpace r n) (hordered : List.Pairwise (fun (x1 x2 : Fin (r + 1)) => x1 < x2) (front ++ [row])) (hhighest : ∀ (a b : Fin (r + 1)), a < b → (polarization r n a b) q = 0) : (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowProjectedLowerOperator.upperPolarizationPath✝ (front ++ [row])) ((MvPolynomial.pderiv (variableIndex (front.headD row) k)) q) = (-1) ^ front.length • (MvPolynomial.pderiv (variableIndex row k)) q

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowProjectedLowerOperator.polarizationPathStart_eq_sort_headD {r : ℕ} (row : Fin (r + 1)) (S : Finset (Fin (r + 1))) : AllRankArbitraryRowBranchingOperator.polarizationPathStart row S = (S.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2).headD row

theorem MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamPathPairing.internalDerivative_downstreamPolarization_fischer_inner {r n : ℕ} (lam : Fin (r + 1) → ℕ) (i j : Fin (r + 1)) (hij : i < j) (p : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (v : HigherHarmonicYoung.PolynomialSpace r n) (k : Fin n) : SpherePacking.Fischer.polynomialInner ((r + 1) * n) ((MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex i k)) ↑p) ((HigherHarmonicYoung.polarization r n j i) v) = -SpherePacking.Fischer.polynomialInner ((r + 1) * n) ((MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex j k)) ↑p) v

theorem MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamPathPairing.downstreamCorrectedDerivative_fischer_cross_recurrence {r n : ℕ} (lam : Fin (r + 1) → ℕ) (a i : Fin (r + 1)) (p q : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (k : Fin n) : SpherePacking.Fischer.polynomialInner ((r + 1) * n) ((MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex i k)) ↑p) (MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamCorrectedDerivative✝ lam a q k i) = SpherePacking.Fischer.polynomialInner ((r + 1) * n) ((MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex i k)) ↑p) ((MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex i k)) ↑q) - ∑ j : Fin (r + 1), if _h : i < j then (MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamShift✝ lam a j)⁻¹ * SpherePacking.Fischer.polynomialInner ((r + 1) * n) ((MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex j k)) ↑p) (MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamCorrectedDerivative✝ lam a q k j) else 0

theorem MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamPathPairing.downstreamCorrectedDerivative_fischer_cross_sum_recurrence {r n : ℕ} (lam : Fin (r + 1) → ℕ) (a i : Fin (r + 1)) (p q : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) : ∑ k : Fin n, SpherePacking.Fischer.polynomialInner ((r + 1) * n) ((MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex i k)) ↑p) (MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamCorrectedDerivative✝ lam a q k i) = ↑(lam i) * inner ℝ p q - ∑ j : Fin (r + 1), if _h : i < j then (MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamShift✝ lam a j)⁻¹ * ∑ k : Fin n, SpherePacking.Fischer.polynomialInner ((r + 1) * n) ((MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex j k)) ↑p) (MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamCorrectedDerivative✝ lam a q k j) else 0

theorem MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamMembership.downstreamCorrectedDerivative_mem_traceFree {r n : ℕ} (lam : Fin (r + 1) → ℕ) (a : Fin (r + 1)) (p : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (k : Fin n) (i : Fin (r + 1)) : MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamCorrectedDerivative✝ lam a p k i ∈ HigherHarmonicYoung.traceFreeSubmodule r n

theorem MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamMembership.internalDerivative_rowEuler_shifted {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (k : Fin n) (i c : Fin (r + 1)) : (HigherHarmonicYoung.rowEuler r n c) ((MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex i k)) ↑p) = MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamMembership.loweredRowEigenvalue✝ lam i c • (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex i k)) ↑p

theorem MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamMembership.downstreamPolarization_rowEuler_shifted {r n : ℕ} (lam : Fin (r + 1) → ℕ) (i j c : Fin (r + 1)) (hij : i < j) (q : HigherHarmonicYoung.PolynomialSpace r n) (hq : (HigherHarmonicYoung.rowEuler r n c) q = MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamMembership.loweredRowEigenvalue✝ lam j c • q) : (HigherHarmonicYoung.rowEuler r n c) ((HigherHarmonicYoung.polarization r n j i) q) = MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamMembership.loweredRowEigenvalue✝ lam i c • (HigherHarmonicYoung.polarization r n j i) q

theorem MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamMembership.downstreamCorrectedDerivative_rowEuler {r n : ℕ} (lam : Fin (r + 1) → ℕ) (a : Fin (r + 1)) (p : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (k : Fin n) (i c : Fin (r + 1)) : (HigherHarmonicYoung.rowEuler r n c) (MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamCorrectedDerivative✝ lam a p k i) = MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamMembership.loweredRowEigenvalue✝ lam i c • MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamCorrectedDerivative✝ lam a p k i

theorem MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamMembership.downstreamCorrectedDerivative_source_rowEuler {r n : ℕ} (lam : Fin (r + 1) → ℕ) (a : Fin (r + 1)) (ha : 0 < lam a) (p : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (k : Fin n) (c : Fin (r + 1)) : (HigherHarmonicYoung.rowEuler r n c) (MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamCorrectedDerivative✝ lam a p k a) = ↑(HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight lam a c) • MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamCorrectedDerivative✝ lam a p k a

theorem MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamHarmonicMembership.downstreamCorrectedDerivative_source_mem_multihomogeneous {r n : ℕ} (lam : Fin (r + 1) → ℕ) (a : Fin (r + 1)) (ha : 0 < lam a) (p : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (k : Fin n) : MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamCorrectedDerivative✝ lam a p k a ∈ HigherHarmonicYoung.youngMultihomogeneousSubmodule n (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight lam a)

theorem MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamHarmonicMembership.downstreamCorrectedDerivative_source_mem_harmonicYoung_of_simpleRoots {r n : ℕ} (lam : Fin (r + 1) → ℕ) (a : Fin (r + 1)) (ha : 0 < lam a) (p : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (k : Fin n) (hsimple : ∀ (j : Fin r), (HigherHarmonicYoung.polarization r n j.castSucc j.succ) (MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamCorrectedDerivative✝ lam a p k a) = 0) : MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamCorrectedDerivative✝ lam a p k a ∈ HigherHarmonicYoung.harmonicYoungSubmodule (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight lam a)

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowDownstreamScalarTelescoping.downstreamScalar_backward_step (A current next leading tail : ℝ) (i : ℕ) (hden : A - next + ↑(i + 1) ≠ 0) : current - next + (1 - (A - next + ↑(i + 1))⁻¹) * (leading * tail - (A - next + ↑(i + 1))) = leading * (tail * MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowDownstreamScalarTelescoping.downstreamScalarFactor✝ A next i) - (A - current + ↑i)

@[simp]

theorem MetricCodes.Spherical.HigherYoungDownstreamFiniteIntervalSums.mem_strictDownstreamRows {m : ℕ} (i j : Fin m) : j ∈ MetricCodes.Spherical.HigherYoungDownstreamFiniteIntervalSums.strictDownstreamRows✝ i ↔ i < j

@[simp]

theorem MetricCodes.Spherical.HigherYoungDownstreamFiniteIntervalSums.mem_strictBetweenRows {m : ℕ} (i d j : Fin m) : j ∈ MetricCodes.Spherical.HigherYoungDownstreamFiniteIntervalSums.strictBetweenRows✝ i d ↔ i < j ∧ j < d

theorem MetricCodes.Spherical.HigherYoungDownstreamFiniteIntervalSums.strictBetweenRows_eq_Ioo {m : ℕ} (i d : Fin m) : MetricCodes.Spherical.HigherYoungDownstreamFiniteIntervalSums.strictBetweenRows✝ i d = Finset.Ioo i d

theorem MetricCodes.Spherical.HigherYoungDownstreamFiniteIntervalSums.card_strictBetweenRows {m : ℕ} (i d : Fin m) : (MetricCodes.Spherical.HigherYoungDownstreamFiniteIntervalSums.strictBetweenRows✝ i d).card = ↑d - ↑i - 1

theorem MetricCodes.Spherical.HigherYoungDownstreamFiniteIntervalSums.strictBetweenRows_eq_empty_of_succ {m : ℕ} (i d : Fin m) (hid : ↑d = ↑i + 1) : MetricCodes.Spherical.HigherYoungDownstreamFiniteIntervalSums.strictBetweenRows✝ i d = ∅

theorem MetricCodes.Spherical.HigherYoungDownstreamFiniteIntervalSums.disjoint_strictBetween_singleton {m : ℕ} (i d : Fin m) : Disjoint (MetricCodes.Spherical.HigherYoungDownstreamFiniteIntervalSums.strictBetweenRows✝ i d) {d}

theorem MetricCodes.Spherical.HigherYoungDownstreamFiniteIntervalSums.disjoint_strictBetween_downstream {m : ℕ} (i d : Fin m) : Disjoint (MetricCodes.Spherical.HigherYoungDownstreamFiniteIntervalSums.strictBetweenRows✝ i d) (MetricCodes.Spherical.HigherYoungDownstreamFiniteIntervalSums.strictDownstreamRows✝ d)

theorem MetricCodes.Spherical.HigherYoungDownstreamFiniteIntervalSums.disjoint_singleton_downstream {m : ℕ} (d : Fin m) : Disjoint {d} (MetricCodes.Spherical.HigherYoungDownstreamFiniteIntervalSums.strictDownstreamRows✝ d)

theorem MetricCodes.Spherical.HigherYoungDownstreamFiniteIntervalSums.disjoint_between_union_singleton_downstream {m : ℕ} (i d : Fin m) : Disjoint (MetricCodes.Spherical.HigherYoungDownstreamFiniteIntervalSums.strictBetweenRows✝ i d ∪ {d}) (MetricCodes.Spherical.HigherYoungDownstreamFiniteIntervalSums.strictDownstreamRows✝ d)

theorem MetricCodes.Spherical.HigherYoungDownstreamFiniteIntervalSums.strictDownstreamRows_eq_between_union_singleton_union_downstream {m : ℕ} (i d : Fin m) (hid : i < d) : MetricCodes.Spherical.HigherYoungDownstreamFiniteIntervalSums.strictDownstreamRows✝ i = MetricCodes.Spherical.HigherYoungDownstreamFiniteIntervalSums.strictBetweenRows✝ i d ∪ {d} ∪ MetricCodes.Spherical.HigherYoungDownstreamFiniteIntervalSums.strictDownstreamRows✝ d

theorem MetricCodes.Spherical.HigherYoungDownstreamFiniteIntervalSums.sum_strictDownstreamRows_eq_sum_between_add_add_downstream {m : ℕ} {A : Type u_1} [AddCommMonoid A] (i d : Fin m) (hid : i < d) (f : Fin m → A) : ∑ j ∈ MetricCodes.Spherical.HigherYoungDownstreamFiniteIntervalSums.strictDownstreamRows✝ i, f j = ∑ j ∈ MetricCodes.Spherical.HigherYoungDownstreamFiniteIntervalSums.strictBetweenRows✝ i d, f j + f d + ∑ j ∈ MetricCodes.Spherical.HigherYoungDownstreamFiniteIntervalSums.strictDownstreamRows✝ d, f j

theorem MetricCodes.Spherical.HigherYoungDownstreamFiniteIntervalSums.sum_ite_downstream_eq_sum_ite_between_add_add_downstream {m : ℕ} {A : Type u_1} [AddCommMonoid A] (i d : Fin m) (hid : i < d) (f : Fin m → A) : (∑ j : Fin m, if i < j then f j else 0) = (∑ j : Fin m, if i < j ∧ j < d then f j else 0) + f d + ∑ j : Fin m, if d < j then f j else 0

theorem MetricCodes.Spherical.HigherYoungDownstreamFiniteIntervalSums.sum_ite_between_eq_zero_of_succ {m : ℕ} {A : Type u_1} [AddCommMonoid A] (i d : Fin m) (hid : ↑d = ↑i + 1) (f : Fin m → A) : (∑ j : Fin m, if i < j ∧ j < d then f j else 0) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowDownstreamRecurrenceClosedForm.downstreamRows_castSucc_eq_insert_succ {r : ℕ} (i : Fin r) : MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankInternalRowLowerGram.downstreamRows✝ i.castSucc = insert i.succ (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankInternalRowLowerGram.downstreamRows✝ i.succ)

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowDownstreamRecurrenceClosedForm.downstreamDenominator_eq_downstreamShift {r : ℕ} (lam : Fin (r + 1) → ℕ) (a q : Fin (r + 1)) (haq : a < q) (hdom : Antitone lam) : MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankInternalRowLowerGram.downstreamDenominator✝ lam a q = MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamShift✝ lam a q

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowDownstreamRecurrenceClosedForm.downstreamNumerator_eq_downstreamShift_sub_one {r : ℕ} (lam : Fin (r + 1) → ℕ) (a q : Fin (r + 1)) (haq : a < q) (hdom : Antitone lam) : MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankInternalRowLowerGram.downstreamNumerator✝ lam a q = MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamShift✝ lam a q - 1

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowDownstreamRecurrenceClosedForm.downstreamRecurrence_eq_internalRowLowerGramScalar_mul {r : ℕ} (lam : Fin (r + 1) → ℕ) (a : Fin (r + 1)) (hdom : Antitone lam) (F : Fin (r + 1) → ℝ) (I : ℝ) (hrec : ∀ (i : Fin (r + 1)), F i = ↑(lam i) * I - ∑ j : Fin (r + 1), if i < j then (MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamShift✝ lam a j)⁻¹ * F j else 0) : F a = ArbitraryRankInternalRowLowerGram.internalRowLowerGramScalar lam a * I

theorem MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamGram.projectedCoordinateLower_basis_eq_downstreamCorrectedDerivative {r n : ℕ} (lam mu : Fin (r + 1) → ℕ) (a : Fin (r + 1)) (hdeg : ∑ i : Fin (r + 1), lam i = ∑ i : Fin (r + 1), mu i + 1) (p : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (k : Fin n) (hmem : MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamCorrectedDerivative✝ lam a p k a ∈ HigherHarmonicYoung.harmonicYoungSubmodule mu) : (HigherHarmonicYoung.projectedCoordinateLower mu lam hdeg a ((EuclideanSpace.basisFun (Fin n) ℝ) k)) p = ⟨MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamCorrectedDerivative✝ lam a p k a, hmem⟩

theorem MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamGram.youngClebschLower_downstream_inner_eq_cross_sum {r n : ℕ} (lam mu : Fin (r + 1) → ℕ) (a : Fin (r + 1)) (hdeg : ∑ i : Fin (r + 1), lam i = ∑ i : Fin (r + 1), mu i + 1) (hmem : ∀ (p : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (k : Fin n), MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamCorrectedDerivative✝ lam a p k a ∈ HigherHarmonicYoung.harmonicYoungSubmodule mu) (p q : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) : inner ℝ ((HigherHarmonicYoung.youngClebschLower mu lam hdeg a) p) ((HigherHarmonicYoung.youngClebschLower mu lam hdeg a) q) = ∑ k : Fin n, SpherePacking.Fischer.polynomialInner ((r + 1) * n) ((MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a k)) ↑p) (MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamCorrectedDerivative✝ lam a q k a)

theorem MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamGram.youngClebschLower_arbitrary_inner_eq_cross_sum_of_simpleRoots {r n : ℕ} (lam : Fin (r + 1) → ℕ) (a : Fin (r + 1)) (ha : 0 < lam a) (hsimple : ∀ (p : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (k : Fin n) (j : Fin r), (HigherHarmonicYoung.polarization r n j.castSucc j.succ) (MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamCorrectedDerivative✝ lam a p k a) = 0) (p q : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) : inner ℝ ((HigherHarmonicYoung.youngClebschLower (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight lam a) lam ⋯ a) p) ((HigherHarmonicYoung.youngClebschLower (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight lam a) lam ⋯ a) q) = ∑ k : Fin n, SpherePacking.Fischer.polynomialInner ((r + 1) * n) ((MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a k)) ↑p) (MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamCorrectedDerivative✝ lam a q k a)

theorem MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamGram.downstreamFischerCrossSum_eq_internalRowLowerGramScalar {r n : ℕ} (lam : Fin (r + 1) → ℕ) (a : Fin (r + 1)) (hdom : Antitone lam) (p q : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) : MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamGram.downstreamFischerCrossSum✝ lam a p q a = HigherHarmonicYoung.ArbitraryRankInternalRowLowerGram.internalRowLowerGramScalar lam a * inner ℝ p q

theorem MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamGram.youngClebschLower_arbitrary_inner_of_simpleRoots {r n : ℕ} (lam : Fin (r + 1) → ℕ) (a : Fin (r + 1)) (ha : 0 < lam a) (hdom : Antitone lam) (hsimple : ∀ (p : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (k : Fin n) (j : Fin r), (HigherHarmonicYoung.polarization r n j.castSucc j.succ) (MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamCorrectedDerivative✝ lam a p k a) = 0) (p q : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) : inner ℝ ((HigherHarmonicYoung.youngClebschLower (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight lam a) lam ⋯ a) p) ((HigherHarmonicYoung.youngClebschLower (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight lam a) lam ⋯ a) q) = HigherHarmonicYoung.ArbitraryRankInternalRowLowerGram.internalRowLowerGramScalar lam a * inner ℝ p q

theorem MetricCodes.Spherical.HigherYoungDownstreamSimpleRootInvariant.downstreamShift_succ_sub_castSucc {r : ℕ} (lam : Fin (r + 1) → ℕ) (a : Fin (r + 1)) (c : Fin r) : MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamShift✝ lam a c.succ - MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamShift✝ lam a c.castSucc = ↑(lam c.castSucc) - ↑(lam c.succ) + 1

theorem MetricCodes.Spherical.HigherYoungDownstreamSimpleRootInvariant.adjacentRowEuler_sub_on_downstream {r n : ℕ} (lam : Fin (r + 1) → ℕ) (a : Fin (r + 1)) (c : Fin r) (p : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (k : Fin n) : (HigherHarmonicYoung.rowEuler r n c.castSucc) (MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamCorrectedDerivative✝ lam a p k c.succ) - (HigherHarmonicYoung.rowEuler r n c.succ) (MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamCorrectedDerivative✝ lam a p k c.succ) = (↑(lam c.castSucc) - ↑(lam c.succ) + 1) • MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamCorrectedDerivative✝ lam a p k c.succ

theorem MetricCodes.Spherical.HigherYoungDownstreamSimpleRootInvariant.simpleRoot_internalDerivative {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (k : Fin n) (c : Fin r) (i : Fin (r + 1)) : (HigherHarmonicYoung.polarization r n c.castSucc c.succ) ((MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex i k)) ↑p) = if c.castSucc = i then -(MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex c.succ k)) ↑p else 0

theorem MetricCodes.Spherical.HigherYoungDownstreamSimpleRootInvariant.simpleRoot_downstreamPolarization_of_left {r n : ℕ} (lam : Fin (r + 1) → ℕ) (a i : Fin (r + 1)) (c : Fin r) (hic : i < c.castSucc) (p : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (k : Fin n) (j : Fin (r + 1)) (hjroot : (HigherHarmonicYoung.polarization r n c.castSucc c.succ) (MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamCorrectedDerivative✝ lam a p k j) = if c.castSucc = j then -(MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamShift✝ lam a j / MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamShift✝ lam a c.succ) • MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamCorrectedDerivative✝ lam a p k c.succ else 0) : (HigherHarmonicYoung.polarization r n c.castSucc c.succ) ((HigherHarmonicYoung.polarization r n j i) (MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamCorrectedDerivative✝ lam a p k j)) = if j = c.castSucc then -(MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamShift✝ lam a c.castSucc / MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamShift✝ lam a c.succ) • (HigherHarmonicYoung.polarization r n c.castSucc i) (MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamCorrectedDerivative✝ lam a p k c.succ) else if j = c.succ then (HigherHarmonicYoung.polarization r n c.castSucc i) (MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamCorrectedDerivative✝ lam a p k c.succ) else 0

theorem MetricCodes.Spherical.HigherYoungDownstreamSimpleRootInvariant.simpleRoot_downstreamPolarization_of_right {r n : ℕ} (lam : Fin (r + 1) → ℕ) (a i : Fin (r + 1)) (c : Fin r) (hci : c.castSucc < i) (p : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (k : Fin n) (j : Fin (r + 1)) (hij : i < j) (hjroot : (HigherHarmonicYoung.polarization r n c.castSucc c.succ) (MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamCorrectedDerivative✝ lam a p k j) = 0) : (HigherHarmonicYoung.polarization r n c.castSucc c.succ) ((HigherHarmonicYoung.polarization r n j i) (MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamCorrectedDerivative✝ lam a p k j)) = 0

theorem MetricCodes.Spherical.HigherYoungDownstreamAdjacentCancellationAlgebra.neg_add_inv_sub_smul_eq_neg_div_smul {V : Type u_1} [AddCommGroup V] [Module ℝ V] (x y : ℝ) (hy : y ≠ 0) (v : V) : -v + y⁻¹ • (y - x) • v = -(x / y) • v

theorem MetricCodes.Spherical.HigherYoungDownstreamAdjacentSumHelpers.sum_downstream_two_root_terms_eq_zero {m : ℕ} {V : Type u_1} [AddCommGroup V] [Module ℝ V] (δ : Fin m → ℝ) (i c d : Fin m) (hic : i < c) (hcd : c < d) (hc : δ c ≠ 0) (U : V) : (∑ j : Fin m, if i < j then (δ j)⁻¹ • if j = c then -(δ c / δ d) • U else if j = d then U else 0 else 0) = 0

theorem MetricCodes.Spherical.HigherYoungDownstreamAdjacentSumHelpers.sum_downstream_adjacent_root_eq_selected_sub_tail {m : ℕ} {V : Type u_1} [AddCommGroup V] [Module ℝ V] (δ : Fin m → ℝ) (c d : Fin m) (hcd : c < d) (hsucc : ↑d = ↑c + 1) (g : ℝ) (T : V) (P : Fin m → V) : (∑ j : Fin m, if c < j then (δ j)⁻¹ • if j = d then g • T else -P j else 0) = (δ d)⁻¹ • g • T - ∑ j : Fin m, if d < j then (δ j)⁻¹ • P j else 0

theorem MetricCodes.Spherical.HigherYoungDownstreamSimpleRootInvariant.simpleRoot_downstreamPolarization_of_self {r n : ℕ} (lam : Fin (r + 1) → ℕ) (a : Fin (r + 1)) (c : Fin r) (p : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (k : Fin n) (j : Fin (r + 1)) (hcj : c.castSucc < j) (hjroot : (HigherHarmonicYoung.polarization r n c.castSucc c.succ) (MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamCorrectedDerivative✝ lam a p k j) = 0) : (HigherHarmonicYoung.polarization r n c.castSucc c.succ) ((HigherHarmonicYoung.polarization r n j c.castSucc) (MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamCorrectedDerivative✝ lam a p k j)) = if j = c.succ then (↑(lam c.castSucc) - ↑(lam c.succ) + 1) • MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamCorrectedDerivative✝ lam a p k c.succ else -(HigherHarmonicYoung.polarization r n j c.succ) (MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamCorrectedDerivative✝ lam a p k j)

theorem MetricCodes.Spherical.HigherYoungDownstreamSimpleRootInvariant.downstreamCorrectedDerivative_simpleRoot {r n : ℕ} (lam : Fin (r + 1) → ℕ) (a : Fin (r + 1)) (hdom : Antitone lam) (p : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (k : Fin n) (i : Fin (r + 1)) (hai : a ≤ i) (c : Fin r) : (HigherHarmonicYoung.polarization r n c.castSucc c.succ) (MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamCorrectedDerivative✝ lam a p k i) = if c.castSucc = i then -(MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamShift✝ lam a i / MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamShift✝ lam a c.succ) • MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamCorrectedDerivative✝ lam a p k c.succ else 0

theorem MetricCodes.Spherical.HigherYoungDownstreamSimpleRootInvariant.downstreamCorrectedDerivative_source_simpleRoot_eq_zero {r n : ℕ} (lam : Fin (r + 1) → ℕ) (a : Fin (r + 1)) (hdom : Antitone lam) (p : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (k : Fin n) (c : Fin r) : (HigherHarmonicYoung.polarization r n c.castSucc c.succ) (MetricCodes.Spherical.HigherYoungArbitraryRowDownstreamCorrection.downstreamCorrectedDerivative✝ lam a p k a) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowDownstreamActualChannels.youngClebschLower_arbitrary_inner {r n : ℕ} (lam : Fin (r + 1) → ℕ) (a : Fin (r + 1)) (ha : 0 < lam a) (hdom : Antitone lam) (p q : ↥(HarmonicYoungSpace lam)) : inner ℝ ((youngClebschLower (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight lam a) lam ⋯ a) p) ((youngClebschLower (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight lam a) lam ⋯ a) q) = ArbitraryRankInternalRowLowerGram.internalRowLowerGramScalar lam a * inner ℝ p q

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowDownstreamActualChannels.youngClebschLower_arbitrary_adjoint_comp_self {r n : ℕ} (lam : Fin (r + 1) → ℕ) (a : Fin (r + 1)) (ha : 0 < lam a) (hdom : Antitone lam) : LinearMap.adjoint (youngClebschLower (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight lam a) lam ⋯ a) ∘ₗ youngClebschLower (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight lam a) lam ⋯ a = ArbitraryRankInternalRowLowerGram.internalRowLowerGramScalar lam a • LinearMap.id

@[simp]

theorem MetricCodes.Spherical.HigherYoungArbitraryRowLoweringProjectedAxisWitness.loweredInternalYoungWeight_raiseWeight {r : ℕ} (lam : Fin (r + 1) → ℕ) (row : Fin (r + 1)) : HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight (HigherChannel.raiseWeight lam row) row = lam

theorem MetricCodes.Spherical.HigherYoungArbitraryRowLoweringProjectedAxisWitness.youngClebschLower_inner_of_raisedSignature {r n : ℕ} (source target : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hrow : target = HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight source row) (hpositive : 0 < source row) (hdom : Antitone source) (hdeg : ∑ i : Fin (r + 1), source i = ∑ i : Fin (r + 1), target i + 1) (p q : ↥(HigherHarmonicYoung.HarmonicYoungSpace source)) : inner ℝ ((HigherHarmonicYoung.youngClebschLower target source hdeg row) p) ((HigherHarmonicYoung.youngClebschLower target source hdeg row) q) = HigherHarmonicYoung.ArbitraryRankInternalRowLowerGram.internalRowLowerGramScalar source row * inner ℝ p q

theorem MetricCodes.Spherical.HigherYoungArbitraryRowLoweringProjectedAxisWitness.raiseWeight_strictly_removable {r : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (row j : Fin (r + 1)) (hj : ↑j = ↑row + 1) : HigherChannel.raiseWeight lam row j < HigherChannel.raiseWeight lam row row

structure MetricCodes.Spherical.HigherYoungArbitraryRowLoweringProjectedAxisWitness.GenuineLoweringFibreAxisData {r m n : ℕ} (a : Fin (r + 2) → ℝ) (b : Fin (r + 1) → ℝ) (o : HigherProjectionInstantiation.SpherePoint n) (fibre : (i : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) → ↥(HigherHierarchyActualBoxSufficiency.BoxStabilizer n b) →ₗᵢ[ℝ] HigherYoungMovingFibres.YoungVertex (HigherYoungActualGraphAssembly.boxSignature a n) i) (target source : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) (row : Fin (r + 2)) (hdeg : ∑ i : Fin (r + 1 + 1), HigherYoungActualGraphAssembly.boxSignature a n source i = ∑ i : Fin (r + 1 + 1), HigherYoungActualGraphAssembly.boxSignature a n target i + 1) : Type

Data encoding the genuine lowering fibre axis construction.

• coefficient : ℝ

  The coefficient component.

• coefficient_sq : self.coefficient ^ 2 = HigherHarmonicYoung.ArbitraryRankInternalRowLowerGram.internalRowLowerGramScalar (HigherYoungActualGraphAssembly.boxSignature a n source) row * HigherChannel.plusProbability n (HigherYoungActualGraphAssembly.boxSignature a n target) (HigherHierarchy.Weyl.flooredWeight b n) row
• projected_axis (v : ↥(HigherHierarchyActualBoxSufficiency.BoxStabilizer n b)) : (HigherHarmonicYoung.projectedCoordinateRaise (HigherYoungActualGraphAssembly.boxSignature a n source) (HigherYoungActualGraphAssembly.boxSignature a n target) hdeg row ↑o) ((fibre target) v) = self.coefficient • (fibre source) v

theorem MetricCodes.Spherical.HigherYoungAllRankGTFibreReverseProbability.reverseCoefficient_sq_of_forward_sq_and_weylRatio {r n : ℕ} (low : Fin (r + 1) → ℕ) (mu : Fin r → ℕ) (row : Fin (r + 1)) (h : HigherChannel.FiniteInterlacing n low mu) (hraise : HigherChannel.FiniteInterlacing n (HigherChannel.raiseWeight low row) mu) (lowerGram raisingGram coefficient : ℝ) (hforward : coefficient ^ 2 = lowerGram * HigherChannel.plusProbability n low mu row) (hgramRatio : raisingGram = lowerGram * HigherChannel.weylEdgeRatio n low row) : coefficient ^ 2 = raisingGram * HigherChannel.minusProbability n (HigherChannel.raiseWeight low row) mu row

structure MetricCodes.Spherical.HigherHarmonicYoung.AllRankCanonicalBoxProjectedAxisWitness.CanonicalBoxEdgeAxisData {r m n : ℕ} (a : Fin (r + 2) → ℝ) (b : Fin (r + 1) → ℝ) (o : HigherProjectionInstantiation.SpherePoint n) (fibre : (i : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) → ↥(HigherHierarchyActualBoxSufficiency.BoxStabilizer n b) →ₗᵢ[ℝ] HigherYoungMovingFibres.YoungVertex (HigherYoungActualGraphAssembly.boxSignature a n) i) (low high : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) (row : Fin (r + 2)) (hrow : HigherYoungActualGraphAssembly.boxSignature a n high = HigherChannel.raiseWeight (HigherYoungActualGraphAssembly.boxSignature a n low) row) : Type

Data encoding the canonical box edge axis construction.

• forward : HigherYoungArbitraryRowLoweringProjectedAxisWitness.GenuineLoweringFibreAxisData a b o fibre low high row ⋯

  The forward component.

• raisingGram : ℝ

  The raising gram component.

• raisingGram_pos : 0 < self.raisingGram
• raisingGram_inner (p q : HigherYoungMovingFibres.YoungVertex (HigherYoungActualGraphAssembly.boxSignature a n) low) : inner ℝ ((youngClebschRaise (HigherYoungActualGraphAssembly.boxSignature a n high) (HigherYoungActualGraphAssembly.boxSignature a n low) ⋯ row) p) ((youngClebschRaise (HigherYoungActualGraphAssembly.boxSignature a n high) (HigherYoungActualGraphAssembly.boxSignature a n low) ⋯ row) q) = self.raisingGram * inner ℝ p q
• raisingGram_ratio : self.raisingGram = ArbitraryRankInternalRowLowerGram.internalRowLowerGramScalar (HigherYoungActualGraphAssembly.boxSignature a n high) row * HigherChannel.weylEdgeRatio n (HigherYoungActualGraphAssembly.boxSignature a n low) row
• reverse_range (v : ↥(HigherHierarchyActualBoxSufficiency.BoxStabilizer n b)) : (projectedCoordinateLower (HigherYoungActualGraphAssembly.boxSignature a n low) (HigherYoungActualGraphAssembly.boxSignature a n high) ⋯ row ↑o) ((fibre high) v) ∈ (fibre low).range

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankCanonicalBoxProjectedAxisWitness.canonicalBoxReverseProjectedAxis_of_edgeData {r m n : ℕ} (a : Fin (r + 2) → ℝ) (b : Fin (r + 1) → ℝ) (o : HigherProjectionInstantiation.SpherePoint n) (fibre : (i : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) → ↥(HigherHierarchyActualBoxSufficiency.BoxStabilizer n b) →ₗᵢ[ℝ] HigherYoungMovingFibres.YoungVertex (HigherYoungActualGraphAssembly.boxSignature a n) i) (low high : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) (row : Fin (r + 2)) (hrow : HigherYoungActualGraphAssembly.boxSignature a n high = HigherChannel.raiseWeight (HigherYoungActualGraphAssembly.boxSignature a n low) row) (D : CanonicalBoxEdgeAxisData a b o fibre low high row hrow) (v : ↥(HigherHierarchyActualBoxSufficiency.BoxStabilizer n b)) : (projectedCoordinateLower (HigherYoungActualGraphAssembly.boxSignature a n low) (HigherYoungActualGraphAssembly.boxSignature a n high) ⋯ row ↑o) ((fibre high) v) = D.forward.coefficient • (fibre low) v

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.AllRankCanonicalBoxProjectedAxisWitness.canonicalBoxProjectedAxisWitness {r m n : ℕ} (a : Fin (r + 2) → ℝ) (b : Fin (r + 1) → ℝ) (hstable : ∀ (v : HigherHierarchy.RectangularVertices.Vertex (r + 1) m), HigherChannel.FiniteInterlacing n (HigherHierarchy.RectangularVertices.signature a n v) (HigherChannel.flooredCoordinates b n)) (hgram : ∀ (i : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m), AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram (HigherYoungActualGraphAssembly.boxSignature a n i) (HigherHierarchy.Weyl.flooredWeight b n) ⋯) (o : HigherProjectionInstantiation.SpherePoint n) (haxis : (low high : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) → (row : Fin (r + 2)) → (hrow : HigherYoungActualGraphAssembly.boxSignature a n high = HigherChannel.raiseWeight (HigherYoungActualGraphAssembly.boxSignature a n low) row) → CanonicalBoxEdgeAxisData a b o (AllRankGelfandTsetlinCanonicalFibre.canonicalBoxGelfandTsetlinFibre a b hstable hgram) low high row hrow) (target source : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) (h : 0 < HigherHierarchyActualBoxSufficiency.boxProbability a b n target source) : HigherYoungAllRankActualBoxInstantiation.BoxProjectedAxisWitness a b o (AllRankGelfandTsetlinCanonicalFibre.canonicalBoxGelfandTsetlinFibre a b hstable hgram) target source h

The canonical box projected axis witness used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowUnconditionalBranch.fixedAxisInitialSimpleRootCancellation_of_antitone {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (row : Fin (r + 1)) (k : Fin n) : MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowTransverseYoungBranch.FixedAxisInitialSimpleRootCancellation✝ lam row k

def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowAxialAdjointGram.arbitraryRowAxialLowerScalar {r : ℕ} (lam : Fin (r + 1) → ℕ) (row : Fin (r + 1)) : ℝ

The arbitrary row axial lower scalar used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowAxialAdjointGram.sortedPrecedingPath_pairwise {r : ℕ} (row : Fin (r + 1)) (S : Finset (Fin (r + 1))) (hsub : S ⊆ AllRankArbitraryRowBranchingOperator.precedingRows row) : List.Pairwise (fun (x1 x2 : Fin (r + 1)) => x1 < x2) ((S.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ [row])

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowAxialAdjointGram.arbitraryRowAxialLower_summand_of_highest {r n : ℕ} (lam : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (k : Fin n) (S : Finset (Fin (r + 1))) (hS : S ⊆ AllRankArbitraryRowBranchingOperator.precedingRows row) (q : PolynomialSpace r n) (hhighest : ∀ (a b : Fin (r + 1)), a < b → (polarization r n a b) q = 0) : AllRankArbitraryRowBranchingOperator.polarizationPathCoefficient lam row S • (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowProjectedLowerOperator.upperPolarizationPath✝ ((S.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ [row])) ((MvPolynomial.pderiv (variableIndex (AllRankArbitraryRowBranchingOperator.polarizationPathStart row S) k)) q) = (∏ i ∈ AllRankArbitraryRowBranchingOperator.precedingRows row \ S, AllRankArbitraryRowBranchingOperator.shiftedRowGap lam row i) • (MvPolynomial.pderiv (variableIndex row k)) q

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowAxialAdjointGram.arbitraryRowAxialLower_of_highest {r n : ℕ} (lam : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (k : Fin n) (q : PolynomialSpace r n) (hhighest : ∀ (a b : Fin (r + 1)), a < b → (polarization r n a b) q = 0) : (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowProjectedLowerOperator.arbitraryRowAxialLower✝ lam row k) q = arbitraryRowAxialLowerScalar lam row • (MvPolynomial.pderiv (variableIndex row k)) q

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankRawForwardAxisRange.simultaneousHarmonicProjection_residual_mem_gram_all_degree {r n d : ℕ} (p : ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) d)) : ↑p - ↑↑((simultaneousHarmonicProjection r n d) p) ∈ youngGramRadialIdeal r n

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankRawForwardAxisRange.youngHarmonicLift_residual_mem_gram_all_degree {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p : ↥(homogeneousYoungHighestWeightSubmodule lam)) : ↑↑p - ↑((youngHarmonicLift lam) p) ∈ youngGramRadialIdeal r n

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankRawForwardAxisRange.reverseInterlacingPolynomialSeed_sub_harmonicBranch_mem_gram {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (p : ↥(HarmonicYoungSpace mu)) : (ArbitraryRankReverseInterlacingPolynomialSeed.reverseInterlacingPolynomialSeed lam mu) p - ↑((ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch lam mu h) p) ∈ youngGramRadialIdeal (r + 1) (n + 1)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankRawForwardAxisRange.arbitraryRowAxialRaise_harmonicBranch_sub_rawSeed_mem_gram {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (row : Fin (r + 2)) (p : ↥(HarmonicYoungSpace mu)) : (AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam row (Fin.last n)) ↑((ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch lam mu h) p) - (AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam row (Fin.last n)) ((ArbitraryRankReverseInterlacingPolynomialSeed.reverseInterlacingPolynomialSeed lam mu) p) ∈ youngGramRadialIdeal (r + 1) (n + 1)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankRawForwardAxisRange.arbitraryRowAxialRaise_harmonicBranch_sub_adjacent_mem_gram_of_pathExchange {r n : ℕ} (low high : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (hlow : HigherRepresentationGraph.Interlaces low mu) (hhigh : HigherRepresentationGraph.Interlaces high mu) (row : Fin (r + 2)) (coefficient : ℝ) (hexchange : ∀ (p : ↥(HarmonicYoungSpace mu)), (AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise low row (Fin.last n)) ((ArbitraryRankReverseInterlacingPolynomialSeed.reverseInterlacingPolynomialSeed low mu) p) - coefficient • (ArbitraryRankReverseInterlacingPolynomialSeed.reverseInterlacingPolynomialSeed high mu) p ∈ youngGramRadialIdeal (r + 1) (n + 1)) (p : ↥(HarmonicYoungSpace mu)) : (AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise low row (Fin.last n)) ↑((ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch low mu hlow) p) - coefficient • ↑((ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch high mu hhigh) p) ∈ youngGramRadialIdeal (r + 1) (n + 1)

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowBaseAxisChannel.arbitraryRowAxialLowerScalar_pos {r : ℕ} (lam : Fin (r + 1) → ℕ) (row : Fin (r + 1)) : 0 < ArbitraryRowAxialAdjointGram.arbitraryRowAxialLowerScalar lam row

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowBaseAxisChannel.arbitraryRowAxialRaise_fischer_inner_eq_lowerScalar_mul_coordinate {r n : ℕ} (lam : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (k : Fin n) (p q : PolynomialSpace r n) (hhighest : ∀ (a b : Fin (r + 1)), a < b → (polarization r n a b) q = 0) : SpherePacking.Fischer.polynomialInner ((r + 1) * n) ((AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam row k) p) q = ArbitraryRowAxialAdjointGram.arbitraryRowAxialLowerScalar lam row * SpherePacking.Fischer.polynomialInner ((r + 1) * n) (MvPolynomial.X (variableIndex row k) * p) q

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.AllRankRawProjectedRaiseMickelsson.arbitraryRowSameAxisHarmonicRaise {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (row : Fin (r + 1)) (k : Fin n) : ↥(HarmonicYoungSpace lam) →ₗ[ℝ] ↥(HarmonicYoungSpace (HigherChannel.raiseWeight lam row))

The arbitrary row same axis harmonic raise used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankRawProjectedRaiseMickelsson.arbitraryRowSameAxisHarmonicRaise_inner {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (row : Fin (r + 1)) (k : Fin n) (p : ↥(HarmonicYoungSpace lam)) (q : ↥(HarmonicYoungSpace (HigherChannel.raiseWeight lam row))) : inner ℝ ((arbitraryRowSameAxisHarmonicRaise lam hdom row k) p) q = SpherePacking.Fischer.polynomialInner ((r + 1) * n) ((AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam row k) ↑p) ↑q

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankRawProjectedRaiseMickelsson.projectedCoordinateRaise_eq_arbitraryRowSameAxisHarmonicRaise {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (row : Fin (r + 1)) (k : Fin n) (p : ↥(HarmonicYoungSpace lam)) : (projectedCoordinateRaise (HigherChannel.raiseWeight lam row) lam ⋯ row ((EuclideanSpace.basisFun (Fin n) ℝ) k)) p = (ArbitraryRowAxialAdjointGram.arbitraryRowAxialLowerScalar lam row)⁻¹ • (arbitraryRowSameAxisHarmonicRaise lam hdom row k) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankCanonicalForwardAxisRange.arbitraryRowSameAxisHarmonicRaise_sub_raw_mem_gram {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (row : Fin (r + 1)) (k : Fin n) (p : ↥(HarmonicYoungSpace lam)) : ↑((AllRankRawProjectedRaiseMickelsson.arbitraryRowSameAxisHarmonicRaise lam hdom row k) p) - (AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam row k) ↑p ∈ youngGramRadialIdeal r n

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankCanonicalForwardAxisRange.arbitraryRowSameAxisHarmonicRaise_reverseBranch_eq_of_pathExchange {r n : ℕ} (low : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (row : Fin (r + 2)) (hlow : HigherRepresentationGraph.Interlaces low mu) (hhigh : HigherRepresentationGraph.Interlaces (HigherChannel.raiseWeight low row) mu) (hdom : Antitone low) (coefficient : ℝ) (hexchange : ∀ (p : ↥(HarmonicYoungSpace mu)), (AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise low row (Fin.last n)) ((ArbitraryRankReverseInterlacingPolynomialSeed.reverseInterlacingPolynomialSeed low mu) p) - coefficient • (ArbitraryRankReverseInterlacingPolynomialSeed.reverseInterlacingPolynomialSeed (HigherChannel.raiseWeight low row) mu) p ∈ youngGramRadialIdeal (r + 1) (n + 1)) (p : ↥(HarmonicYoungSpace mu)) : (AllRankRawProjectedRaiseMickelsson.arbitraryRowSameAxisHarmonicRaise low hdom row (Fin.last n)) ((ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch low mu hlow) p) = coefficient • (ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch (HigherChannel.raiseWeight low row) mu hhigh) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankCanonicalForwardAxisRange.projectedCoordinateRaise_reverseInterlacingHarmonicBranch_eq_of_pathExchange {r n : ℕ} (low : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (row : Fin (r + 2)) (hlow : HigherRepresentationGraph.Interlaces low mu) (hhigh : HigherRepresentationGraph.Interlaces (HigherChannel.raiseWeight low row) mu) (hdom : Antitone low) (coefficient : ℝ) (hexchange : ∀ (p : ↥(HarmonicYoungSpace mu)), (AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise low row (Fin.last n)) ((ArbitraryRankReverseInterlacingPolynomialSeed.reverseInterlacingPolynomialSeed low mu) p) - coefficient • (ArbitraryRankReverseInterlacingPolynomialSeed.reverseInterlacingPolynomialSeed (HigherChannel.raiseWeight low row) mu) p ∈ youngGramRadialIdeal (r + 1) (n + 1)) (p : ↥(HarmonicYoungSpace mu)) : (projectedCoordinateRaise (HigherChannel.raiseWeight low row) low ⋯ row ((EuclideanSpace.basisFun (Fin (n + 1)) ℝ) (Fin.last n))) ((ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch low mu hlow) p) = ((ArbitraryRowAxialAdjointGram.arbitraryRowAxialLowerScalar low row)⁻¹ * coefficient) • (ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch (HigherChannel.raiseWeight low row) mu hhigh) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankCanonicalForwardAxisRange.projectedCoordinateRaise_reverseInterlacingHarmonicBranch_mem_range_of_pathExchange {r n : ℕ} (low : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (row : Fin (r + 2)) (hlow : HigherRepresentationGraph.Interlaces low mu) (hhigh : HigherRepresentationGraph.Interlaces (HigherChannel.raiseWeight low row) mu) (hdom : Antitone low) (coefficient : ℝ) (hexchange : ∀ (p : ↥(HarmonicYoungSpace mu)), (AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise low row (Fin.last n)) ((ArbitraryRankReverseInterlacingPolynomialSeed.reverseInterlacingPolynomialSeed low mu) p) - coefficient • (ArbitraryRankReverseInterlacingPolynomialSeed.reverseInterlacingPolynomialSeed (HigherChannel.raiseWeight low row) mu) p ∈ youngGramRadialIdeal (r + 1) (n + 1)) (p : ↥(HarmonicYoungSpace mu)) : (projectedCoordinateRaise (HigherChannel.raiseWeight low row) low ⋯ row ((EuclideanSpace.basisFun (Fin (n + 1)) ℝ) (Fin.last n))) ((ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch low mu hlow) p) ∈ (ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch (HigherChannel.raiseWeight low row) mu hhigh).range

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankCanonicalFibreAxisTransfer.canonicalFibreAxisCoefficient_sq (raw sourceGram targetGram : ℝ) (hsource : 0 < sourceGram) (htarget : 0 < targetGram) : (raw * √targetGram / √sourceGram) ^ 2 = raw ^ 2 * targetGram / sourceGram

theorem MetricCodes.Spherical.HigherYoungArbitraryRankAdjacentInterlacingSchedule.interlacingGap_raiseWeight {r : ℕ} {low : Fin (r + 2) → ℕ} {mu : Fin (r + 1) → ℕ} (hlow : HigherRepresentationGraph.Interlaces low mu) (row i : Fin (r + 2)) : HigherYoungArbitraryRankInterlacingGapSchedule.interlacingGap (HigherChannel.raiseWeight low row) mu i = HigherYoungArbitraryRankInterlacingGapSchedule.interlacingGap low mu i + if i = row then 1 else 0

theorem MetricCodes.Spherical.HigherYoungArbitraryRankAdjacentInterlacingSchedule.reverseInterlacingRowSchedule_raiseWeight_count {r : ℕ} {low : Fin (r + 2) → ℕ} {mu : Fin (r + 1) → ℕ} (hlow : HigherRepresentationGraph.Interlaces low mu) (row i : Fin (r + 2)) : List.count i (HigherYoungArbitraryRankInterlacingLegalSchedule.reverseInterlacingRowSchedule (HigherChannel.raiseWeight low row) mu) = List.count i (HigherYoungArbitraryRankInterlacingLegalSchedule.reverseInterlacingRowSchedule low mu) + if i = row then 1 else 0

theorem MetricCodes.Spherical.HigherYoungArbitraryRankAdjacentInterlacingSchedule.reverseInterlacingRowSchedule_raiseWeight_perm {r : ℕ} {low : Fin (r + 2) → ℕ} {mu : Fin (r + 1) → ℕ} (hlow : HigherRepresentationGraph.Interlaces low mu) (row : Fin (r + 2)) : (HigherYoungArbitraryRankInterlacingLegalSchedule.reverseInterlacingRowSchedule (HigherChannel.raiseWeight low row) mu).Perm (HigherYoungArbitraryRankInterlacingLegalSchedule.reverseInterlacingRowSchedule low mu ++ [row])

def MetricCodes.Spherical.HigherYoungArbitraryRankAdjacentInterlacingSchedule.adjacentReversePrefix {r : ℕ} (low : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (row : Fin (r + 2)) : List (Fin (r + 2))

The adjacent reverse prefix used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

def MetricCodes.Spherical.HigherYoungArbitraryRankAdjacentInterlacingSchedule.adjacentReverseSuffix {r : ℕ} (low : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (row : Fin (r + 2)) : List (Fin (r + 2))

The adjacent reverse suffix used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.

theorem MetricCodes.Spherical.HigherYoungArbitraryRankAdjacentInterlacingSchedule.le_of_mem_adjacentReversePrefix {r : ℕ} (low : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (row i : Fin (r + 2)) (hi : i ∈ adjacentReversePrefix low mu row) : row ≤ i

theorem MetricCodes.Spherical.HigherYoungArbitraryRankAdjacentInterlacingSchedule.lt_of_mem_adjacentReverseSuffix {r : ℕ} (low : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (row i : Fin (r + 2)) (hi : i ∈ adjacentReverseSuffix low mu row) : i < row

theorem MetricCodes.Spherical.HigherYoungArbitraryRankAdjacentInterlacingSchedule.reverseInterlacingRowSchedule_eq_adjacentReversePrefix_append_suffix {r : ℕ} (low : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (row : Fin (r + 2)) : HigherYoungArbitraryRankInterlacingLegalSchedule.reverseInterlacingRowSchedule low mu = adjacentReversePrefix low mu row ++ adjacentReverseSuffix low mu row

theorem MetricCodes.Spherical.HigherYoungArbitraryRankAdjacentInterlacingSchedule.reverseInterlacingRowSchedule_raiseWeight_eq_prefix_cons_suffix {r : ℕ} {low : Fin (r + 2) → ℕ} {mu : Fin (r + 1) → ℕ} (hlow : HigherRepresentationGraph.Interlaces low mu) (row : Fin (r + 2)) : HigherYoungArbitraryRankInterlacingLegalSchedule.reverseInterlacingRowSchedule (HigherChannel.raiseWeight low row) mu = adjacentReversePrefix low mu row ++ row :: adjacentReverseSuffix low mu row

theorem MetricCodes.Spherical.HigherYoungArbitraryRankAdjacentInterlacingSchedule.arbitraryRowPathWeight_append {r : ℕ} (lam : Fin (r + 2) → ℕ) (pref suff : List (Fin (r + 2))) : HigherHarmonicYoung.ArbitraryRowMickelssonGramIdeal.arbitraryRowPathWeight lam (pref ++ suff) = HigherHarmonicYoung.ArbitraryRowMickelssonGramIdeal.arbitraryRowPathWeight (HigherHarmonicYoung.ArbitraryRowMickelssonGramIdeal.arbitraryRowPathWeight lam pref) suff

theorem MetricCodes.Spherical.HigherYoungArbitraryRankAdjacentInterlacingSchedule.arbitraryRowPathWeight_adjacentReversePrefix_append_suffix {r : ℕ} {low : Fin (r + 2) → ℕ} {mu : Fin (r + 1) → ℕ} (hlow : HigherRepresentationGraph.Interlaces low mu) (row : Fin (r + 2)) : HigherHarmonicYoung.ArbitraryRowMickelssonGramIdeal.arbitraryRowPathWeight (ThreeRowYoungBranching.appendZeroWeight mu) (adjacentReversePrefix low mu row ++ adjacentReverseSuffix low mu row) = low