All-rank harmonic rigidity

Completion of the root complex and rigidity of harmonic highest-weight vectors.

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootVectorBracket_single_rootBracket {r : ℕ} (α β γ : PositiveRoot r) : rootVectorBracket (fun₀ | α => 1) (rootBracket β γ) = ∑ δ : PositiveRoot r, rootStructureConstant β γ δ • rootBracket α δ

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootStructureConstant_jacobi {r : ℕ} (α β γ ε : PositiveRoot r) : ∑ δ : PositiveRoot r, rootStructureConstant β γ δ * rootStructureConstant α δ ε + ∑ δ : PositiveRoot r, rootStructureConstant γ α δ * rootStructureConstant β δ ε + ∑ δ : PositiveRoot r, rootStructureConstant α β δ * rootStructureConstant γ δ ε = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.actualExteriorRootCreation_anticommute {ι : Type u_1} {M : Type u_2} [LinearOrder ι] [AddCommGroup M] [Module ℝ M] (a b : ι) : actualExteriorRootCreation M a * actualExteriorRootCreation M b + actualExteriorRootCreation M b * actualExteriorRootCreation M a = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.actualExteriorRootCreation_contraction_contraction_cubic_anticommute {ι : Type u_1} {M : Type u_2} [LinearOrder ι] [AddCommGroup M] [Module ℝ M] (α β γ δ ε ζ : ι) : actualExteriorRootCreation M γ * (actualExteriorRootContraction M β * actualExteriorRootContraction M α) * (actualExteriorRootCreation M ζ * (actualExteriorRootContraction M ε * actualExteriorRootContraction M δ)) + actualExteriorRootCreation M ζ * (actualExteriorRootContraction M ε * actualExteriorRootContraction M δ) * (actualExteriorRootCreation M γ * (actualExteriorRootContraction M β * actualExteriorRootContraction M α)) = (((if α = ζ then actualExteriorRootCreation M γ * (actualExteriorRootContraction M β * (actualExteriorRootContraction M ε * actualExteriorRootContraction M δ)) else 0) - if β = ζ then actualExteriorRootCreation M γ * (actualExteriorRootContraction M α * (actualExteriorRootContraction M ε * actualExteriorRootContraction M δ)) else 0) + if δ = γ then actualExteriorRootCreation M ζ * (actualExteriorRootContraction M ε * (actualExteriorRootContraction M β * actualExteriorRootContraction M α)) else 0) - if ε = γ then actualExteriorRootCreation M ζ * (actualExteriorRootContraction M δ * (actualExteriorRootContraction M β * actualExteriorRootContraction M α)) else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorBracketAtom_swap {r n : ℕ} (α β γ : PositiveRoot r) : fullRootExteriorBracketAtom r n β α γ = -fullRootExteriorBracketAtom r n α β γ

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorBracket_weightedAtom_swap {r n : ℕ} (α β γ : PositiveRoot r) : rootStructureConstant β α γ • fullRootExteriorBracketAtom r n β α γ = rootStructureConstant α β γ • fullRootExteriorBracketAtom r n α β γ

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorBracketUnordered (r n : ℕ) : Module.End ℝ (FullRootExteriorPolynomialChain r n)

Sum the exterior bracket atoms over all ordered root triples with their structure constants.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootStructureConstant_eq_zero_of_incomparable {r : ℕ} (α β γ : PositiveRoot r) (hαβ : ¬α < β) (hβα : ¬β < α) : rootStructureConstant α β γ = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorBracketUnordered_eq_two_smul (r n : ℕ) : fullRootExteriorBracketUnordered r n = 2 • fullRootExteriorBracket r n

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootExteriorCoboundaryAtom_swap {M : Type u_1} [AddCommGroup M] [Module ℝ M] {r : ℕ} (α β γ : PositiveRoot r) : actualExteriorRootCreation M β * (actualExteriorRootCreation M α * actualExteriorRootContraction M γ) = -(actualExteriorRootCreation M α * (actualExteriorRootCreation M β * actualExteriorRootContraction M γ))

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootExteriorCoboundary_weightedAtom_swap {M : Type u_1} [AddCommGroup M] [Module ℝ M] {r : ℕ} (α β γ : PositiveRoot r) : rootStructureConstant β α γ • (actualExteriorRootCreation M β * (actualExteriorRootCreation M α * actualExteriorRootContraction M γ)) = rootStructureConstant α β γ • (actualExteriorRootCreation M α * (actualExteriorRootCreation M β * actualExteriorRootContraction M γ))

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.actualExteriorRootBracketCoboundary_eq_two_ordered_sum {M : Type u_1} [AddCommGroup M] [Module ℝ M] {r : ℕ} : actualExteriorRootBracketCoboundary rootStructureConstant = 2 • ∑ α : PositiveRoot r, ∑ β : PositiveRoot r, if α < β then ∑ γ : PositiveRoot r, rootStructureConstant α β γ • (actualExteriorRootCreation M α * (actualExteriorRootCreation M β * actualExteriorRootContraction M γ)) else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.actualOrderedRootBracketCoboundary_eq_ordered_sum {M : Type u_1} [AddCommGroup M] [Module ℝ M] {r : ℕ} : actualOrderedRootBracketCoboundary = ∑ α : PositiveRoot r, ∑ β : PositiveRoot r, if α < β then ∑ γ : PositiveRoot r, rootStructureConstant α β γ • (actualExteriorRootCreation M α * (actualExteriorRootCreation M β * actualExteriorRootContraction M γ)) else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.actualExteriorRootBracketCoboundary_zeroExtension_of_card_ne {r n k : ℕ} (f : RootPolynomialChain r n k) (S : Finset (PositiveRoot r)) (hS : S.card ≠ k + 1) : (actualExteriorRootBracketCoboundary rootStructureConstant) ((rootPolynomialChainZeroExtension r n k) f) S = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.actualOrderedRootBracketCoboundary_zeroExtension_of_card_ne {r n k : ℕ} (f : RootPolynomialChain r n k) (S : Finset (PositiveRoot r)) (hS : S.card ≠ k + 1) : actualOrderedRootBracketCoboundary ((rootPolynomialChainZeroExtension r n k) f) S = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.actualOrderedRootBracketCoboundary_zeroExtension_apply_of_single {r n k : ℕ} (f : RootPolynomialChain r n k) (S : RootWedge r (k + 1)) (hsingle : ∀ (T : RootWedge r k) (p : PolynomialSpace r n), actualOrderedRootBracketCoboundary (Pi.single (↑T) p) ↑S = rootBracketBoundaryCoefficient S T • p) : actualOrderedRootBracketCoboundary ((rootPolynomialChainZeroExtension r n k) f) ↑S = (rootBracketCoboundary r n k) f S

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootOrderCode_lt_iff_of_structureConstant_ne_zero {r : ℕ} (α β γ : PositiveRoot r) (h : rootStructureConstant α β γ ≠ 0) : positiveRootOrderCode α < positiveRootOrderCode β ↔ α < β

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorActionAtom_mul_self_zero {r n : ℕ} (α : PositiveRoot r) : fullRootExteriorActionAtom r n α * fullRootExteriorActionAtom r n α = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorActionAtom_pair {r n : ℕ} (α β : PositiveRoot r) : fullRootExteriorActionAtom r n α * fullRootExteriorActionAtom r n β + fullRootExteriorActionAtom r n β * fullRootExteriorActionAtom r n α = (fullRootExteriorPolynomialAction r n α * fullRootExteriorPolynomialAction r n β - fullRootExteriorPolynomialAction r n β * fullRootExteriorPolynomialAction r n α) * (actualExteriorRootContraction (PolynomialSpace r n) α * actualExteriorRootContraction (PolynomialSpace r n) β)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorAction_square_eq_unordered_structureConstants (r n : ℕ) : fullRootExteriorAction r n * fullRootExteriorAction r n = ∑ α : PositiveRoot r, ∑ β : PositiveRoot r, if positiveRootOrderCode α < positiveRootOrderCode β then ∑ γ : PositiveRoot r, rootStructureConstant α β γ • (fullRootExteriorPolynomialAction r n γ * (actualExteriorRootContraction (PolynomialSpace r n) α * actualExteriorRootContraction (PolynomialSpace r n) β)) else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorPolynomialAction_bracketAtom_commute {r n : ℕ} (δ α β γ : PositiveRoot r) : fullRootExteriorPolynomialAction r n δ * fullRootExteriorBracketAtom r n α β γ = fullRootExteriorBracketAtom r n α β γ * fullRootExteriorPolynomialAction r n δ

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorActionAtom_bracketAtom_anticommute {r n : ℕ} (δ α β γ : PositiveRoot r) : fullRootExteriorActionAtom r n δ * fullRootExteriorBracketAtom r n α β γ + fullRootExteriorBracketAtom r n α β γ * fullRootExteriorActionAtom r n δ = if δ = γ then fullRootExteriorPolynomialAction r n γ * (actualExteriorRootContraction (PolynomialSpace r n) β * actualExteriorRootContraction (PolynomialSpace r n) α) else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorAction_bracketAtom_anticommute {r n : ℕ} (α β γ : PositiveRoot r) : fullRootExteriorAction r n * fullRootExteriorBracketAtom r n α β γ + fullRootExteriorBracketAtom r n α β γ * fullRootExteriorAction r n = fullRootExteriorPolynomialAction r n γ * (actualExteriorRootContraction (PolynomialSpace r n) β * actualExteriorRootContraction (PolynomialSpace r n) α)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorAction_bracket_anticommute (r n : ℕ) : fullRootExteriorAction r n * fullRootExteriorBracket r n + fullRootExteriorBracket r n * fullRootExteriorAction r n = ∑ α : PositiveRoot r, ∑ β : PositiveRoot r, if α < β then ∑ γ : PositiveRoot r, rootStructureConstant α β γ • (fullRootExteriorPolynomialAction r n γ * (actualExteriorRootContraction (PolynomialSpace r n) β * actualExteriorRootContraction (PolynomialSpace r n) α)) else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorAction_square_add_mixed_eq_zero (r n : ℕ) : fullRootExteriorAction r n * fullRootExteriorAction r n + fullRootExteriorAction r n * fullRootExteriorBracket r n + fullRootExteriorBracket r n * fullRootExteriorAction r n = 0

@[instance_reducible]

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootExteriorBridgeDecidableEq (r : ℕ) : DecidableEq (PositiveRoot r)

The positive root exterior bridge decidable eq used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootExteriorBridgeDecidableEq r = LinearOrder.toDecidableEq

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorBracketAtom_single_apply {r n k : ℕ} (S : RootWedge r (k + 1)) (T : RootWedge r k) (α β γ : PositiveRoot r) (p : PolynomialSpace r n) : (fullRootExteriorBracketAtom r n α β γ) (Pi.single (↑S) p) ↑T = if α ∈ ↑S ∧ β ∈ (↑S).erase α ∧ γ ∉ ((↑S).erase α).erase β ∧ ↑T = insert γ (((↑S).erase α).erase β) then (realExteriorRootSign (↑S) α * realExteriorRootSign ((↑S).erase α) β * realExteriorRootSign (↑T) γ) • p else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorBracket_single_apply {r n k : ℕ} (S : RootWedge r (k + 1)) (T : RootWedge r k) (p : PolynomialSpace r n) : (fullRootExteriorBracket r n) (Pi.single (↑S) p) ↑T = rootBracketBoundaryCoefficient S T • p

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorBracket_zeroExtension_apply {r n k : ℕ} (f : RootPolynomialChain r n (k + 1)) (T : RootWedge r k) : (fullRootExteriorBracket r n) ((rootPolynomialChainZeroExtension r n (k + 1)) f) ↑T = (rootBracketBoundary r n k) f T

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.two_smul_sum_mul_sum_eq_sum_anticommutator {ι : Type u_1} {V : Type u_2} [Fintype ι] [AddCommGroup V] [Module ℝ V] (A : ι → Module.End ℝ V) : 2 • ((∑ i : ι, A i) * ∑ i : ι, A i) = ∑ i : ι, ∑ j : ι, (A i * A j + A j * A i)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.smul_operator_anticommutator {V : Type u_1} [AddCommGroup V] [Module ℝ V] (a b : ℝ) (A B : Module.End ℝ V) : a • A * b • B + b • B * a • A = (a * b) • (A * B + B * A)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorCubicIncidenceOne (r n : ℕ) : Module.End ℝ (FullRootExteriorPolynomialChain r n)

The cubic bracket contribution in which the second structure constant outputs the first input root.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorCubicIncidenceTwo (r n : ℕ) : Module.End ℝ (FullRootExteriorPolynomialChain r n)

The cubic bracket contribution in which the second structure constant outputs the second input root.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorCubicIncidenceThree (r n : ℕ) : Module.End ℝ (FullRootExteriorPolynomialChain r n)

The cubic bracket contribution using the first bracket's output as the next bracket's first input.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorCubicIncidenceFour (r n : ℕ) : Module.End ℝ (FullRootExteriorPolynomialChain r n)

The cubic bracket contribution using the first bracket's output as the next bracket's second input.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorBracketUnordered_square_eq_cubicIncidences (r n : ℕ) : 2 • (fullRootExteriorBracketUnordered r n * fullRootExteriorBracketUnordered r n) = fullRootExteriorCubicIncidenceOne r n - fullRootExteriorCubicIncidenceTwo r n + fullRootExteriorCubicIncidenceThree r n - fullRootExteriorCubicIncidenceFour r n

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.actualExteriorRootContraction_triple_cyclic {r n : ℕ} (a b c : PositiveRoot r) : actualExteriorRootContraction (PolynomialSpace r n) a * (actualExteriorRootContraction (PolynomialSpace r n) b * actualExteriorRootContraction (PolynomialSpace r n) c) = actualExteriorRootContraction (PolynomialSpace r n) b * (actualExteriorRootContraction (PolynomialSpace r n) c * actualExteriorRootContraction (PolynomialSpace r n) a)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootStructureConstant_exteriorJacobi_sum_zero {r n : ℕ} (γ : PositiveRoot r) : ∑ x : PositiveRoot r × PositiveRoot r × PositiveRoot r, (∑ a : PositiveRoot r, rootStructureConstant x.2.1 x.2.2 a * rootStructureConstant x.1 a γ) • (actualExteriorRootCreation (PolynomialSpace r n) γ * (actualExteriorRootContraction (PolynomialSpace r n) x.1 * (actualExteriorRootContraction (PolynomialSpace r n) x.2.1 * actualExteriorRootContraction (PolynomialSpace r n) x.2.2))) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorBracket_incidence_sum_zero (r n : ℕ) : ∑ α : PositiveRoot r, ∑ β : PositiveRoot r, ∑ γ : PositiveRoot r, ∑ δ : PositiveRoot r, ∑ ε : PositiveRoot r, (rootStructureConstant α β γ * rootStructureConstant δ ε α) • (actualExteriorRootCreation (PolynomialSpace r n) γ * (actualExteriorRootContraction (PolynomialSpace r n) β * (actualExteriorRootContraction (PolynomialSpace r n) ε * actualExteriorRootContraction (PolynomialSpace r n) δ))) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorCubicIncidenceTwo_eq_neg (r n : ℕ) : fullRootExteriorCubicIncidenceTwo r n = -fullRootExteriorCubicIncidenceOne r n

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorCubicIncidenceThree_eq (r n : ℕ) : fullRootExteriorCubicIncidenceThree r n = fullRootExteriorCubicIncidenceOne r n

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorCubicIncidenceFour_eq_neg (r n : ℕ) : fullRootExteriorCubicIncidenceFour r n = -fullRootExteriorCubicIncidenceOne r n

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorCubicIncidenceOne_eq_zero (r n : ℕ) : fullRootExteriorCubicIncidenceOne r n = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorBracketUnordered_mul_self_zero (r n : ℕ) : fullRootExteriorBracketUnordered r n * fullRootExteriorBracketUnordered r n = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorBracket_mul_self_zero (r n : ℕ) : fullRootExteriorBracket r n * fullRootExteriorBracket r n = 0

@[instance_reducible]

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootGradedMixedDecidableEq (r : ℕ) : DecidableEq (PositiveRoot r)

The positive root graded mixed decidable eq used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootGradedMixedDecidableEq r = LinearOrder.toDecidableEq

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorAction_zeroExtension_of_card_ne {r n k : ℕ} (f : RootPolynomialChain r n (k + 1)) (S : Finset (PositiveRoot r)) (hS : S.card ≠ k) : (fullRootExteriorAction r n) ((rootPolynomialChainZeroExtension r n (k + 1)) f) S = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorAction_zeroExtension_eq_zeroExtension {r n k : ℕ} (f : RootPolynomialChain r n (k + 1)) : (fullRootExteriorAction r n) ((rootPolynomialChainZeroExtension r n (k + 1)) f) = (rootPolynomialChainZeroExtension r n k) ((rootActionBoundary r n k) f)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorBracketAtom_zeroExtension_of_card_ne {r n k : ℕ} (f : RootPolynomialChain r n (k + 1)) (S : Finset (PositiveRoot r)) (hS : S.card ≠ k) (α β γ : PositiveRoot r) : (fullRootExteriorBracketAtom r n α β γ) ((rootPolynomialChainZeroExtension r n (k + 1)) f) S = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorBracket_zeroExtension_of_card_ne {r n k : ℕ} (f : RootPolynomialChain r n (k + 1)) (S : Finset (PositiveRoot r)) (hS : S.card ≠ k) : (fullRootExteriorBracket r n) ((rootPolynomialChainZeroExtension r n (k + 1)) f) S = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorBracket_zeroExtension_eq_zeroExtension_of_apply {r n k : ℕ} (f : RootPolynomialChain r n (k + 1)) (happly : ∀ (T : RootWedge r k), (fullRootExteriorBracket r n) ((rootPolynomialChainZeroExtension r n (k + 1)) f) ↑T = (rootBracketBoundary r n k) f T) : (fullRootExteriorBracket r n) ((rootPolynomialChainZeroExtension r n (k + 1)) f) = (rootPolynomialChainZeroExtension r n k) ((rootBracketBoundary r n k) f)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootActionBracketBoundary_mixed_square_eq_zero_of_bridge {r n k : ℕ} (f : RootPolynomialChain r n (k + 2)) (T : RootWedge r k) (hbridge : ∀ (j : ℕ) (g : RootPolynomialChain r n (j + 1)) (U : RootWedge r j), (fullRootExteriorBracket r n) ((rootPolynomialChainZeroExtension r n (j + 1)) g) ↑U = (rootBracketBoundary r n j) g U) : (rootActionBoundary r n k) ((rootActionBoundary r n (k + 1)) f) T + (rootActionBoundary r n k) ((rootBracketBoundary r n (k + 1)) f) T + (rootBracketBoundary r n k) ((rootActionBoundary r n (k + 1)) f) T = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorBracket_zeroExtension_eq_zeroExtension {r n k : ℕ} (f : RootPolynomialChain r n (k + 1)) : (fullRootExteriorBracket r n) ((rootPolynomialChainZeroExtension r n (k + 1)) f) = (rootPolynomialChainZeroExtension r n k) ((rootBracketBoundary r n k) f)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootActionBracketBoundary_mixed_square_eq_zero {r n k : ℕ} (f : RootPolynomialChain r n (k + 2)) (T : RootWedge r k) : (rootActionBoundary r n k) ((rootActionBoundary r n (k + 1)) f) T + (rootActionBoundary r n k) ((rootBracketBoundary r n (k + 1)) f) T + (rootBracketBoundary r n k) ((rootActionBoundary r n (k + 1)) f) T = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootBracketBoundary_comp_self_apply_eq_zero {r n k : ℕ} (f : RootPolynomialChain r n (k + 2)) (T : RootWedge r k) : (rootBracketBoundary r n k) ((rootBracketBoundary r n (k + 1)) f) T = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorLowerRootStructureIncidence_zeroExtension_apply {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (f : RootJointHarmonicChain n lam k) (S : AdmissibleRootWedge lam k) : (fullRootExteriorLowerRootStructureIncidence r n) ((rootPolynomialChainZeroExtension r n k) ((rootJointHarmonicPolynomialInclusion n lam k) f)) ↑↑S = -↑↑((rootJointHarmonicActionLowerRootStructureCross n lam k) f S)

@[instance_reducible]

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootHodgeLowerDecidableEq (r : ℕ) : DecidableEq (PositiveRoot r)

The positive root hodge lower decidable eq used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootHodgeLowerDecidableEq r = LinearOrder.toDecidableEq

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.actualOrderedRootBracketCoboundaryAtom_single_transpose {r n k : ℕ} (S : RootWedge r (k + 1)) (T : RootWedge r k) (α β γ : PositiveRoot r) (p : PolynomialSpace r n) : (actualExteriorRootCreation (PolynomialSpace r n) α * (actualExteriorRootCreation (PolynomialSpace r n) β * actualExteriorRootContraction (PolynomialSpace r n) γ)) (Pi.single (↑T) p) ↑S = (fullRootExteriorBracketAtom r n α β γ) (Pi.single (↑S) p) ↑T

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.actualOrderedRootBracketCoboundary_single_apply {r n k : ℕ} (S : RootWedge r (k + 1)) (T : RootWedge r k) (p : PolynomialSpace r n) : actualOrderedRootBracketCoboundary (Pi.single (↑T) p) ↑S = rootBracketBoundaryCoefficient S T • p

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.actualOrderedRootBracketCoboundary_zeroExtension_apply {r n k : ℕ} (f : RootPolynomialChain r n k) (S : RootWedge r (k + 1)) : actualOrderedRootBracketCoboundary ((rootPolynomialChainZeroExtension r n k) f) ↑S = (rootBracketCoboundary r n k) f S

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.actualOrderedRootBracketCoboundary_zeroExtension {r n k : ℕ} (f : RootPolynomialChain r n k) : actualOrderedRootBracketCoboundary ((rootPolynomialChainZeroExtension r n k) f) = (rootPolynomialChainZeroExtension r n (k + 1)) ((rootBracketCoboundary r n k) f)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicBracketActionMixed_add_lowerStructure_eq_zero {r n k : ℕ} (lam : Fin (r + 1) → ℕ) : rootJointHarmonicBracketActionMixed n lam k + rootJointHarmonicActionLowerRootStructureCross n lam (k + 1) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.actualExteriorRootCreation_creation_contraction_contraction_anticommute {ι : Type u_1} {M : Type u_2} [LinearOrder ι] [AddCommGroup M] [Module ℝ M] (a b c d : ι) : actualExteriorRootCreation M a * (actualExteriorRootCreation M b * (actualExteriorRootContraction M c * actualExteriorRootContraction M d)) + actualExteriorRootCreation M b * (actualExteriorRootContraction M c * actualExteriorRootContraction M d) * actualExteriorRootCreation M a = (if a = d then actualExteriorRootCreation M b * actualExteriorRootContraction M c else 0) - if a = c then actualExteriorRootCreation M b * actualExteriorRootContraction M d else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorUpperPolynomialAction_creation_commute {r n : ℕ} (α β : PositiveRoot r) : fullRootExteriorUpperPolynomialAction r n α * actualExteriorRootCreation (PolynomialSpace r n) β = actualExteriorRootCreation (PolynomialSpace r n) β * fullRootExteriorUpperPolynomialAction r n α

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorUpperPolynomialAction_contraction_commute {r n : ℕ} (α β : PositiveRoot r) : fullRootExteriorUpperPolynomialAction r n α * actualExteriorRootContraction (PolynomialSpace r n) β = actualExteriorRootContraction (PolynomialSpace r n) β * fullRootExteriorUpperPolynomialAction r n α

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorUpperActionAtom (r n : ℕ) (α : PositiveRoot r) : Module.End ℝ (FullRootExteriorPolynomialChain r n)

The upper polynomial action composed with exterior creation of the same root.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorUpperPolynomialAction_bracketAtom_commute {r n : ℕ} (δ α β γ : PositiveRoot r) : fullRootExteriorUpperPolynomialAction r n δ * fullRootExteriorBracketAtom r n α β γ = fullRootExteriorBracketAtom r n α β γ * fullRootExteriorUpperPolynomialAction r n δ

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorUpperActionAtom_bracketAtom_anticommute {r n : ℕ} (δ α β γ : PositiveRoot r) : fullRootExteriorUpperActionAtom r n δ * fullRootExteriorBracketAtom r n α β γ + fullRootExteriorBracketAtom r n α β γ * fullRootExteriorUpperActionAtom r n δ = (if δ = α then fullRootExteriorUpperPolynomialAction r n α * (actualExteriorRootCreation (PolynomialSpace r n) γ * actualExteriorRootContraction (PolynomialSpace r n) β) else 0) - if δ = β then fullRootExteriorUpperPolynomialAction r n β * (actualExteriorRootCreation (PolynomialSpace r n) γ * actualExteriorRootContraction (PolynomialSpace r n) α) else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorActionCoboundary_bracketAtom_anticommute {r n : ℕ} (α β γ : PositiveRoot r) : fullRootExteriorActionCoboundary r n * fullRootExteriorBracketAtom r n α β γ + fullRootExteriorBracketAtom r n α β γ * fullRootExteriorActionCoboundary r n = fullRootExteriorUpperPolynomialAction r n α * (actualExteriorRootCreation (PolynomialSpace r n) γ * actualExteriorRootContraction (PolynomialSpace r n) β) - fullRootExteriorUpperPolynomialAction r n β * (actualExteriorRootCreation (PolynomialSpace r n) γ * actualExteriorRootContraction (PolynomialSpace r n) α)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorActionCoboundary_bracket_anticommute (r n : ℕ) : fullRootExteriorActionCoboundary r n * fullRootExteriorBracket r n + fullRootExteriorBracket r n * fullRootExteriorActionCoboundary r n = ∑ α : PositiveRoot r, ∑ β : PositiveRoot r, if α < β then ∑ γ : PositiveRoot r, rootStructureConstant α β γ • (fullRootExteriorUpperPolynomialAction r n α * (actualExteriorRootCreation (PolynomialSpace r n) γ * actualExteriorRootContraction (PolynomialSpace r n) β) - fullRootExteriorUpperPolynomialAction r n β * (actualExteriorRootCreation (PolynomialSpace r n) γ * actualExteriorRootContraction (PolynomialSpace r n) α)) else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorUpperStructureAtom_apply {r n : ℕ} (α β γ : PositiveRoot r) (f : FullRootExteriorPolynomialChain r n) (S : Finset (PositiveRoot r)) : (fullRootExteriorUpperPolynomialAction r n γ * (actualExteriorRootCreation (PolynomialSpace r n) α * actualExteriorRootContraction (PolynomialSpace r n) β)) f S = if _hα : α ∈ S then if _hβ : β ∈ S.erase α then 0 else (realExteriorRootSign S α * realExteriorRootSign (insert β (S.erase α)) β) • (positiveRootUpperOperator n γ) (f (insert β (S.erase α))) else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicActionUpperRootStructureCross_apply_coe {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (f : RootJointHarmonicChain n lam k) (S : AdmissibleRootWedge lam k) : ↑↑((rootJointHarmonicActionUpperRootStructureCross n lam k) f S) = ∑ α : PositiveRoot r, if hα : α ∈ ↑↑S then ∑ β : PositiveRoot r, if hβ : β ∈ ↑↑S then 0 else if hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert β ((↑↑S).erase α)) i then ∑ γ : PositiveRoot r, if _hγ : rootStructureConstant β γ α = 0 then 0 else (rootSwapExteriorHodgeSign S α β * rootStructureConstant β γ α) • (polarization r n (positiveRootFirst γ) (positiveRootSecond γ)) ↑↑(f (rootAdmissibleSwap lam S α β hα hβ hadm)) else 0 else 0

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicActionBracketMixed {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (k : ℕ) : RootJointHarmonicChain n lam (k + 1) →ₗ[ℝ] RootJointHarmonicChain n lam (k + 1)

The two mixed compositions of the action coboundary and bracket boundary on joint harmonic chains.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicFullMixedHodge {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (k : ℕ) : RootJointHarmonicChain n lam (k + 1) →ₗ[ℝ] RootJointHarmonicChain n lam (k + 1)

The four mixed action-bracket terms in the weighted Hodge operator on joint harmonic chains.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicFullMixedHodge_eq_halves {r n k : ℕ} (lam : Fin (r + 1) → ℕ) : rootJointHarmonicFullMixedHodge n lam k = rootJointHarmonicActionBracketMixed n lam k + (weightedRootBracketCoboundary n lam k ∘ₗ weightedExteriorActionDifferential n lam k + weightedExteriorActionDifferential n lam (k + 1) ∘ₗ weightedRootBracketCoboundary n lam (k + 1))

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicFullMixedHodge_eq_actionBracket_add_bracketAction {r n k : ℕ} (lam : Fin (r + 1) → ℕ) : rootJointHarmonicFullMixedHodge n lam k = rootJointHarmonicActionBracketMixed n lam k + rootJointHarmonicBracketActionMixed n lam k

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicFullMixedHodge_add_offDiagonal_eq_zero_of_halves {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (hupper : rootJointHarmonicActionBracketMixed n lam k + rootJointHarmonicActionUpperRootStructureCross n lam (k + 1) = 0) (hlower : rootJointHarmonicBracketActionMixed n lam k + rootJointHarmonicActionLowerRootStructureCross n lam (k + 1) = 0) : rootJointHarmonicFullMixedHodge n lam k + rootJointHarmonicActionHodgeOffDiagonal n lam (k + 1) = 0

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootPolynomialActionBracketMixed (r n k : ℕ) : RootPolynomialChain r n (k + 1) →ₗ[ℝ] RootPolynomialChain r n (k + 1)

The mixed action-coboundary and bracket-boundary operator on polynomial chains.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicPolynomialInclusion_actionBracketMixed_intertwines {r n k : ℕ} (lam : Fin (r + 1) → ℕ) : rootJointHarmonicPolynomialInclusion n lam (k + 1) ∘ₗ rootJointHarmonicActionBracketMixed n lam k = rootPolynomialActionBracketMixed r n k ∘ₗ rootJointHarmonicPolynomialInclusion n lam (k + 1)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorUpperRootStructureIncidence (r n : ℕ) : Module.End ℝ (FullRootExteriorPolynomialChain r n)

The structure-constant sum coupling upper polynomial action, root creation, and root contraction.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootStructureConstant_output_eq_left_zero {r : ℕ} (α β : PositiveRoot r) : rootStructureConstant α β α = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.sum_root_pairs_eq_ordered_add_reverse {r : ℕ} {V : Type u_1} [AddCommGroup V] (F : PositiveRoot r → PositiveRoot r → V) (hzero : ∀ (α β : PositiveRoot r), ¬α < β → ¬β < α → F α β = 0) : ∑ α : PositiveRoot r, ∑ β : PositiveRoot r, F α β = ∑ α : PositiveRoot r, ∑ β : PositiveRoot r, if α < β then F α β + F β α else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorActionCoboundary_bracket_eq_neg_upperStructure (r n : ℕ) : fullRootExteriorActionCoboundary r n * fullRootExteriorBracket r n + fullRootExteriorBracket r n * fullRootExteriorActionCoboundary r n = -fullRootExteriorUpperRootStructureIncidence r n

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorUpperRootStructureIncidence_zeroExtension_apply {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (f : RootJointHarmonicChain n lam k) (S : AdmissibleRootWedge lam k) : (fullRootExteriorUpperRootStructureIncidence r n) ((rootPolynomialChainZeroExtension r n k) ((rootJointHarmonicPolynomialInclusion n lam k) f)) ↑↑S = ↑↑((rootJointHarmonicActionUpperRootStructureCross n lam k) f S)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicActionBracketMixed_add_upperStructure_eq_zero {r n k : ℕ} (lam : Fin (r + 1) → ℕ) : rootJointHarmonicActionBracketMixed n lam k + rootJointHarmonicActionUpperRootStructureCross n lam (k + 1) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootChevalleyEilenbergBoundary_comp_self_of_actionBracket (r n k : ℕ) (ha : rootActionBoundary r n k ∘ₗ rootActionBoundary r n (k + 1) + rootActionBoundary r n k ∘ₗ rootBracketBoundary r n (k + 1) + rootBracketBoundary r n k ∘ₗ rootActionBoundary r n (k + 1) = 0) (hb : rootBracketBoundary r n k ∘ₗ rootBracketBoundary r n (k + 1) = 0) : rootChevalleyEilenbergBoundary r n k ∘ₗ rootChevalleyEilenbergBoundary r n (k + 1) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedChevalleyEilenbergDifferential_comp_self_of_unweighted {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (h : rootChevalleyEilenbergBoundary r n k ∘ₗ rootChevalleyEilenbergBoundary r n (k + 1) = 0) : weightedChevalleyEilenbergDifferential n lam k ∘ₗ weightedChevalleyEilenbergDifferential n lam (k + 1) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.fischerCore_injective_of_coercive_add_adjoint_squares {E : Type u_1} {F : Type u_2} {G : Type u_3} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [AddCommGroup G] [Module ℝ G] (cE : InnerProductSpace.Core ℝ E) (cF : InnerProductSpace.Core ℝ F) (cG : InnerProductSpace.Core ℝ G) (L : F →ₗ[ℝ] F) (B : F →ₗ[ℝ] E) (Bstar : E →ₗ[ℝ] F) (C : G →ₗ[ℝ] F) (Cstar : F →ₗ[ℝ] G) (hBstar : ∀ (x : E) (y : F), inner ℝ (Bstar x) y = inner ℝ x (B y)) (hCstar : ∀ (x : F) (y : G), inner ℝ (Cstar x) y = inner ℝ x (C y)) (hL : ∀ (x : F), x ≠ 0 → 0 < inner ℝ x (L x)) : Function.Injective ⇑(L + Bstar ∘ₗ B + C ∘ₗ Cstar)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedChevalleyEilenbergCoboundary {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (k : ℕ) : RootJointHarmonicChain n lam k →ₗ[ℝ] RootJointHarmonicChain n lam (k + 1)

The weighted Chevalley-Eilenberg coboundary, combining the action and root-bracket coboundaries.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedChevalleyEilenberg_fischer_adjoint {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (p : RootJointHarmonicChain n lam (k + 1)) (q : RootJointHarmonicChain n lam k) : inner ℝ ((weightedChevalleyEilenbergDifferential n lam k) p) q = inner ℝ p ((weightedChevalleyEilenbergCoboundary n lam k) q)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedChevalleyEilenberg_fischer_adjoint_reverse {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (q : RootJointHarmonicChain n lam k) (p : RootJointHarmonicChain n lam (k + 1)) : inner ℝ ((weightedChevalleyEilenbergCoboundary n lam k) q) p = inner ℝ q ((weightedChevalleyEilenbergDifferential n lam k) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedRootBracketBoundary_fischer_adjoint_reverse {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (q : RootJointHarmonicChain n lam k) (p : RootJointHarmonicChain n lam (k + 1)) : inner ℝ ((weightedRootBracketCoboundary n lam k) q) p = inner ℝ q ((weightedRootBracketBoundary n lam k) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.bgg_chain_range_eq_ker_of_coercive_add_adjoint_squares {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (d : RootJointHarmonicChain n lam (k + 1) →ₗ[ℝ] RootJointHarmonicChain n lam k) (dStar : RootJointHarmonicChain n lam k →ₗ[ℝ] RootJointHarmonicChain n lam (k + 1)) (e : RootJointHarmonicChain n lam (k + 1 + 1) →ₗ[ℝ] RootJointHarmonicChain n lam (k + 1)) (eStar : RootJointHarmonicChain n lam (k + 1) →ₗ[ℝ] RootJointHarmonicChain n lam (k + 1 + 1)) (L : RootJointHarmonicChain n lam (k + 1) →ₗ[ℝ] RootJointHarmonicChain n lam (k + 1)) (B : RootJointHarmonicChain n lam (k + 1) →ₗ[ℝ] RootJointHarmonicChain n lam k) (Bstar : RootJointHarmonicChain n lam k →ₗ[ℝ] RootJointHarmonicChain n lam (k + 1)) (C : RootJointHarmonicChain n lam (k + 1 + 1) →ₗ[ℝ] RootJointHarmonicChain n lam (k + 1)) (Cstar : RootJointHarmonicChain n lam (k + 1) →ₗ[ℝ] RootJointHarmonicChain n lam (k + 1 + 1)) (hdStar : ∀ (x : RootJointHarmonicChain n lam k) (y : RootJointHarmonicChain n lam (k + 1)), inner ℝ (dStar x) y = inner ℝ x (d y)) (heStar : ∀ (x : RootJointHarmonicChain n lam (k + 1)) (y : RootJointHarmonicChain n lam (k + 1 + 1)), inner ℝ (eStar x) y = inner ℝ x (e y)) (hBstar : ∀ (x : RootJointHarmonicChain n lam k) (y : RootJointHarmonicChain n lam (k + 1)), inner ℝ (Bstar x) y = inner ℝ x (B y)) (hCstar : ∀ (x : RootJointHarmonicChain n lam (k + 1)) (y : RootJointHarmonicChain n lam (k + 1 + 1)), inner ℝ (Cstar x) y = inner ℝ x (C y)) (hchain : d ∘ₗ e = 0) (hdecomposition : dStar ∘ₗ d + e ∘ₗ eStar = L + Bstar ∘ₗ B + C ∘ₗ Cstar) (hL : ∀ (x : RootJointHarmonicChain n lam (k + 1)), x ≠ 0 → 0 < inner ℝ x (L x)) : e.range = d.ker

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedChevalleyEilenberg_exact_of_hodge_diagonal {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (L : RootJointHarmonicChain n lam (k + 1) →ₗ[ℝ] RootJointHarmonicChain n lam (k + 1)) (hchain : weightedChevalleyEilenbergDifferential n lam k ∘ₗ weightedChevalleyEilenbergDifferential n lam (k + 1) = 0) (hmixed : weightedExteriorActionCoboundary n lam k ∘ₗ weightedExteriorActionDifferential n lam k + weightedExteriorActionDifferential n lam (k + 1) ∘ₗ weightedExteriorActionCoboundary n lam (k + 1) + (weightedExteriorActionCoboundary n lam k ∘ₗ weightedRootBracketBoundary n lam k + weightedRootBracketCoboundary n lam k ∘ₗ weightedExteriorActionDifferential n lam k + weightedExteriorActionDifferential n lam (k + 1) ∘ₗ weightedRootBracketCoboundary n lam (k + 1) + weightedRootBracketBoundary n lam (k + 1) ∘ₗ weightedExteriorActionCoboundary n lam (k + 1)) = L) (hLge : ∀ (f : RootJointHarmonicChain n lam (k + 1)), inner ℝ f ((rootJointHarmonicIncludedDescendingFischerLaplacian n lam (k + 1)) f) ≤ inner ℝ f (L f)) : (weightedChevalleyEilenbergDifferential n lam (k + 1)).range = (weightedChevalleyEilenbergDifferential n lam k).ker

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonic_action_plus_mixed_hodge_eq_diagonal_of_cross_cancellation {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (haction : weightedExteriorActionCoboundary n lam k ∘ₗ weightedExteriorActionDifferential n lam k + weightedExteriorActionDifferential n lam (k + 1) ∘ₗ weightedExteriorActionCoboundary n lam (k + 1) = rootJointHarmonicHodgeDiagonal n lam (k + 1) + rootJointHarmonicActionHodgeOffDiagonal n lam (k + 1)) (hmixed : rootJointHarmonicFullMixedHodge n lam k + rootJointHarmonicActionHodgeOffDiagonal n lam (k + 1) = 0) : weightedExteriorActionCoboundary n lam k ∘ₗ weightedExteriorActionDifferential n lam k + weightedExteriorActionDifferential n lam (k + 1) ∘ₗ weightedExteriorActionCoboundary n lam (k + 1) + rootJointHarmonicFullMixedHodge n lam k = rootJointHarmonicHodgeDiagonal n lam (k + 1)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedChevalleyEilenberg_mixed_hodge_eq_diagonal_of_root_cross_halves {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (haction : weightedExteriorActionCoboundary n lam k ∘ₗ weightedExteriorActionDifferential n lam k + weightedExteriorActionDifferential n lam (k + 1) ∘ₗ weightedExteriorActionCoboundary n lam (k + 1) = rootJointHarmonicHodgeDiagonal n lam (k + 1) + rootJointHarmonicActionHodgeOffDiagonal n lam (k + 1)) (hupper : rootJointHarmonicActionBracketMixed n lam k + rootJointHarmonicActionUpperRootStructureCross n lam (k + 1) = 0) (hlower : rootJointHarmonicBracketActionMixed n lam k + rootJointHarmonicActionLowerRootStructureCross n lam (k + 1) = 0) : weightedExteriorActionCoboundary n lam k ∘ₗ weightedExteriorActionDifferential n lam k + weightedExteriorActionDifferential n lam (k + 1) ∘ₗ weightedExteriorActionCoboundary n lam (k + 1) + (weightedExteriorActionCoboundary n lam k ∘ₗ weightedRootBracketBoundary n lam k + weightedRootBracketCoboundary n lam k ∘ₗ weightedExteriorActionDifferential n lam k + weightedExteriorActionDifferential n lam (k + 1) ∘ₗ weightedRootBracketCoboundary n lam (k + 1) + weightedRootBracketBoundary n lam (k + 1) ∘ₗ weightedExteriorActionCoboundary n lam (k + 1)) = rootJointHarmonicHodgeDiagonal n lam (k + 1)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootActionBracketBoundary_mixed_comp_self_zero (r n k : ℕ) : rootActionBoundary r n k ∘ₗ rootActionBoundary r n (k + 1) + rootActionBoundary r n k ∘ₗ rootBracketBoundary r n (k + 1) + rootBracketBoundary r n k ∘ₗ rootActionBoundary r n (k + 1) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootBracketBoundary_comp_self_zero (r n k : ℕ) : rootBracketBoundary r n k ∘ₗ rootBracketBoundary r n (k + 1) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootChevalleyEilenbergBoundary_comp_self_zero (r n k : ℕ) : rootChevalleyEilenbergBoundary r n k ∘ₗ rootChevalleyEilenbergBoundary r n (k + 1) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedChevalleyEilenbergDifferential_comp_self_zero {r n k : ℕ} (lam : Fin (r + 1) → ℕ) : weightedChevalleyEilenbergDifferential n lam k ∘ₗ weightedChevalleyEilenbergDifferential n lam (k + 1) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedChevalleyEilenberg_exact_of_hodge_root_identities {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (haction : weightedExteriorActionCoboundary n lam k ∘ₗ weightedExteriorActionDifferential n lam k + weightedExteriorActionDifferential n lam (k + 1) ∘ₗ weightedExteriorActionCoboundary n lam (k + 1) = rootJointHarmonicHodgeDiagonal n lam (k + 1) + rootJointHarmonicActionHodgeOffDiagonal n lam (k + 1)) (hupper : rootJointHarmonicActionBracketMixed n lam k + rootJointHarmonicActionUpperRootStructureCross n lam (k + 1) = 0) (hlower : rootJointHarmonicBracketActionMixed n lam k + rootJointHarmonicActionLowerRootStructureCross n lam (k + 1) = 0) : (weightedChevalleyEilenbergDifferential n lam (k + 1)).range = (weightedChevalleyEilenbergDifferential n lam k).ker

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedChevalleyEilenberg_exact {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) : (weightedChevalleyEilenbergDifferential n lam (k + 1)).range = (weightedChevalleyEilenbergDifferential n lam k).ker

theorem MetricCodes.Spherical.HigherHarmonicYoung.weyl_dimension_eq_finrank_harmonicYoung {r n : ℕ} (hn : 2 * r + 4 ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) : HigherHierarchy.Weyl.dimension n lam = ↑(Module.finrank ℝ ↥(HarmonicYoungSpace lam))

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankFischerGramWeylRecurrence.finrank_raiseWeight_eq_finrank_mul_weylEdgeRatio {r n : ℕ} (low : Fin (r + 1) → ℕ) (mu : Fin r → ℕ) (row : Fin (r + 1)) (hlow : HigherChannel.FiniteInterlacing n low mu) (hhigh : HigherChannel.FiniteInterlacing n (HigherChannel.raiseWeight low row) mu) : ↑(Module.finrank ℝ ↥(HarmonicYoungSpace (HigherChannel.raiseWeight low row))) = ↑(Module.finrank ℝ ↥(HarmonicYoungSpace low)) * HigherChannel.weylEdgeRatio n low row

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankFischerGramWeylRecurrence.arbitraryRowRaiseTensorGramScalar_eq_lowerGram_mul_weylEdgeRatio {r n : ℕ} (low : Fin (r + 1) → ℕ) (mu : Fin r → ℕ) (row : Fin (r + 1)) (hlow : HigherChannel.FiniteInterlacing n low mu) (hhigh : HigherChannel.FiniteInterlacing n (HigherChannel.raiseWeight low row) mu) : ArbitraryRowRaiseLowerTensorTrace.arbitraryRowRaiseTensorGramScalar (HigherChannel.raiseWeight low row) row = ArbitraryRankInternalRowLowerGram.internalRowLowerGramScalar (HigherChannel.raiseWeight low row) row * HigherChannel.weylEdgeRatio n low row

noncomputable def MetricCodes.Spherical.HigherYoungArbitraryRankColumnHighestCoefficientDescent.sourceMatrixTranspose (m : ℕ) : HigherHarmonicYoung.BideterminantHighestLine.SourceMatrix m ≃ₐ[ℂ] HigherHarmonicYoung.BideterminantHighestLine.SourceMatrix m

The polynomial-algebra automorphism that transposes the two indices of each source matrix variable.

Equations

• MetricCodes.Spherical.HigherYoungArbitraryRankColumnHighestCoefficientDescent.sourceMatrixTranspose m = MvPolynomial.renameEquiv ℂ (Equiv.prodComm (Fin m) (Fin m))

noncomputable def MetricCodes.Spherical.HigherYoungArbitraryRankColumnHighestCoefficientDescent.sourceExponentTranspose {m : ℕ} (d : Fin m × Fin m →₀ ℕ) : Fin m × Fin m →₀ ℕ

Transpose the row and column indices of a source matrix monomial's exponent vector.

Equations

• MetricCodes.Spherical.HigherYoungArbitraryRankColumnHighestCoefficientDescent.sourceExponentTranspose d = Finsupp.mapDomain (⇑(Equiv.prodComm (Fin m) (Fin m))) d

@[simp]

theorem MetricCodes.Spherical.HigherYoungArbitraryRankColumnHighestCoefficientDescent.sourceMatrixTranspose_X {m : ℕ} (i j : Fin m) : (sourceMatrixTranspose m) (MvPolynomial.X (i, j)) = MvPolynomial.X (j, i)

theorem MetricCodes.Spherical.HigherYoungArbitraryRankColumnHighestCoefficientDescent.sourceMatrixTranspose_pderiv {m : ℕ} (i j : Fin m) (p : HigherHarmonicYoung.BideterminantHighestLine.SourceMatrix m) : (sourceMatrixTranspose m) ((MvPolynomial.pderiv (i, j)) p) = (MvPolynomial.pderiv (j, i)) ((sourceMatrixTranspose m) p)

theorem MetricCodes.Spherical.HigherYoungArbitraryRankColumnHighestCoefficientDescent.sourceMatrixTranspose_columnRoot {m : ℕ} (i j : Fin m) (p : HigherHarmonicYoung.BideterminantHighestLine.SourceMatrix m) : (sourceMatrixTranspose m) ((HigherHarmonicYoung.BideterminantHighestLine.sourceColumnRoot i j) p) = (HigherHarmonicYoung.BideterminantHighestLine.sourceRowRoot i j) ((sourceMatrixTranspose m) p)

@[simp]

theorem MetricCodes.Spherical.HigherYoungArbitraryRankColumnHighestCoefficientDescent.sourceExponentTranspose_apply {m : ℕ} (d : Fin m × Fin m →₀ ℕ) (i j : Fin m) : (sourceExponentTranspose d) (i, j) = d (j, i)

@[simp]

theorem MetricCodes.Spherical.HigherYoungArbitraryRankColumnHighestCoefficientDescent.sourceExponentTranspose_transpose {m : ℕ} (d : Fin m × Fin m →₀ ℕ) : sourceExponentTranspose (sourceExponentTranspose d) = d

theorem MetricCodes.Spherical.HigherYoungArbitraryRankColumnHighestCoefficientDescent.sourceMatrixTranspose_coeff {m : ℕ} (p : HigherHarmonicYoung.BideterminantHighestLine.SourceMatrix m) (d : Fin m × Fin m →₀ ℕ) : ((sourceMatrixTranspose m) p).coeff (sourceExponentTranspose d) = p.coeff d

theorem MetricCodes.Spherical.HigherYoungArbitraryRankColumnHighestCoefficientDescent.exists_lowerTriangular_coeff_ne_zero_of_columnHighest {m : ℕ} (p : HigherHarmonicYoung.BideterminantHighestLine.SourceMatrix m) (hp : p ≠ 0) (hhighest : ∀ (i j : Fin m), i < j → (HigherHarmonicYoung.BideterminantHighestLine.sourceColumnRoot i j) p = 0) : ∃ (d : Fin m × Fin m →₀ ℕ), p.coeff d ≠ 0 ∧ ∀ (i j : Fin m), i < j → d (i, j) = 0

def MetricCodes.Spherical.HigherYoungArbitraryRankTriangularMarginDominance.sourceMarginPrefix {m : ℕ} (f : Fin m → ℕ) (k : ℕ) : ℕ

The sum of the first k entries of a row or column margin.

Equations

• MetricCodes.Spherical.HigherYoungArbitraryRankTriangularMarginDominance.sourceMarginPrefix f k = ∑ i : Fin m, if ↑i < k then f i else 0

theorem MetricCodes.Spherical.HigherYoungArbitraryRankTriangularMarginDominance.sourceColumnPrefix_le_sourceRowPrefix_of_upper {m : ℕ} (d : Fin m × Fin m →₀ ℕ) (hupper : ∀ (i j : Fin m), j < i → d (i, j) = 0) (k : ℕ) : sourceMarginPrefix (HigherHarmonicYoung.BideterminantHighestLine.sourceColumnDegree d) k ≤ sourceMarginPrefix (HigherHarmonicYoung.BideterminantHighestLine.sourceRowDegree d) k

theorem MetricCodes.Spherical.HigherYoungArbitraryRankTriangularMarginDominance.sourceRowPrefix_le_sourceColumnPrefix_of_lower {m : ℕ} (d : Fin m × Fin m →₀ ℕ) (hlower : ∀ (i j : Fin m), i < j → d (i, j) = 0) (k : ℕ) : sourceMarginPrefix (HigherHarmonicYoung.BideterminantHighestLine.sourceRowDegree d) k ≤ sourceMarginPrefix (HigherHarmonicYoung.BideterminantHighestLine.sourceColumnDegree d) k

theorem MetricCodes.Spherical.HigherYoungArbitraryRankTriangularMarginDominance.sourceMarginPrefix_succ {m : ℕ} (f : Fin m → ℕ) (i : Fin m) : sourceMarginPrefix f (↑i + 1) = sourceMarginPrefix f ↑i + f i

theorem MetricCodes.Spherical.HigherYoungArbitraryRankTriangularMarginDominance.sourceMargins_eq_of_upper_and_lower {m : ℕ} (lam nu : Fin m → ℕ) (dUpper dLower : Fin m × Fin m →₀ ℕ) (hupper : ∀ (i j : Fin m), j < i → dUpper (i, j) = 0) (hlower : ∀ (i j : Fin m), i < j → dLower (i, j) = 0) (hupperRow : ∀ (i : Fin m), HigherHarmonicYoung.BideterminantHighestLine.sourceRowDegree dUpper i = lam i) (hupperColumn : ∀ (i : Fin m), HigherHarmonicYoung.BideterminantHighestLine.sourceColumnDegree dUpper i = nu i) (hlowerRow : ∀ (i : Fin m), HigherHarmonicYoung.BideterminantHighestLine.sourceRowDegree dLower i = lam i) (hlowerColumn : ∀ (i : Fin m), HigherHarmonicYoung.BideterminantHighestLine.sourceColumnDegree dLower i = nu i) : lam = nu

def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightProjection.columnVariableWeight (m : ℕ) : Fin m × Fin m → Fin m → ℕ

Assign each source matrix variable unit weight in its column coordinate.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightProjection.columnVariableWeight m z = Pi.single z.2 1

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightProjection.columnVariableWeight_weight {m : ℕ} (d : Fin m × Fin m →₀ ℕ) : (Finsupp.weight (columnVariableWeight m)) d = fun (j : Fin m) => BideterminantHighestLine.sourceColumnDegree d j

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightProjection.columnWeightComponent {m : ℕ} (ν : Fin m → ℕ) (p : BideterminantHighestLine.SourceMatrix m) : BideterminantHighestLine.SourceMatrix m

Project a source matrix polynomial to the component with column-degree vector ν.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightProjection.coeff_columnWeightComponent {m : ℕ} (ν : Fin m → ℕ) (p : BideterminantHighestLine.SourceMatrix m) (d : Fin m × Fin m →₀ ℕ) : (columnWeightComponent ν p).coeff d = if (fun (j : Fin m) => BideterminantHighestLine.sourceColumnDegree d j) = ν then p.coeff d else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightProjection.columnWeightComponent_ne_zero_of_coeff_ne_zero {m : ℕ} (p : BideterminantHighestLine.SourceMatrix m) (d : Fin m × Fin m →₀ ℕ) (hd : p.coeff d ≠ 0) : columnWeightComponent (fun (j : Fin m) => BideterminantHighestLine.sourceColumnDegree d j) p ≠ 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightCartan.sourceColumnRoot_self_columnWeightComponent {m : ℕ} (ν : Fin m → ℕ) (p : BideterminantHighestLine.SourceMatrix m) (i : Fin m) : (BideterminantHighestLine.sourceColumnRoot i i) (ArbitraryRankColumnWeightProjection.columnWeightComponent ν p) = ↑(ν i) • ArbitraryRankColumnWeightProjection.columnWeightComponent ν p

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightRowRoot.sourceColumnDegree_add {m : ℕ} (d e : Fin m × Fin m →₀ ℕ) (column : Fin m) : BideterminantHighestLine.sourceColumnDegree (d + e) column = BideterminantHighestLine.sourceColumnDegree d column + BideterminantHighestLine.sourceColumnDegree e column

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightRowRoot.sourceColumnDegree_single {m : ℕ} (row column target : Fin m) (degree : ℕ) : BideterminantHighestLine.sourceColumnDegree (fun₀ | (row, column) => degree) target = if column = target then degree else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightRowRoot.sourceColumnDegree_rowTransfer {m : ℕ} (d : Fin m × Fin m →₀ ℕ) (source target column test : Fin m) (hoccupied : 0 < d (source, column)) : BideterminantHighestLine.sourceColumnDegree ((d - fun₀ | (source, column) => 1) + fun₀ | (target, column) => 1) test = BideterminantHighestLine.sourceColumnDegree d test

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightRowRoot.columnWeightComponent_X_mul_pderiv_row {m : ℕ} (ν : Fin m → ℕ) (p : BideterminantHighestLine.SourceMatrix m) (source target column : Fin m) : MvPolynomial.X (target, column) * (MvPolynomial.pderiv (source, column)) (ArbitraryRankColumnWeightProjection.columnWeightComponent ν p) = ArbitraryRankColumnWeightProjection.columnWeightComponent ν (MvPolynomial.X (target, column) * (MvPolynomial.pderiv (source, column)) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightRowRoot.sourceRowRoot_columnWeightComponent {m : ℕ} (ν : Fin m → ℕ) (p : BideterminantHighestLine.SourceMatrix m) (source target : Fin m) : (BideterminantHighestLine.sourceRowRoot target source) (ArbitraryRankColumnWeightProjection.columnWeightComponent ν p) = ArbitraryRankColumnWeightProjection.columnWeightComponent ν ((BideterminantHighestLine.sourceRowRoot target source) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightRowRoot.columnWeightComponent_rowHighest {m : ℕ} (ν : Fin m → ℕ) (p : BideterminantHighestLine.SourceMatrix m) (hhighest : ∀ (i j : Fin m), i < j → (BideterminantHighestLine.sourceRowRoot i j) p = 0) (i j : Fin m) : i < j → (BideterminantHighestLine.sourceRowRoot i j) (ArbitraryRankColumnWeightProjection.columnWeightComponent ν p) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightRowRoot.columnWeightComponent_rowCartan {m : ℕ} (ν lam : Fin m → ℕ) (p : BideterminantHighestLine.SourceMatrix m) (hcartan : ∀ (i : Fin m), (BideterminantHighestLine.sourceRowRoot i i) p = ↑(lam i) • p) (i : Fin m) : (BideterminantHighestLine.sourceRowRoot i i) (ArbitraryRankColumnWeightProjection.columnWeightComponent ν p) = ↑(lam i) • ArbitraryRankColumnWeightProjection.columnWeightComponent ν p

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightRootShift.columnWeight_shift_sub_single_add {m : ℕ} (d : Fin m × Fin m →₀ ℕ) (k i j : Fin m) (hd : d (k, i) ≠ 0) : (fun (t : Fin m) => BideterminantHighestLine.sourceColumnDegree ((d - fun₀ | (k, i) => 1) + fun₀ | (k, j) => 1) t) + Pi.single i 1 = (fun (t : Fin m) => BideterminantHighestLine.sourceColumnDegree d t) + Pi.single j 1

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightRootShift.coeff_sourceColumnRoot_columnWeightComponent {m : ℕ} (ν : Fin m → ℕ) (p : BideterminantHighestLine.SourceMatrix m) (i j : Fin m) (hij : i ≠ j) (d : Fin m × Fin m →₀ ℕ) : ((BideterminantHighestLine.sourceColumnRoot i j) (ArbitraryRankColumnWeightProjection.columnWeightComponent ν p)).coeff d = if ν + Pi.single i 1 = (fun (t : Fin m) => BideterminantHighestLine.sourceColumnDegree d t) + Pi.single j 1 then ((BideterminantHighestLine.sourceColumnRoot i j) p).coeff d else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightRootShift.columnWeightComponent_columnHighest {m : ℕ} (ν : Fin m → ℕ) (p : BideterminantHighestLine.SourceMatrix m) (i j : Fin m) (hij : i < j) (hhighest : (BideterminantHighestLine.sourceColumnRoot i j) p = 0) : (BideterminantHighestLine.sourceColumnRoot i j) (ArbitraryRankColumnWeightProjection.columnWeightComponent ν p) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightRootShift.columnWeightComponent_columnHighest_all {m : ℕ} (ν : Fin m → ℕ) (p : BideterminantHighestLine.SourceMatrix m) (hhighest : ∀ (i j : Fin m), i < j → (BideterminantHighestLine.sourceColumnRoot i j) p = 0) (i j : Fin m) (hij : i < j) : (BideterminantHighestLine.sourceColumnRoot i j) (ArbitraryRankColumnWeightProjection.columnWeightComponent ν p) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankIsotropicSupportCartanWeight.exists_upperTriangular_coeff_ne_zero_of_rowHighest {m : ℕ} (p : BideterminantHighestLine.SourceMatrix m) (hp : p ≠ 0) (hhighest : ∀ (i j : Fin m), i < j → (BideterminantHighestLine.sourceRowRoot i j) p = 0) : ∃ (d : Fin m × Fin m →₀ ℕ), p.coeff d ≠ 0 ∧ ∀ (i j : Fin m), j < i → d (i, j) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankIsotropicSupportCartanWeight.source_rowWeight_eq_columnWeight_of_biHighest {m : ℕ} (lam nu : Fin m → ℕ) (p : BideterminantHighestLine.SourceMatrix m) (hp : p ≠ 0) (hrow : ∀ (i : Fin m), (BideterminantHighestLine.sourceRowRoot i i) p = ↑(lam i) • p) (hcolumn : ∀ (i : Fin m), (BideterminantHighestLine.sourceColumnRoot i i) p = ↑(nu i) • p) (hrowHighest : ∀ (i j : Fin m), i < j → (BideterminantHighestLine.sourceRowRoot i j) p = 0) (hcolumnHighest : ∀ (i j : Fin m), i < j → (BideterminantHighestLine.sourceColumnRoot i j) p = 0) : lam = nu

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankIsotropicSupportCartanWeight.sourceColumnDegree_eq_rowWeight_of_coeff_ne_zero_of_biHighest {m : ℕ} (lam : Fin m → ℕ) (p : BideterminantHighestLine.SourceMatrix m) (hrow : ∀ (i : Fin m), (BideterminantHighestLine.sourceRowRoot i i) p = ↑(lam i) • p) (hrowHighest : ∀ (i j : Fin m), i < j → (BideterminantHighestLine.sourceRowRoot i j) p = 0) (hcolumnHighest : ∀ (i j : Fin m), i < j → (BideterminantHighestLine.sourceColumnRoot i j) p = 0) (d : Fin m × Fin m →₀ ℕ) (hd : p.coeff d ≠ 0) : (fun (i : Fin m) => BideterminantHighestLine.sourceColumnDegree d i) = lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankIsotropicSupportCartanWeight.sourceColumnRoot_self_eq_rowWeight_of_biHighest {m : ℕ} (lam : Fin m → ℕ) (p : BideterminantHighestLine.SourceMatrix m) (hrow : ∀ (i : Fin m), (BideterminantHighestLine.sourceRowRoot i i) p = ↑(lam i) • p) (hrowHighest : ∀ (i j : Fin m), i < j → (BideterminantHighestLine.sourceRowRoot i j) p = 0) (hcolumnHighest : ∀ (i j : Fin m), i < j → (BideterminantHighestLine.sourceColumnRoot i j) p = 0) (i : Fin m) : (BideterminantHighestLine.sourceColumnRoot i i) p = ↑(lam i) • p

theorem MetricCodes.Spherical.HigherYoungFullComplexSpanRowEquations.rowDerivation_polynomialComplexification {r n : ℕ} (i j : Fin (r + 1)) (p : HigherHarmonicYoung.PolynomialSpace r n) : (HigherHarmonicYoung.DeterminantVectors.rowDerivation i j) (HigherYoungTwoRowLieIrreducibility.polynomialComplexification p) = HigherYoungTwoRowLieIrreducibility.polynomialComplexification ((HigherHarmonicYoung.polarization r n i j) p)

theorem MetricCodes.Spherical.HigherYoungFullComplexSpanRowEquations.rowDerivation_self_of_mem_fullYoungComplexPolynomialSpan {r n : ℕ} (lam : Fin (r + 1) → ℕ) {f : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hf : f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (i : Fin (r + 1)) : (HigherHarmonicYoung.DeterminantVectors.rowDerivation i i) f = ↑(lam i) • f

theorem MetricCodes.Spherical.HigherYoungFullComplexSpanRowEquations.rowDerivation_upper_of_mem_fullYoungComplexPolynomialSpan {r n : ℕ} (lam : Fin (r + 1) → ℕ) {f : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hf : f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (i j : Fin (r + 1)) (hij : i < j) : (HigherHarmonicYoung.DeterminantVectors.rowDerivation i j) f = 0

theorem MetricCodes.Spherical.HigherYoungFullComplexSpanTraceFree.complexTraceOperator_polynomialComplexification {r n : ℕ} (i j : Fin (r + 1)) (p : HigherHarmonicYoung.PolynomialSpace r n) : HigherHarmonicYoung.complexTraceOperator i j (HigherYoungTwoRowLieIrreducibility.polynomialComplexification p) = HigherYoungTwoRowLieIrreducibility.polynomialComplexification ((HigherHarmonicYoung.traceOperator r n i j) p)

theorem MetricCodes.Spherical.HigherYoungFullComplexSpanTraceFree.complexTraceOperator_of_mem_fullYoungComplexPolynomialSpan {r n : ℕ} (lam : Fin (r + 1) → ℕ) {f : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hf : f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (i j : Fin (r + 1)) : HigherHarmonicYoung.complexTraceOperator i j f = 0

theorem MetricCodes.Spherical.HigherYoungFullComplexSpanHomogeneity.isHomogeneous_of_mem_fullYoungComplexPolynomialSpan {r n : ℕ} (lam : Fin (r + 1) → ℕ) {f : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hf : f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) : f.IsHomogeneous (∑ i : Fin (r + 1), lam i)

theorem MetricCodes.Spherical.HigherYoungOrthogonalPositiveRootKernelIsotropicSupport.exists_nullSubstitution_of_mem_fullYoungComplexPolynomialSpan_maximalCartan {r n : ℕ} (h : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) {f : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hf : f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (hcartan : (HigherYoungAmbientCartanIsotropicEigenvalues.totalAmbientCartan h) f = ↑(2 * ∑ i : Fin (r + 1), lam i) • f) : ∃ (q : MvPolynomial (Fin (r + 1) × Fin (r + 1)) ℂ), (HigherHarmonicYoung.nullSubstitution h) q = f

theorem MetricCodes.Spherical.HigherYoungArbitraryRankHarmonicHoweHighestRigidity.sourceColumnRoot_upper_of_positiveRootKernel {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (p : HigherHarmonicYoung.BideterminantHighestLine.SourceMatrix (r + 1)) (hroots : ∀ (α : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n), (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation hn α) ((HigherHarmonicYoung.nullSubstitution hn) p) = 0) (i j : Fin (r + 1)) (hij : i < j) : (HigherHarmonicYoung.BideterminantHighestLine.sourceColumnRoot i j) p = 0

theorem MetricCodes.Spherical.HigherYoungArbitraryRankHarmonicHoweHighestRigidity.sourceRowRoot_self_of_mem_fullYoungComplexPolynomialSpan {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (p : HigherHarmonicYoung.BideterminantHighestLine.SourceMatrix (r + 1)) (hp : (HigherHarmonicYoung.nullSubstitution hn) p ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (i : Fin (r + 1)) : (HigherHarmonicYoung.BideterminantHighestLine.sourceRowRoot i i) p = ↑(lam i) • p

theorem MetricCodes.Spherical.HigherYoungArbitraryRankHarmonicHoweHighestRigidity.sourceRowRoot_upper_of_mem_fullYoungComplexPolynomialSpan {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (p : HigherHarmonicYoung.BideterminantHighestLine.SourceMatrix (r + 1)) (hp : (HigherHarmonicYoung.nullSubstitution hn) p ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (i j : Fin (r + 1)) (hij : i < j) : (HigherHarmonicYoung.BideterminantHighestLine.sourceRowRoot i j) p = 0

theorem MetricCodes.Spherical.HigherYoungArbitraryRankHarmonicHoweHighestRigidity.mem_ambientIsotropicHighestSubmodule_of_isotropic_positiveRootKernel {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) {f : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hf : f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (hsupport : ∃ (p : HigherHarmonicYoung.BideterminantHighestLine.SourceMatrix (r + 1)), (HigherHarmonicYoung.nullSubstitution hn) p = f) (hroots : ∀ (α : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n), (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation hn α) f = 0) (hsourceCartan : ∀ (p : HigherHarmonicYoung.BideterminantHighestLine.SourceMatrix (r + 1)), (∀ (i : Fin (r + 1)), (HigherHarmonicYoung.BideterminantHighestLine.sourceRowRoot i i) p = ↑(lam i) • p) → (∀ (i j : Fin (r + 1)), i < j → (HigherHarmonicYoung.BideterminantHighestLine.sourceRowRoot i j) p = 0) → (∀ (i j : Fin (r + 1)), i < j → (HigherHarmonicYoung.BideterminantHighestLine.sourceColumnRoot i j) p = 0) → ∀ (i : Fin (r + 1)), (HigherHarmonicYoung.BideterminantHighestLine.sourceColumnRoot i i) p = ↑(lam i) • p) : f ∈ HigherHarmonicYoung.IsotropicAmbientHighestLine.ambientIsotropicHighestSubmodule hn lam

theorem MetricCodes.Spherical.HigherYoungArbitraryRankHarmonicHoweHighestRigidity.mem_ambientIsotropicHighestSubmodule_of_positiveRootKernel_and_support {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) {f : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hf : f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (hsupport : ∃ (p : HigherHarmonicYoung.BideterminantHighestLine.SourceMatrix (r + 1)), (HigherHarmonicYoung.nullSubstitution hn) p = f) (hroots : ∀ (α : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n), (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation hn α) f = 0) : f ∈ HigherHarmonicYoung.IsotropicAmbientHighestLine.ambientIsotropicHighestSubmodule hn lam

theorem MetricCodes.Spherical.HigherYoungArbitraryRankHarmonicHoweHighestRigidity.mem_ambientIsotropicHighestSubmodule_of_positiveRootKernel_maximalCartan {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) {f : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hf : f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (hroots : ∀ (α : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n), (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation hn α) f = 0) (hcartan : (HigherYoungAmbientCartanIsotropicEigenvalues.totalAmbientCartan hn) f = ↑(2 * ∑ i : Fin (r + 1), lam i) • f) : f ∈ HigherHarmonicYoung.IsotropicAmbientHighestLine.ambientIsotropicHighestSubmodule hn lam

noncomputable def MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.totalYoungRowEuler {r n : ℕ} : Derivation ℂ (MvPolynomial (Fin ((r + 1) * n)) ℂ) (MvPolynomial (Fin ((r + 1) * n)) ℂ)

The total Euler derivation obtained by summing the diagonal derivations of all Young rows.

Equations

• MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.totalYoungRowEuler = ∑ a : Fin (r + 1), MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.rowDerivation a a

noncomputable def MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.antiholomorphicEulerDefect {r n : ℕ} (h : 2 * (r + 1) ≤ n) : Derivation ℂ (MvPolynomial (Fin ((r + 1) * n)) ℂ) (MvPolynomial (Fin ((r + 1) * n)) ℂ)

The Euler contribution from conjugate isotropic variables and their antiholomorphic derivatives.

Equations

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

noncomputable def MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.unusedCoordinateEulerDefect {r n : ℕ} : Derivation ℂ (MvPolynomial (Fin ((r + 1) * n)) ℂ) (MvPolynomial (Fin ((r + 1) * n)) ℂ)

The Euler contribution of ambient coordinates outside the chosen isotropic pairs.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.totalYoungRowEuler_apply {r n : ℕ} (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) : totalYoungRowEuler f = ∑ a : Fin (r + 1), (HigherHarmonicYoung.DeterminantVectors.rowDerivation a a) f

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.totalYoungRowEuler_of_rowCartan {r n : ℕ} (lam : Fin (r + 1) → ℕ) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hrow : ∀ (a : Fin (r + 1)), (HigherHarmonicYoung.DeterminantVectors.rowDerivation a a) f = ↑(lam a) • f) : totalYoungRowEuler f = ↑(∑ a : Fin (r + 1), lam a) • f

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.totalYoungRowEuler_X {r n : ℕ} (a : Fin (r + 1)) (t : Fin n) : totalYoungRowEuler (MvPolynomial.X (HigherHarmonicYoung.variableIndex a t)) = MvPolynomial.X (HigherHarmonicYoung.variableIndex a t)

@[simp]

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.antiholomorphicEulerDefect_apply {r n : ℕ} (h : 2 * (r + 1) ≤ n) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) : (antiholomorphicEulerDefect h) f = ∑ a : Fin (r + 1), ∑ p : Fin (r + 1), HigherHarmonicYoung.DeterminantVectors.conjugateIsotropicVariable h a p * (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) f

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.antiholomorphicDerivative_X_even {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a p b q : Fin (r + 1)) : (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) (MvPolynomial.X (HigherHarmonicYoung.variableIndex b (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h q))) = if a = b ∧ p = q then 1 else 0

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.antiholomorphicDerivative_X_odd {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a p b q : Fin (r + 1)) : (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) (MvPolynomial.X (HigherHarmonicYoung.variableIndex b (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h q))) = if a = b ∧ p = q then MvPolynomial.C Complex.I else 0

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.antiholomorphicDerivative_X_unused {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a p b : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) : (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) (MvPolynomial.X (HigherHarmonicYoung.variableIndex b t)) = 0

@[simp]

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.unusedCoordinateEulerDefect_apply {r n : ℕ} (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) : unusedCoordinateEulerDefect f = ∑ a : Fin (r + 1), ∑ t : Fin n with 2 * (r + 1) ≤ ↑t, MvPolynomial.X (HigherHarmonicYoung.variableIndex a t) * (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a t)) f

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.antiholomorphicEulerDefect_X_even {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a p : Fin (r + 1)) : (antiholomorphicEulerDefect h) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h p))) = HigherHarmonicYoung.DeterminantVectors.conjugateIsotropicVariable h a p

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.antiholomorphicEulerDefect_X_odd {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a p : Fin (r + 1)) : (antiholomorphicEulerDefect h) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h p))) = HigherHarmonicYoung.DeterminantVectors.conjugateIsotropicVariable h a p * MvPolynomial.C Complex.I

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.antiholomorphicEulerDefect_X_unused {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) : (antiholomorphicEulerDefect h) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a t)) = 0

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.unusedCoordinateEulerDefect_X {r n : ℕ} (a : Fin (r + 1)) (t : Fin n) : unusedCoordinateEulerDefect (MvPolynomial.X (HigherHarmonicYoung.variableIndex a t)) = if 2 * (r + 1) ≤ ↑t then MvPolynomial.X (HigherHarmonicYoung.variableIndex a t) else 0

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.totalAmbientCartan_X_even {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a p : Fin (r + 1)) : (HigherYoungAmbientCartanIsotropicEigenvalues.totalAmbientCartan h) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h p))) = HigherHarmonicYoung.DeterminantVectors.isotropicVariable h a p - HigherHarmonicYoung.DeterminantVectors.conjugateIsotropicVariable h a p

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.totalAmbientCartan_X_odd {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a p : Fin (r + 1)) : (HigherYoungAmbientCartanIsotropicEigenvalues.totalAmbientCartan h) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h p))) = -Complex.I • (HigherHarmonicYoung.DeterminantVectors.isotropicVariable h a p + HigherHarmonicYoung.DeterminantVectors.conjugateIsotropicVariable h a p)

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.antiholomorphicEulerDefect_eq_zero {r n : ℕ} (h : 2 * (r + 1) ≤ n) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hanti : ∀ (a p : Fin (r + 1)), (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) f = 0) : (antiholomorphicEulerDefect h) f = 0

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.unusedCoordinateEulerDefect_eq_zero {r n : ℕ} (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hunused : ∀ (a : Fin (r + 1)) (t : Fin n), 2 * (r + 1) ≤ ↑t → (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a t)) f = 0) : unusedCoordinateEulerDefect f = 0

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.totalYoungRowEuler_sub_totalAmbientCartan_eq_defects {r n : ℕ} (h : 2 * (r + 1) ≤ n) : 2 • totalYoungRowEuler - HigherYoungAmbientCartanIsotropicEigenvalues.totalAmbientCartan h = 2 • antiholomorphicEulerDefect h + 2 • unusedCoordinateEulerDefect

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.totalAmbientCartan_eq_maximal_of_rowCartan_antiholomorphic_unused {r n : ℕ} (h : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hrow : ∀ (a : Fin (r + 1)), (HigherHarmonicYoung.DeterminantVectors.rowDerivation a a) f = ↑(lam a) • f) (hanti : ∀ (a p : Fin (r + 1)), (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) f = 0) (hunused : ∀ (a : Fin (r + 1)) (t : Fin n), 2 * (r + 1) ≤ ↑t → (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a t)) f = 0) : (HigherYoungAmbientCartanIsotropicEigenvalues.totalAmbientCartan h) f = ↑(2 * ∑ a : Fin (r + 1), lam a) • f

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestUnusedDerivativeVanishing.isotropicMatrix_det_ne_zero {r n : ℕ} (h : 2 * (r + 1) ≤ n) : (Matrix.of fun (a p : Fin (r + 1)) => HigherHarmonicYoung.DeterminantVectors.isotropicVariable h a p).det ≠ 0

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestUnusedDerivativeVanishing.isotropicMatrix_transpose_mulVec_injective {r n : ℕ} (h : 2 * (r + 1) ≤ n) (v : Fin (r + 1) → MvPolynomial (Fin ((r + 1) * n)) ℂ) (hv : (Matrix.of fun (a p : Fin (r + 1)) => HigherHarmonicYoung.DeterminantVectors.isotropicVariable h a p).transpose.mulVec v = 0) : v = 0

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestUnusedDerivativeVanishing.isotropicMatrix_unusedDerivative_eq_zero_of_shortRoot {r n : ℕ} (h : 2 * (r + 1) ≤ n) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hantiholomorphic : ∀ (a p : Fin (r + 1)), (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) f = 0) (t : Fin n) (hshort : ∀ (p : Fin (r + 1)), (HigherHarmonicYoung.DeterminantVectors.ambientShortPositiveRoot h p t) f = 0) (p : Fin (r + 1)) : ∑ a : Fin (r + 1), HigherHarmonicYoung.DeterminantVectors.isotropicVariable h a p * (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a t)) f = 0

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestUnusedDerivativeVanishing.unused_pderiv_eq_zero_of_antiholomorphic_and_shortRoot {r n : ℕ} (h : 2 * (r + 1) ≤ n) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hantiholomorphic : ∀ (a p : Fin (r + 1)), (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) f = 0) (hshort : ∀ (p : Fin (r + 1)) (t : Fin n), 2 * (r + 1) ≤ ↑t → (HigherHarmonicYoung.DeterminantVectors.ambientShortPositiveRoot h p t) f = 0) (a : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) : (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a t)) f = 0

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestUnusedDerivativeVanishing.unused_pderiv_eq_zero_of_antiholomorphic_and_positiveRootKernel {r n : ℕ} (h : 2 * (r + 1) ≤ n) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hantiholomorphic : ∀ (a p : Fin (r + 1)), (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) f = 0) (hroot : ∀ (α : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n), (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation h α) f = 0) (a : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) : (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a t)) f = 0

def MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootEnergyIdentity.unusedAmbientCoordinates {r n : ℕ} : Finset (Fin n)

The ambient coordinates beyond the r + 1 selected even-odd pairs.

Equations

• MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootEnergyIdentity.unusedAmbientCoordinates = {t : Fin n | 2 * (r + 1) ≤ ↑t}

@[simp]

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootEnergyIdentity.mem_unusedAmbientCoordinates {r n : ℕ} (t : Fin n) : t ∈ unusedAmbientCoordinates ↔ 2 * (r + 1) ≤ ↑t

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootEnergyIdentity.shortRoot_unusedDerivative {r n : ℕ} (h : 2 * (r + 1) ≤ n) (b p : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) : (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex b t)) ((HigherHarmonicYoung.DeterminantVectors.ambientShortPositiveRoot h p t) f) = ∑ a : Fin (r + 1), (HigherHarmonicYoung.DeterminantVectors.isotropicVariable h a p * (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex b t)) ((MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a t)) f) - MvPolynomial.X (HigherHarmonicYoung.variableIndex a t) * (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex b t)) ((HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) f)) - (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b p) f

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootEnergyIdentity.shortRoot_unusedDerivative_sum {r n : ℕ} (h : 2 * (r + 1) ≤ n) (b p : Fin (r + 1)) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) : ∑ t ∈ unusedAmbientCoordinates, (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex b t)) ((HigherHarmonicYoung.DeterminantVectors.ambientShortPositiveRoot h p t) f) = ∑ t ∈ unusedAmbientCoordinates, ∑ a : Fin (r + 1), (HigherHarmonicYoung.DeterminantVectors.isotropicVariable h a p * (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex b t)) ((MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a t)) f) - MvPolynomial.X (HigherHarmonicYoung.variableIndex a t) * (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex b t)) ((HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) f)) - unusedAmbientCoordinates.card • (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b p) f

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootEnergyIdentity.shortRoot_unusedDerivative_sum_eq_card_smul_of_rootKernel {r n : ℕ} (h : 2 * (r + 1) ≤ n) (b p : Fin (r + 1)) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hroot : ∀ (t : Fin n), 2 * (r + 1) ≤ ↑t → (HigherHarmonicYoung.DeterminantVectors.ambientShortPositiveRoot h p t) f = 0) : ∑ t ∈ unusedAmbientCoordinates, ∑ a : Fin (r + 1), (HigherHarmonicYoung.DeterminantVectors.isotropicVariable h a p * (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex b t)) ((MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a t)) f) - MvPolynomial.X (HigherHarmonicYoung.variableIndex a t) * (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex b t)) ((HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) f)) = unusedAmbientCoordinates.card • (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b p) f

noncomputable def MetricCodes.Spherical.HigherYoungIsotropicComplexTraceDecomposition.holomorphicDerivative {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a p : Fin (r + 1)) : Derivation ℂ (MvPolynomial (Fin ((r + 1) * n)) ℂ) (MvPolynomial (Fin ((r + 1) * n)) ℂ)

The even-coordinate partial derivative minus i times the paired odd-coordinate derivative.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherYoungIsotropicComplexTraceDecomposition.holomorphicDerivative_apply {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a p : Fin (r + 1)) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) : (holomorphicDerivative h a p) f = (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h p))) f - MvPolynomial.C Complex.I * (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h p))) f

@[simp]

theorem MetricCodes.Spherical.HigherYoungIsotropicComplexTraceDecomposition.antiholomorphicDerivative_apply {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a p : Fin (r + 1)) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) : (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) f = (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h p))) f + MvPolynomial.C Complex.I * (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h p))) f

theorem MetricCodes.Spherical.HigherYoungIsotropicComplexTraceDecomposition.occupiedEven_disjoint_occupiedOdd {r n : ℕ} (h : 2 * (r + 1) ≤ n) : Disjoint (Finset.image (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h) Finset.univ) (Finset.image (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h) Finset.univ)

theorem MetricCodes.Spherical.HigherYoungIsotropicComplexTraceDecomposition.occupiedCoordinates_eq_even_union_odd {r n : ℕ} (h : 2 * (r + 1) ≤ n) : {t : Fin n | ↑t < 2 * (r + 1)} = Finset.image (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h) Finset.univ ∪ Finset.image (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h) Finset.univ

theorem MetricCodes.Spherical.HigherYoungIsotropicComplexTraceDecomposition.sum_occupied_eq_even_odd {r n : ℕ} {A : Type u_1} [AddCommMonoid A] (h : 2 * (r + 1) ≤ n) (g : Fin n → A) : ∑ t : Fin n with ↑t < 2 * (r + 1), g t = ∑ p : Fin (r + 1), (g (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h p) + g (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h p))

theorem MetricCodes.Spherical.HigherYoungIsotropicComplexTraceDecomposition.sum_univ_eq_even_odd_add_unused {r n : ℕ} {A : Type u_1} [AddCommMonoid A] (h : 2 * (r + 1) ≤ n) (g : Fin n → A) : ∑ t : Fin n, g t = ∑ p : Fin (r + 1), (g (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h p) + g (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h p)) + ∑ t ∈ HigherYoungAllRankHarmonicHighestRootEnergyIdentity.unusedAmbientCoordinates, g t

theorem MetricCodes.Spherical.HigherYoungIsotropicComplexTraceDecomposition.occupiedMixedTrace_eq_holomorphic_antiholomorphic {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a b p : Fin (r + 1)) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) : (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h p))) ((MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex b (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h p))) f) + (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h p))) ((MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex b (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h p))) f) = 2⁻¹ • ((holomorphicDerivative h a p) ((HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b p) f) + (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) ((holomorphicDerivative h b p) f))

theorem MetricCodes.Spherical.HigherYoungIsotropicComplexTraceDecomposition.complexTraceOperator_eq_isotropicDerivative_add_unused {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a b : Fin (r + 1)) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) : HigherHarmonicYoung.complexTraceOperator a b f = 2⁻¹ • ∑ p : Fin (r + 1), ((holomorphicDerivative h a p) ((HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b p) f) + (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) ((holomorphicDerivative h b p) f)) + ∑ t ∈ HigherYoungAllRankHarmonicHighestRootEnergyIdentity.unusedAmbientCoordinates, (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a t)) ((MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex b t)) f)

theorem MetricCodes.Spherical.HigherYoungIsotropicComplexTraceDecomposition.unusedMixedHessian_eq_neg_isotropicDerivative_of_traceFree {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a b : Fin (r + 1)) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (htrace : HigherHarmonicYoung.complexTraceOperator a b f = 0) : ∑ t ∈ HigherYoungAllRankHarmonicHighestRootEnergyIdentity.unusedAmbientCoordinates, (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a t)) ((MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex b t)) f) = -(2⁻¹ • ∑ p : Fin (r + 1), ((holomorphicDerivative h a p) ((HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b p) f) + (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) ((holomorphicDerivative h b p) f)))

theorem MetricCodes.Spherical.HigherYoungIsotropicComplexTraceDecomposition.unusedMixedHessian_of_mem_fullYoungComplexPolynomialSpan {r n : ℕ} (h : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) {f : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hf : f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (a b : Fin (r + 1)) : ∑ t ∈ HigherYoungAllRankHarmonicHighestRootEnergyIdentity.unusedAmbientCoordinates, (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a t)) ((MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex b t)) f) = -(2⁻¹ • ∑ p : Fin (r + 1), ((holomorphicDerivative h a p) ((HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b p) f) + (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) ((holomorphicDerivative h b p) f)))

theorem MetricCodes.Spherical.HigherYoungAllRankAntiHolomorphicRootCommutators.complex_pderiv_commute {N : ℕ} (i j : Fin N) (f : MvPolynomial (Fin N) ℂ) : (MvPolynomial.pderiv i) ((MvPolynomial.pderiv j) f) = (MvPolynomial.pderiv j) ((MvPolynomial.pderiv i) f)

theorem MetricCodes.Spherical.HigherYoungAllRankAntiHolomorphicRootCommutators.pderiv_rowDerivation {r n : ℕ} (a i j : Fin (r + 1)) (k : Fin n) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) : (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a k)) ((HigherHarmonicYoung.DeterminantVectors.rowDerivation i j) f) = (if a = i then (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex j k)) f else 0) + (HigherHarmonicYoung.DeterminantVectors.rowDerivation i j) ((MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a k)) f)

theorem MetricCodes.Spherical.HigherYoungAllRankAntiHolomorphicRootCommutators.rowDerivation_antiholomorphicDerivative_commutator {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a b c p : Fin (r + 1)) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) : (HigherHarmonicYoung.DeterminantVectors.rowDerivation a b) ((HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h c p) f) - (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h c p) ((HigherHarmonicYoung.DeterminantVectors.rowDerivation a b) f) = if a = c then -(HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b p) f else 0

theorem MetricCodes.Spherical.HigherYoungAllRankAntiHolomorphicRootCommutators.rowDerivation_antiholomorphicDerivative_matching {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a b p : Fin (r + 1)) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) : (HigherHarmonicYoung.DeterminantVectors.rowDerivation a b) ((HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) f) - (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) ((HigherHarmonicYoung.DeterminantVectors.rowDerivation a b) f) = -(HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b p) f

theorem MetricCodes.Spherical.HigherYoungAllRankShortRootAntiHolomorphicMixedTraceCancellation.occupiedRowEuler_eq_isotropicDerivatives {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a b q : Fin (r + 1)) (g : MvPolynomial (Fin ((r + 1) * n)) ℂ) : MvPolynomial.X (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h q)) * (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex b (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h q))) g + MvPolynomial.X (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h q)) * (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex b (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h q))) g = 2⁻¹ • (HigherHarmonicYoung.DeterminantVectors.isotropicVariable h a q * (HigherYoungIsotropicComplexTraceDecomposition.holomorphicDerivative h b q) g + HigherHarmonicYoung.DeterminantVectors.conjugateIsotropicVariable h a q * (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b q) g)

theorem MetricCodes.Spherical.HigherYoungAllRankShortRootAntiHolomorphicMixedTraceCancellation.rowDerivation_eq_isotropicDerivatives_add_unused {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a b : Fin (r + 1)) (g : MvPolynomial (Fin ((r + 1) * n)) ℂ) : (HigherHarmonicYoung.DeterminantVectors.rowDerivation a b) g = 2⁻¹ • ∑ q : Fin (r + 1), (HigherHarmonicYoung.DeterminantVectors.isotropicVariable h a q * (HigherYoungIsotropicComplexTraceDecomposition.holomorphicDerivative h b q) g + HigherHarmonicYoung.DeterminantVectors.conjugateIsotropicVariable h a q * (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b q) g) + ∑ t ∈ HigherYoungAllRankHarmonicHighestRootEnergyIdentity.unusedAmbientCoordinates, MvPolynomial.X (HigherHarmonicYoung.variableIndex a t) * (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex b t)) g

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicRootEnergyTraceRowCancellation.shortRoot_mixedRemainder_eq_neg_rowDerivation_add_isotropic_traces {r n : ℕ} (h : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) {f : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hf : f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (b p : Fin (r + 1)) : ∑ t ∈ HigherYoungAllRankHarmonicHighestRootEnergyIdentity.unusedAmbientCoordinates, ∑ a : Fin (r + 1), (HigherHarmonicYoung.DeterminantVectors.isotropicVariable h a p * (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex b t)) ((MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a t)) f) - MvPolynomial.X (HigherHarmonicYoung.variableIndex a t) * (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex b t)) ((HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) f)) = -∑ a : Fin (r + 1), (HigherHarmonicYoung.DeterminantVectors.rowDerivation a b) ((HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) f) + 2⁻¹ • ∑ q : Fin (r + 1), ∑ a : Fin (r + 1), (HigherHarmonicYoung.DeterminantVectors.isotropicVariable h a q * (HigherYoungIsotropicComplexTraceDecomposition.holomorphicDerivative h b q) ((HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) f) + HigherHarmonicYoung.DeterminantVectors.conjugateIsotropicVariable h a q * (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b q) ((HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) f) - HigherHarmonicYoung.DeterminantVectors.isotropicVariable h a p * (HigherYoungIsotropicComplexTraceDecomposition.holomorphicDerivative h b q) ((HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a q) f) - HigherHarmonicYoung.DeterminantVectors.isotropicVariable h a p * (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b q) ((HigherYoungIsotropicComplexTraceDecomposition.holomorphicDerivative h a q) f))

theorem MetricCodes.Spherical.HigherYoungAmbientDifferenceRootAntiHolomorphicDerivativeCommutator.antiholomorphicDerivative_antiholomorphicDerivative_commute {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a p b q : Fin (r + 1)) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) : (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) ((HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b q) f) = (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b q) ((HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) f)

theorem MetricCodes.Spherical.HigherYoungAmbientDifferenceRootAntiHolomorphicDerivativeCommutator.ambientPositiveRoot_antiholomorphicDerivative_commutator_apply {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p q b s : Fin (r + 1)) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) : (HigherHarmonicYoung.DeterminantVectors.ambientPositiveRoot h p q) ((HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b s) f) - (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b s) ((HigherHarmonicYoung.DeterminantVectors.ambientPositiveRoot h p q) f) = if s = q then 2 • (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b p) f else 0

theorem MetricCodes.Spherical.HigherYoungAmbientDifferenceRootAntiHolomorphicDerivativeCommutator.ambientPositiveRoot_antiholomorphicDerivative_of_rootKernel {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p q b : Fin (r + 1)) (_hpq : p ≠ q) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hf : (HigherHarmonicYoung.DeterminantVectors.ambientPositiveRoot h p q) f = 0) : (HigherHarmonicYoung.DeterminantVectors.ambientPositiveRoot h p q) ((HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b q) f) = 2 • (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b p) f

theorem MetricCodes.Spherical.HigherYoungAmbientSumRootHolomorphicDerivativeCommutator.holomorphicDerivative_isotropicVariable {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a p i j : Fin (r + 1)) : (HigherYoungIsotropicComplexTraceDecomposition.holomorphicDerivative h a p) (HigherHarmonicYoung.DeterminantVectors.isotropicVariable h i j) = if a = i ∧ p = j then 2 else 0

theorem MetricCodes.Spherical.HigherYoungAmbientSumRootHolomorphicDerivativeCommutator.complexPolynomial_pderiv_commute {ι : Type u_1} (i j : ι) (f : MvPolynomial ι ℂ) : (MvPolynomial.pderiv i) ((MvPolynomial.pderiv j) f) = (MvPolynomial.pderiv j) ((MvPolynomial.pderiv i) f)

theorem MetricCodes.Spherical.HigherYoungAmbientSumRootHolomorphicDerivativeCommutator.antiholomorphicDerivative_holomorphicDerivative_commute {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a p b q : Fin (r + 1)) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) : (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) ((HigherYoungIsotropicComplexTraceDecomposition.holomorphicDerivative h b q) f) = (HigherYoungIsotropicComplexTraceDecomposition.holomorphicDerivative h b q) ((HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) f)

@[simp]

theorem MetricCodes.Spherical.HigherYoungAmbientSumRootHolomorphicDerivativeCommutator.ambientSumPositiveRoot_self {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p : Fin (r + 1)) : HigherHarmonicYoung.DeterminantVectors.ambientSumPositiveRoot h p p = 0

theorem MetricCodes.Spherical.HigherYoungAmbientSumRootHolomorphicDerivativeCommutator.ambientSumPositiveRoot_apply_antiholomorphic {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p q : Fin (r + 1)) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) : (HigherHarmonicYoung.DeterminantVectors.ambientSumPositiveRoot h p q) f = ∑ a : Fin (r + 1), (HigherHarmonicYoung.DeterminantVectors.isotropicVariable h a p * (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a q) f - HigherHarmonicYoung.DeterminantVectors.isotropicVariable h a q * (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) f)

theorem MetricCodes.Spherical.HigherYoungAmbientSumRootHolomorphicDerivativeCommutator.ambientSumPositiveRoot_holomorphicDerivative_commutator_apply {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p q b s : Fin (r + 1)) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) : (HigherHarmonicYoung.DeterminantVectors.ambientSumPositiveRoot h p q) ((HigherYoungIsotropicComplexTraceDecomposition.holomorphicDerivative h b s) f) - (HigherYoungIsotropicComplexTraceDecomposition.holomorphicDerivative h b s) ((HigherHarmonicYoung.DeterminantVectors.ambientSumPositiveRoot h p q) f) = (if s = q then 2 • (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b p) f else 0) - if s = p then 2 • (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b q) f else 0

theorem MetricCodes.Spherical.HigherYoungAmbientSumRootHolomorphicDerivativeCommutator.ambientSumPositiveRoot_holomorphicDerivative_commutator {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p q b : Fin (r + 1)) (hpq : p ≠ q) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) : (HigherHarmonicYoung.DeterminantVectors.ambientSumPositiveRoot h p q) ((HigherYoungIsotropicComplexTraceDecomposition.holomorphicDerivative h b q) f) - (HigherYoungIsotropicComplexTraceDecomposition.holomorphicDerivative h b q) ((HigherHarmonicYoung.DeterminantVectors.ambientSumPositiveRoot h p q) f) = 2 • (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b p) f

theorem MetricCodes.Spherical.HigherYoungAmbientSumRootHolomorphicDerivativeCommutator.ambientSumPositiveRoot_holomorphicDerivative_of_rootKernel {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p q b : Fin (r + 1)) (hpq : p ≠ q) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hf : (HigherHarmonicYoung.DeterminantVectors.ambientSumPositiveRoot h p q) f = 0) : (HigherHarmonicYoung.DeterminantVectors.ambientSumPositiveRoot h p q) ((HigherYoungIsotropicComplexTraceDecomposition.holomorphicDerivative h b q) f) = 2 • (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b p) f

theorem MetricCodes.Spherical.HigherYoungAmbientSumRootAllHighestHolomorphicEvaluation.ambientSumPositiveRoot_swap {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p q : Fin (r + 1)) : HigherHarmonicYoung.DeterminantVectors.ambientSumPositiveRoot h p q = -HigherHarmonicYoung.DeterminantVectors.ambientSumPositiveRoot h q p

theorem MetricCodes.Spherical.HigherYoungAmbientSumRootAllHighestHolomorphicEvaluation.ambientSumPositiveRoot_eq_zero_of_all_positive_root_highest {r n : ℕ} (h : 2 * (r + 1) ≤ n) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hroots : ∀ (α : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n), (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation h α) f = 0) (p q : Fin (r + 1)) : (HigherHarmonicYoung.DeterminantVectors.ambientSumPositiveRoot h p q) f = 0

theorem MetricCodes.Spherical.HigherYoungAmbientSumRootAllHighestHolomorphicEvaluation.ambientSumPositiveRoot_holomorphicDerivative_of_all_positive_root_highest {r n : ℕ} (h : 2 * (r + 1) ≤ n) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hroots : ∀ (α : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n), (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation h α) f = 0) (p q b : Fin (r + 1)) : (HigherHarmonicYoung.DeterminantVectors.ambientSumPositiveRoot h p q) ((HigherYoungIsotropicComplexTraceDecomposition.holomorphicDerivative h b q) f) = if p = q then 0 else 2 • (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b p) f

theorem MetricCodes.Spherical.HigherYoungAmbientSumRootAllHighestHolomorphicEvaluation.sum_ambientSumPositiveRoot_holomorphicDerivative_of_all_positive_root_highest {r n : ℕ} (h : 2 * (r + 1) ≤ n) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hroots : ∀ (α : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n), (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation h α) f = 0) (p b : Fin (r + 1)) : ∑ q : Fin (r + 1), (HigherHarmonicYoung.DeterminantVectors.ambientSumPositiveRoot h p q) ((HigherYoungIsotropicComplexTraceDecomposition.holomorphicDerivative h b q) f) = ↑(2 * r) • (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b p) f

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootCoercivity.card_unusedAmbientCoordinates {r n : ℕ} (h : 2 * (r + 1) ≤ n) : HigherYoungAllRankHarmonicHighestRootEnergyIdentity.unusedAmbientCoordinates.card = n - 2 * (r + 1)

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootCoercivity.two_le_card_unusedAmbientCoordinates {r n : ℕ} (h : 2 * (r + 1) ≤ n) (hstable : 2 * (r + 1) + 2 ≤ n) : 2 ≤ HigherYoungAllRankHarmonicHighestRootEnergyIdentity.unusedAmbientCoordinates.card

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootCoercivity.triangularResidual_eq_rowTail_add_columnTail {r : ℕ} (b p : Fin (r + 1)) : 2 * (r + 1) - 2 - ↑b - ↑p = r - ↑b + (r - ↑p)

def MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootCoercivity.harmonicHighestTriangularCoefficient {r : ℕ} (n : ℕ) (lam mu : Fin (r + 1) → ℕ) (b p : Fin (r + 1)) : ℕ

The triangular coercivity coefficient combining unused coordinates, row weights, and root indices.

Equations

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

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootCoercivity.harmonicHighestTriangularCoefficient_eq_tails {r n : ℕ} (lam mu : Fin (r + 1) → ℕ) (b p : Fin (r + 1)) : harmonicHighestTriangularCoefficient n lam mu b p = HigherYoungAllRankHarmonicHighestRootEnergyIdentity.unusedAmbientCoordinates.card + lam b + mu p + (r - ↑b) + (r - ↑p)

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootCoercivity.two_le_harmonicHighestTriangularCoefficient {r n : ℕ} (h : 2 * (r + 1) ≤ n) (hstable : 2 * (r + 1) + 2 ≤ n) (lam mu : Fin (r + 1) → ℕ) (b p : Fin (r + 1)) : 2 ≤ harmonicHighestTriangularCoefficient n lam mu b p

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootCoercivity.harmonicHighestTriangularCoefficient_ne_zero {r n : ℕ} (h : 2 * (r + 1) ≤ n) (hstable : 2 * (r + 1) + 2 ≤ n) (lam mu : Fin (r + 1) → ℕ) (b p : Fin (r + 1)) : harmonicHighestTriangularCoefficient n lam mu b p ≠ 0

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootCoercivity.harmonicHighestTriangularCoefficient_complex_ne_zero {r n : ℕ} (h : 2 * (r + 1) ≤ n) (hstable : 2 * (r + 1) + 2 ≤ n) (lam mu : Fin (r + 1) → ℕ) (b p : Fin (r + 1)) : ↑(harmonicHighestTriangularCoefficient n lam mu b p) ≠ 0

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestTriangularScalarBookkeeping.sum_ite_lt_scalar {r : ℕ} (b : Fin (r + 1)) (c : ℂ) : (∑ a : Fin (r + 1), if a < b then c else 0) = ↑↑b * c

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestTriangularScalarBookkeeping.sum_ite_gt_scalar {r : ℕ} (p : Fin (r + 1)) (c : ℂ) : (∑ q : Fin (r + 1), if p < q then c else 0) = ↑(r - ↑p) * c

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestTriangularScalarBookkeeping.sum_rowHighest_scalar {r : ℕ} (lam : Fin (r + 1) → ℕ) (b : Fin (r + 1)) : (∑ a : Fin (r + 1), if a < b then -1 else if a = b then ↑(lam b) - 1 else 0) = ↑(lam b) - 1 - ↑↑b

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestTriangularScalarBookkeeping.sum_differenceHighest_scalar {r : ℕ} (mu : Fin (r + 1) → ℕ) (p : Fin (r + 1)) : (∑ q : Fin (r + 1), if q < p then 0 else if q = p then ↑(2 * mu p) + 2 else 2) = ↑(2 * mu p) + 2 + 2 * ↑(r - ↑p)

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestTriangularScalarBookkeeping.harmonicHighestTriangularCoefficient_complex_eq {r n : ℕ} (lam mu : Fin (r + 1) → ℕ) (b p : Fin (r + 1)) : ↑(HigherYoungAllRankHarmonicHighestRootCoercivity.harmonicHighestTriangularCoefficient n lam mu b p) = ↑HigherYoungAllRankHarmonicHighestRootEnergyIdentity.unusedAmbientCoordinates.card + (↑(lam b) - 1 - ↑↑b) + 2⁻¹ * (↑(2 * mu p) + 2 + 2 * ↑(r - ↑p) + 2 * ↑r)

theorem MetricCodes.Spherical.HigherYoungAllRankAntiHolomorphicTriangularSums.rowDerivation_antiholomorphic_sum_of_later_rows {r n : ℕ} (h : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) {f : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hf : f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (b p : Fin (r + 1)) (hrowLater : ∀ (a : Fin (r + 1)), b < a → (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) f = 0) : ∑ a : Fin (r + 1), (HigherHarmonicYoung.DeterminantVectors.rowDerivation a b) ((HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) f) = (↑(lam b) - 1 - ↑↑b) • (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b p) f

theorem MetricCodes.Spherical.HigherYoungAllRankActualHighestCasimirRigidity.ambientPositiveRoot_antiholomorphic_sum_of_earlier_columns {r n : ℕ} (h : 2 * (r + 1) ≤ n) (mu : Fin (r + 1) → ℕ) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hroots : ∀ (α : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n), (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation h α) f = 0) (hcartan : ∀ (p : Fin (r + 1)), (HigherHarmonicYoung.DeterminantVectors.ambientCartan h p) f = ↑(2 * mu p) • f) (b p : Fin (r + 1)) (hcolEarlier : ∀ q < p, (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b q) f = 0) : ∑ q : Fin (r + 1), (HigherHarmonicYoung.DeterminantVectors.ambientPositiveRoot h p q) ((HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b q) f) = (↑(2 * mu p) + 2 + 2 * ↑(r - ↑p)) • (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b p) f

theorem MetricCodes.Spherical.HigherYoungFiniteDescendingAscendingInduction.fin_descending_ascending_induction {m : ℕ} {P : Fin m → Fin m → Prop} (hstep : ∀ (b p : Fin m), (∀ (a : Fin m), b < a → ∀ (q : Fin m), P a q) → (∀ q < p, P b q) → P b p) (b p : Fin m) : P b p

theorem MetricCodes.Spherical.HigherYoungAllRankActualHighestAntiHolomorphicRecurrence.harmonicHighestRoot_antiholomorphic_operator_recurrence {r n : ℕ} (h : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) {f : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hf : f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (hroots : ∀ (α : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n), (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation h α) f = 0) (b p : Fin (r + 1)) : ↑(HigherYoungAllRankHarmonicHighestRootEnergyIdentity.unusedAmbientCoordinates.card + r) • (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b p) f + ∑ a : Fin (r + 1), (HigherHarmonicYoung.DeterminantVectors.rowDerivation a b) ((HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) f) + 2⁻¹ • ∑ q : Fin (r + 1), (HigherHarmonicYoung.DeterminantVectors.ambientPositiveRoot h p q) ((HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b q) f) = 0

theorem MetricCodes.Spherical.HigherYoungAllRankActualHighestAntiHolomorphicRecurrence.antiholomorphicDerivative_eq_zero_of_positiveRootKernel_nonnegativeCartan {r n : ℕ} (h : 2 * (r + 1) ≤ n) (hstable : 2 * (r + 1) + 2 ≤ n) (lam mu : Fin (r + 1) → ℕ) {f : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hf : f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (hroots : ∀ (α : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n), (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation h α) f = 0) (hcartan : ∀ (p : Fin (r + 1)), (HigherHarmonicYoung.DeterminantVectors.ambientCartan h p) f = ↑(2 * mu p) • f) (b p : Fin (r + 1)) : (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b p) f = 0

noncomputable def MetricCodes.Spherical.HigherYoungAllRankShortNegativeRootNilpotence.ambientShortNegativeRoot {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p : Fin (r + 1)) (t : Fin n) : Derivation ℂ (MvPolynomial (Fin ((r + 1) * n)) ℂ) (MvPolynomial (Fin ((r + 1) * n)) ℂ)

The negative short-root derivation formed from the two rotations of an isotropic coordinate pair.

Equations

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

noncomputable def MetricCodes.Spherical.HigherYoungAllRankHighestShortRootWeightNonnegative.complexDerivationCommutator {r n : ℕ} (D₁ D₂ : Derivation ℂ (MvPolynomial (Fin ((r + 1) * n)) ℂ) (MvPolynomial (Fin ((r + 1) * n)) ℂ)) : Derivation ℂ (MvPolynomial (Fin ((r + 1) * n)) ℂ) (MvPolynomial (Fin ((r + 1) * n)) ℂ)

The commutator of two complex polynomial derivations, given by the difference of their compositions.

Equations

• MetricCodes.Spherical.HigherYoungAllRankHighestShortRootWeightNonnegative.complexDerivationCommutator D₁ D₂ = Derivation.mk' (↑D₁ ∘ₗ ↑D₂ - ↑D₂ ∘ₗ ↑D₁) ⋯

@[instance_reducible]

noncomputable instance MetricCodes.Spherical.HigherYoungAllRankHighestShortRootWeightNonnegative.complexDerivationBracket {r n : ℕ} : Bracket (Derivation ℂ (MvPolynomial (Fin ((r + 1) * n)) ℂ) (MvPolynomial (Fin ((r + 1) * n)) ℂ)) (Derivation ℂ (MvPolynomial (Fin ((r + 1) * n)) ℂ) (MvPolynomial (Fin ((r + 1) * n)) ℂ))

Equations

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

theorem MetricCodes.Spherical.HigherYoungAllRankHighestShortRootWeightNonnegative.complexAmbientCoordinateDerivation_X {r n : ℕ} (a b : Fin n) (i : Fin (r + 1)) (k : Fin n) : (HigherYoungTwoRowLieIrreducibility.complexAmbientCoordinateDerivation a b) (MvPolynomial.X (HigherHarmonicYoung.variableIndex i k)) = if b = k then MvPolynomial.X (HigherHarmonicYoung.variableIndex i a) else 0

@[simp]

theorem MetricCodes.Spherical.HigherYoungAllRankHighestShortRootWeightNonnegative.complexAmbientRotation_X {r n : ℕ} (a b : Fin n) (i : Fin (r + 1)) (k : Fin n) : (HigherYoungTwoRowLieIrreducibility.complexAmbientRotation a b) (MvPolynomial.X (HigherHarmonicYoung.variableIndex i k)) = (if b = k then MvPolynomial.X (HigherHarmonicYoung.variableIndex i a) else 0) - if a = k then MvPolynomial.X (HigherHarmonicYoung.variableIndex i b) else 0

theorem MetricCodes.Spherical.HigherYoungAllRankHighestShortRootWeightNonnegative.complexAmbientRotation_commutator_same_right {r n : ℕ} (a b t : Fin n) (hab : a ≠ b) (hat : a ≠ t) (hbt : b ≠ t) : ⁅HigherYoungTwoRowLieIrreducibility.complexAmbientRotation a t, HigherYoungTwoRowLieIrreducibility.complexAmbientRotation b t⁆ = HigherYoungTwoRowLieIrreducibility.complexAmbientRotation b a

theorem MetricCodes.Spherical.HigherYoungAllRankHighestShortRootWeightNonnegative.ambientShortPositiveRoot_negative_commutator {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (p : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) : ⁅HigherHarmonicYoung.DeterminantVectors.ambientShortPositiveRoot hn p t, HigherYoungAllRankShortNegativeRootNilpotence.ambientShortNegativeRoot hn p t⁆ = HigherHarmonicYoung.DeterminantVectors.ambientCartan hn p

theorem MetricCodes.Spherical.HigherYoungAllRankHighestShortRootWeightNonnegative.ambientShortPositiveRoot_youngComplexPair {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (p : Fin (r + 1)) (t : Fin n) (u v : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) : (HigherHarmonicYoung.DeterminantVectors.ambientShortPositiveRoot hn p t) (HigherYoungArbitraryRankDominantHighestLinePreservation.youngComplexPair lam u v) = HigherYoungArbitraryRankDominantHighestLinePreservation.youngComplexPair lam ((HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam (HigherHarmonicYoung.DeterminantVectors.evenCoordinate hn p) t) u - (HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam (HigherHarmonicYoung.DeterminantVectors.oddCoordinate hn p) t) v) ((HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam (HigherHarmonicYoung.DeterminantVectors.evenCoordinate hn p) t) v + (HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam (HigherHarmonicYoung.DeterminantVectors.oddCoordinate hn p) t) u)

theorem MetricCodes.Spherical.HigherYoungAllRankHighestShortRootWeightNonnegative.ambientShortNegativeRoot_youngComplexPair {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (p : Fin (r + 1)) (t : Fin n) (u v : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) : (HigherYoungAllRankShortNegativeRootNilpotence.ambientShortNegativeRoot hn p t) (HigherYoungArbitraryRankDominantHighestLinePreservation.youngComplexPair lam u v) = HigherYoungArbitraryRankDominantHighestLinePreservation.youngComplexPair lam (-(HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam (HigherHarmonicYoung.DeterminantVectors.evenCoordinate hn p) t) u - (HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam (HigherHarmonicYoung.DeterminantVectors.oddCoordinate hn p) t) v) (-(HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam (HigherHarmonicYoung.DeterminantVectors.evenCoordinate hn p) t) v + (HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam (HigherHarmonicYoung.DeterminantVectors.oddCoordinate hn p) t) u)

theorem MetricCodes.Spherical.HigherYoungAllRankHighestShortRootWeightNonnegative.shortRootYoungPair_inner_adjoint {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (p : Fin (r + 1)) (t : Fin n) (u v x y : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) : inner ℝ ((HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam (HigherHarmonicYoung.DeterminantVectors.evenCoordinate hn p) t) u - (HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam (HigherHarmonicYoung.DeterminantVectors.oddCoordinate hn p) t) v) x + inner ℝ ((HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam (HigherHarmonicYoung.DeterminantVectors.evenCoordinate hn p) t) v + (HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam (HigherHarmonicYoung.DeterminantVectors.oddCoordinate hn p) t) u) y = inner ℝ u (-(HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam (HigherHarmonicYoung.DeterminantVectors.evenCoordinate hn p) t) x - (HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam (HigherHarmonicYoung.DeterminantVectors.oddCoordinate hn p) t) y) + inner ℝ v (-(HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam (HigherHarmonicYoung.DeterminantVectors.evenCoordinate hn p) t) y + (HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam (HigherHarmonicYoung.DeterminantVectors.oddCoordinate hn p) t) x)

theorem MetricCodes.Spherical.HigherYoungAllRankHighestShortRootWeightNonnegative.shortRootHighest_signedWeight_nonnegative {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) {f : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hf : f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (hfzero : f ≠ 0) (p : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) (hroot : (HigherHarmonicYoung.DeterminantVectors.ambientShortPositiveRoot hn p t) f = 0) (mu : ℤ) (hcartan : (HigherHarmonicYoung.DeterminantVectors.ambientCartan hn p) f = (2 * ↑mu) • f) : 0 ≤ mu

theorem MetricCodes.Spherical.HigherYoungAllRankHighestShortRootWeightNonnegative.positiveRootHighest_signedWeight_nonnegative {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (hstrict : 2 * (r + 1) < n) (lam : Fin (r + 1) → ℕ) {f : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hf : f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (hfzero : f ≠ 0) (mu : Fin (r + 1) → ℤ) (hroot : ∀ (alpha : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n), (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation hn alpha) f = 0) (hcartan : ∀ (p : Fin (r + 1)), (HigherHarmonicYoung.DeterminantVectors.ambientCartan hn p) f = (2 * ↑(mu p)) • f) (p : Fin (r + 1)) : 0 ≤ mu p

theorem MetricCodes.Spherical.HigherYoungAllRankHighestShortRootWeightNonnegative.positiveRootHighest_exists_naturalCartanEigenvalues {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (hstrict : 2 * (r + 1) < n) (lam : Fin (r + 1) → ℕ) {f : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hf : f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (mu : Fin (r + 1) → ℤ) (hroot : ∀ (alpha : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n), (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation hn alpha) f = 0) (hcartan : ∀ (p : Fin (r + 1)), (HigherHarmonicYoung.DeterminantVectors.ambientCartan hn p) f = (2 * ↑(mu p)) • f) : ∃ (nu : Fin (r + 1) → ℕ), ∀ (p : Fin (r + 1)), (HigherHarmonicYoung.DeterminantVectors.ambientCartan hn p) f = ↑(2 * nu p) • f

def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightProjection.ambientSignedVariableWeight {r n : ℕ} (v : Fin ((r + 1) * n)) : Fin (r + 1) → ℤ

The signed coordinate weight: positive on even isotropic indices, negative on odd ones, and zero elsewhere.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightProjection.ambientSignedVariableWeight_even {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a p : Fin (r + 1)) : ambientSignedVariableWeight (variableIndex a (DeterminantVectors.evenCoordinate h p)) = Pi.single p 1

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightProjection.ambientSignedVariableWeight_odd {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a p : Fin (r + 1)) : ambientSignedVariableWeight (variableIndex a (DeterminantVectors.oddCoordinate h p)) = Pi.single p (-1)

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightProjection.ambientSignedVariableWeight_unused {r n : ℕ} (a : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) : ambientSignedVariableWeight (variableIndex a t) = 0

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightProjection.ambientSignedWeightComponent {r n : ℕ} (h : 2 * (r + 1) ≤ n) (mu : Fin (r + 1) → ℤ) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) : MvPolynomial (Fin ((r + 1) * n)) ℂ

Project to signed ambient weight mu after changing to isotropic coordinates, then change back.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightProjection.coeff_isotropicInverse_ambientSignedWeightComponent {r n : ℕ} (h : 2 * (r + 1) ≤ n) (mu : Fin (r + 1) → ℤ) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (d : Fin ((r + 1) * n) →₀ ℕ) : ((HigherYoungAmbientRootNilpotence.isotropicCoordinateEquiv h).symm (ambientSignedWeightComponent h mu f)).coeff d = if (Finsupp.weight ambientSignedVariableWeight) d = mu then ((HigherYoungAmbientRootNilpotence.isotropicCoordinateEquiv h).symm f).coeff d else 0

theorem MetricCodes.Spherical.HigherYoungArbitraryRankAmbientSignedWeightGeneratorCartan.ambientCartan_isotropicCoordinateGenerator {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p : Fin (r + 1)) (v : Fin ((r + 1) * n)) : (HigherHarmonicYoung.DeterminantVectors.ambientCartan h p) (HigherYoungAmbientRootNilpotence.isotropicCoordinateGenerator h v) = (2 * ↑(HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightProjection.ambientSignedVariableWeight v p)) • HigherYoungAmbientRootNilpotence.isotropicCoordinateGenerator h v

noncomputable def MetricCodes.Spherical.HigherYoungArbitraryRankSignedDiagonalDerivation.signedDiagonalDerivation {ι : Type u_1} {m : ℕ} (w : ι → Fin m → ℤ) (p : Fin m) : Derivation ℂ (MvPolynomial ι ℂ) (MvPolynomial ι ℂ)

The diagonal derivation sending variable i to 2 * w i p times that variable.

Equations

• MetricCodes.Spherical.HigherYoungArbitraryRankSignedDiagonalDerivation.signedDiagonalDerivation w p = MvPolynomial.mkDerivation ℂ fun (i : ι) => (2 * ↑(w i p)) • MvPolynomial.X i

@[simp]

theorem MetricCodes.Spherical.HigherYoungArbitraryRankSignedDiagonalDerivation.signedDiagonalDerivation_X {ι : Type u_1} {m : ℕ} (w : ι → Fin m → ℤ) (p : Fin m) (i : ι) : (signedDiagonalDerivation w p) (MvPolynomial.X i) = (2 * ↑(w i p)) • MvPolynomial.X i

theorem MetricCodes.Spherical.HigherYoungArbitraryRankSignedDiagonalDerivation.signedDiagonalDerivation_eq_sum {ι : Type u_1} [Fintype ι] {m : ℕ} (w : ι → Fin m → ℤ) (p : Fin m) : signedDiagonalDerivation w p = ∑ i : ι, (2 * ↑(w i p)) • MvPolynomial.X i • MvPolynomial.pderiv i

theorem MetricCodes.Spherical.HigherYoungArbitraryRankSignedDiagonalDerivation.signedDiagonalDerivation_apply {ι : Type u_1} [Fintype ι] {m : ℕ} (w : ι → Fin m → ℤ) (p : Fin m) (q : MvPolynomial ι ℂ) : (signedDiagonalDerivation w p) q = ∑ i : ι, (2 * ↑(w i p)) • (MvPolynomial.X i * (MvPolynomial.pderiv i) q)

theorem MetricCodes.Spherical.HigherYoungArbitraryRankSignedDiagonalDerivation.signedWeight_apply {ι : Type u_1} [Fintype ι] {m : ℕ} (w : ι → Fin m → ℤ) (d : ι →₀ ℕ) (p : Fin m) : (Finsupp.weight w) d p = ∑ i : ι, ↑(d i) * w i p

theorem MetricCodes.Spherical.HigherYoungArbitraryRankSignedDiagonalDerivation.coeff_signedDiagonalDerivation {ι : Type u_1} [Finite ι] {m : ℕ} (w : ι → Fin m → ℤ) (p : Fin m) (q : MvPolynomial ι ℂ) (d : ι →₀ ℕ) : ((signedDiagonalDerivation w p) q).coeff d = 2 * ↑((Finsupp.weight w) d p) * q.coeff d

theorem MetricCodes.Spherical.HigherYoungArbitraryRankSignedDiagonalDerivation.signedDiagonal_weightedHomogeneousComponent {ι : Type u_1} [Finite ι] {m : ℕ} (w : ι → Fin m → ℤ) (p : Fin m) (mu : Fin m → ℤ) (q : MvPolynomial ι ℂ) : (signedDiagonalDerivation w p) ((MvPolynomial.weightedHomogeneousComponent w mu) q) = (2 * ↑(mu p)) • (MvPolynomial.weightedHomogeneousComponent w mu) q

theorem MetricCodes.Spherical.HigherYoungAllRankActualSignedWeightCartanEigen.conjugatedAmbientCartan_eq_signedDiagonal {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p : Fin (r + 1)) : HigherYoungArbitraryRankOrthogonalRootHighestKernel.conjugatedPolynomialDerivation (HigherYoungAmbientRootNilpotence.isotropicCoordinateEquiv h) (HigherHarmonicYoung.DeterminantVectors.ambientCartan h p) = HigherYoungArbitraryRankSignedDiagonalDerivation.signedDiagonalDerivation HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightProjection.ambientSignedVariableWeight p

theorem MetricCodes.Spherical.HigherYoungAllRankActualSignedWeightCartanEigen.ambientCartan_ambientSignedWeightComponent {r n : ℕ} (h : 2 * (r + 1) ≤ n) (mu : Fin (r + 1) → ℤ) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (p : Fin (r + 1)) : (HigherHarmonicYoung.DeterminantVectors.ambientCartan h p) (HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightProjection.ambientSignedWeightComponent h mu f) = (2 * ↑(mu p)) • HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightProjection.ambientSignedWeightComponent h mu f

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightYoungPreservation.youngComplexPolynomialSpan_top_eq_full {r n : ℕ} (lam : Fin (r + 1) → ℕ) : HigherYoungTwoRowLieIrreducibility.youngComplexPolynomialSpan lam ⊤ = HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightYoungPreservation.ambientCartan_mem_fullYoungComplexPolynomialSpan {r n : ℕ} (h : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (p : Fin (r + 1)) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hf : f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) : (DeterminantVectors.ambientCartan h p) f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightYoungPreservation.ambientSignedWeightSupport {r n : ℕ} (h : 2 * (r + 1) ≤ n) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) : Finset (Fin (r + 1) → ℤ)

The ambient signed weight support used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightYoungPreservation.ambientSignedWeightComponent_eq_zero_of_not_mem_support {r n : ℕ} (h : 2 * (r + 1) ≤ n) (mu : Fin (r + 1) → ℤ) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hmu : mu ∉ ambientSignedWeightSupport h f) : ArbitraryRankAmbientSignedWeightProjection.ambientSignedWeightComponent h mu f = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightYoungPreservation.sum_ambientSignedWeightComponent {r n : ℕ} (h : 2 * (r + 1) ≤ n) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) : ∑ mu ∈ ambientSignedWeightSupport h f, ArbitraryRankAmbientSignedWeightProjection.ambientSignedWeightComponent h mu f = f

theorem MetricCodes.Spherical.HigherYoungFiniteJointWeightProjectorInvariant.jointEigenComponent_mem_of_invariant_sum {K : Type u_1} {V : Type u_2} {α : Type u_3} {ι : Type u_4} [Field K] [AddCommGroup V] [Module K V] (T : ι → V →ₗ[K] V) (W : Submodule K V) (hW : ∀ (i : ι), ∀ x ∈ W, (T i) x ∈ W) (S : Finset α) (v : α → V) (eigen : α → ι → K) (heigen : ∀ a ∈ S, ∀ (i : ι), (T i) (v a) = eigen a i • v a) (hseparated : ∀ a ∈ S, ∀ b ∈ S, a ≠ b → ∃ (i : ι), eigen a i ≠ eigen b i) (hsum : ∑ a ∈ S, v a ∈ W) (a : α) (ha : a ∈ S) : v a ∈ W

theorem MetricCodes.Spherical.HigherYoungAllRankActualSignedWeightYoungPreservation.ambientSignedWeightComponent_mem_fullYoungComplexPolynomialSpan {r n : ℕ} (h : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (mu : Fin (r + 1) → ℤ) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hf : f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) : HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightProjection.ambientSignedWeightComponent h mu f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam

theorem MetricCodes.Spherical.HigherYoungArbitraryRankAmbientSignedWeightRootShift.derivation_isWeightedHomogeneous_of_variable_shift {σ : Type u_1} {M : Type u_2} [AddCommGroup M] (w : σ → M) (delta : M) (D : Derivation ℂ (MvPolynomial σ ℂ) (MvPolynomial σ ℂ)) (hD : ∀ (i : σ), MvPolynomial.IsWeightedHomogeneous w (D (MvPolynomial.X i)) (w i + delta)) {mu : M} {p : MvPolynomial σ ℂ} (hp : MvPolynomial.IsWeightedHomogeneous w p mu) : MvPolynomial.IsWeightedHomogeneous w (D p) (mu + delta)

theorem MetricCodes.Spherical.HigherYoungArbitraryRankAmbientSignedWeightRootShift.derivation_weightedHomogeneousComponent_shift {σ : Type u_1} {M : Type u_2} [AddCommGroup M] (w : σ → M) (delta : M) (D : Derivation ℂ (MvPolynomial σ ℂ) (MvPolynomial σ ℂ)) (hD : ∀ (i : σ), MvPolynomial.IsWeightedHomogeneous w (D (MvPolynomial.X i)) (w i + delta)) (mu : M) (p : MvPolynomial σ ℂ) : D ((MvPolynomial.weightedHomogeneousComponent w mu) p) = (MvPolynomial.weightedHomogeneousComponent w (mu + delta)) (D p)

def MetricCodes.Spherical.HigherYoungArbitraryRankAmbientSignedWeightRootShift.orthogonalPositiveRootSignedCharge {r n : ℕ} (alpha : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n) : Fin (r + 1) → ℤ

The signed coordinate charge of a difference, sum, or short positive orthogonal root.

Equations

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

theorem MetricCodes.Spherical.HigherYoungArbitraryRankAmbientSignedWeightRootShift.smul_X_isWeightedHomogeneous {σ : Type u_1} {M : Type u_2} [AddCommGroup M] (w : σ → M) (i : σ) (c : ℂ) : MvPolynomial.IsWeightedHomogeneous w (c • MvPolynomial.X i) (w i)

theorem MetricCodes.Spherical.HigherYoungArbitraryRankAmbientSignedWeightRootShift.isotropicOrthogonalPositiveRoot_X_even_isWeightedHomogeneous {r n : ℕ} (h : 2 * (r + 1) ≤ n) (alpha : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n) (a j : Fin (r + 1)) : MvPolynomial.IsWeightedHomogeneous HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightProjection.ambientSignedVariableWeight ((HigherYoungArbitraryRankOrthogonalRootHighestKernel.isotropicOrthogonalPositiveRootDerivation h alpha) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h j)))) (HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightProjection.ambientSignedVariableWeight (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h j)) + orthogonalPositiveRootSignedCharge alpha)

theorem MetricCodes.Spherical.HigherYoungArbitraryRankAmbientSignedWeightRootShift.isotropicOrthogonalPositiveRoot_X_odd_isWeightedHomogeneous {r n : ℕ} (h : 2 * (r + 1) ≤ n) (alpha : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n) (a j : Fin (r + 1)) : MvPolynomial.IsWeightedHomogeneous HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightProjection.ambientSignedVariableWeight ((HigherYoungArbitraryRankOrthogonalRootHighestKernel.isotropicOrthogonalPositiveRootDerivation h alpha) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h j)))) (HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightProjection.ambientSignedVariableWeight (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h j)) + orthogonalPositiveRootSignedCharge alpha)

theorem MetricCodes.Spherical.HigherYoungArbitraryRankAmbientSignedWeightRootShift.isotropicOrthogonalPositiveRoot_X_unused_isWeightedHomogeneous {r n : ℕ} (h : 2 * (r + 1) ≤ n) (alpha : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n) (a : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) : MvPolynomial.IsWeightedHomogeneous HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightProjection.ambientSignedVariableWeight ((HigherYoungArbitraryRankOrthogonalRootHighestKernel.isotropicOrthogonalPositiveRootDerivation h alpha) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a t))) (HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightProjection.ambientSignedVariableWeight (HigherHarmonicYoung.variableIndex a t) + orthogonalPositiveRootSignedCharge alpha)

theorem MetricCodes.Spherical.HigherYoungArbitraryRankAmbientSignedWeightRootShift.isotropicOrthogonalPositiveRoot_X_isWeightedHomogeneous {r n : ℕ} (h : 2 * (r + 1) ≤ n) (alpha : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n) (v : Fin ((r + 1) * n)) : MvPolynomial.IsWeightedHomogeneous HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightProjection.ambientSignedVariableWeight ((HigherYoungArbitraryRankOrthogonalRootHighestKernel.isotropicOrthogonalPositiveRootDerivation h alpha) (MvPolynomial.X v)) (HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightProjection.ambientSignedVariableWeight v + orthogonalPositiveRootSignedCharge alpha)

theorem MetricCodes.Spherical.HigherYoungArbitraryRankActualSignedWeightRootPreservation.orthogonalPositiveRoot_ambientSignedWeightComponent_shift {r n : ℕ} (h : 2 * (r + 1) ≤ n) (alpha : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n) (mu : Fin (r + 1) → ℤ) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) : (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation h alpha) (HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightProjection.ambientSignedWeightComponent h mu f) = HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightProjection.ambientSignedWeightComponent h (mu + HigherYoungArbitraryRankAmbientSignedWeightRootShift.orthogonalPositiveRootSignedCharge alpha) ((HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation h alpha) f)

theorem MetricCodes.Spherical.HigherYoungArbitraryRankActualSignedWeightRootPreservation.ambientSignedWeightComponent_positiveRootHighest {r n : ℕ} (h : 2 * (r + 1) ≤ n) (mu : Fin (r + 1) → ℤ) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hroots : ∀ (alpha : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n), (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation h alpha) f = 0) (alpha : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n) : (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation h alpha) (HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightProjection.ambientSignedWeightComponent h mu f) = 0

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightDecomposition.ambientSignedWeightSupport {r n : ℕ} (h : 2 * (r + 1) ≤ n) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) : Finset (Fin (r + 1) → ℤ)

The ambient signed weight support used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightDecomposition.weight_mem_ambientSignedWeightSupport_of_coeff_ne_zero {r n : ℕ} (h : 2 * (r + 1) ≤ n) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (d : Fin ((r + 1) * n) →₀ ℕ) (hd : ((HigherYoungAmbientRootNilpotence.isotropicCoordinateEquiv h).symm f).coeff d ≠ 0) : (Finsupp.weight ArbitraryRankAmbientSignedWeightProjection.ambientSignedVariableWeight) d ∈ ambientSignedWeightSupport h f

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightDecomposition.sum_ambientSignedWeightComponent_eq {r n : ℕ} (h : 2 * (r + 1) ≤ n) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) : ∑ mu ∈ ambientSignedWeightSupport h f, ArbitraryRankAmbientSignedWeightProjection.ambientSignedWeightComponent h mu f = f

theorem MetricCodes.Spherical.HigherYoungAllRankActualHighestAntiHolomorphicVanishing.antiholomorphicDerivative_eq_zero_of_fullYoung_positiveRootHighest {r n : ℕ} (h : 2 * (r + 1) ≤ n) (hstable : 2 * (r + 1) + 2 ≤ n) (lam : Fin (r + 1) → ℕ) {f : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hf : f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (hroots : ∀ (α : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n), (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation h α) f = 0) (a p : Fin (r + 1)) : (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) f = 0

theorem MetricCodes.Spherical.HigherYoungAllRankActualHighestKernelRigidity.totalAmbientCartan_eq_maximal_of_positiveRootKernel_antiholomorphic {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) {f : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hf : f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (hroots : ∀ (α : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n), (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation hn α) f = 0) (hanti : ∀ (a p : Fin (r + 1)), (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative hn a p) f = 0) : (HigherYoungAmbientCartanIsotropicEigenvalues.totalAmbientCartan hn) f = ↑(2 * ∑ i : Fin (r + 1), lam i) • f

theorem MetricCodes.Spherical.HigherYoungAllRankActualHighestKernelRigidity.mem_ambientIsotropicHighestSubmodule_of_positiveRootKernel_antiholomorphic {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) {f : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hf : f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (hroots : ∀ (α : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n), (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation hn α) f = 0) (hanti : ∀ (a p : Fin (r + 1)), (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative hn a p) f = 0) : f ∈ HigherHarmonicYoung.IsotropicAmbientHighestLine.ambientIsotropicHighestSubmodule hn lam

theorem MetricCodes.Spherical.HigherYoungAllRankActualHighestKernelRigidity.mem_ambientIsotropicHighestSubmodule_of_positiveRootKernel {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (hstable : 2 * (r + 1) + 2 ≤ n) (lam : Fin (r + 1) → ℕ) {f : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hf : f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (hroots : ∀ (α : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n), (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation hn α) f = 0) : f ∈ HigherHarmonicYoung.IsotropicAmbientHighestLine.ambientIsotropicHighestSubmodule hn lam