Binary and spherical code bounds

The unconditional characteristic-minor argument and the final headline theorems.

theorem MetricCodes.Spherical.HigherYoungAllRankActualProjectedAxisCompletion.fixedLevelHierarchyCodeBound_of_extraStrongCanonicalFischerRecurrence (hrecurrence : ∀ {r m n : ℕ} (a : Fin (r + 2) → ℝ) (b : Fin (r + 1) → ℝ), HigherHierarchy.Interlacing a b → 0 < a (Fin.last (r + 1)) → 2 * (r + 2) + 5 ≤ n + 1 → ∀ (hstable : ∀ (v : HigherHierarchy.RectangularVertices.Vertex (r + 1) m), HigherChannel.FiniteInterlacing (n + 1) (HigherHierarchy.RectangularVertices.signature a (n + 1) v) (HigherChannel.flooredCoordinates b (n + 1))) (low high : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) (row : Fin (r + 2)), HigherYoungActualGraphAssembly.boxSignature a (n + 1) high = HigherChannel.raiseWeight (HigherYoungActualGraphAssembly.boxSignature a (n + 1) low) row → HigherHarmonicYoung.AllRankCanonicalBoxActualForward.CanonicalBoxAdjacentFischerRecurrence a b hstable ⋯ low high row) : HigherHierarchy.FixedLevelHierarchyCodeBound

theorem MetricCodes.Spherical.HigherYoungAllRankActualProjectedAxisCompletion.fixedLevelHierarchyCodeBound_of_actualCharacteristicMinorAndProjector (hedges : ∀ {r m n : ℕ} (a : Fin (r + 2) → ℝ) (b : Fin (r + 1) → ℝ), HigherHierarchy.Interlacing a b → 0 < a (Fin.last (r + 1)) → 2 * (r + 2) + 5 ≤ n + 1 → ∀ (hstable : ∀ (v : HigherHierarchy.RectangularVertices.Vertex (r + 1) m), HigherChannel.FiniteInterlacing (n + 1) (HigherHierarchy.RectangularVertices.signature a (n + 1) v) (HigherChannel.flooredCoordinates b (n + 1))) (low high : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) (row : Fin (r + 2)), HigherYoungActualGraphAssembly.boxSignature a (n + 1) high = HigherChannel.raiseWeight (HigherYoungActualGraphAssembly.boxSignature a (n + 1) low) row → MetricCodes.Spherical.HigherYoungAllRankActualProjectedAxisCompletion.ActualBoxAxisCharacteristicMinor✝ a b hstable ⋯ low ∧ MetricCodes.Spherical.HigherYoungAllRankActualProjectedAxisCompletion.ActualBoxSelectedAxisProjectorAgreement✝ a b hstable ⋯ low row) : HigherHierarchy.FixedLevelHierarchyCodeBound

theorem MetricCodes.Spherical.HigherYoungAllRankActualProjectedAxisCompletion.fixedLevelHierarchyCodeBound_of_actualCharacteristicMinor (hminor : ∀ {r m n : ℕ} (a : Fin (r + 2) → ℝ) (b : Fin (r + 1) → ℝ), HigherHierarchy.Interlacing a b → 0 < a (Fin.last (r + 1)) → 2 * (r + 2) + 5 ≤ n + 1 → ∀ (hstable : ∀ (v : HigherHierarchy.RectangularVertices.Vertex (r + 1) m), HigherChannel.FiniteInterlacing (n + 1) (HigherHierarchy.RectangularVertices.signature a (n + 1) v) (HigherChannel.flooredCoordinates b (n + 1))) (low : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m), MetricCodes.Spherical.HigherYoungAllRankActualProjectedAxisCompletion.ActualBoxAxisCharacteristicMinor✝ a b hstable ⋯ low) : HigherHierarchy.FixedLevelHierarchyCodeBound

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTerminalNegativeProjectorVanishing.allRankCartanCharacteristicProjector_last_false_eq_zero {r n : ℕ} (hn : 2 * r + 4 ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (hzero : lam (Fin.last r) = 0) (mu : Fin r → ℕ) (hfinite : HigherChannel.FiniteInterlacing n lam mu) : AllRankCartanCharacteristicProjector.allRankCartanCharacteristicProjector lam (Fin.last r, false) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTerminalNegativeProjectorVanishing.signedCharacteristicProjector_last_false_eq_zero {r n : ℕ} (hn : 2 * r + 4 ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (hzero : lam (Fin.last r) = 0) (mu : Fin r → ℕ) (hfinite : HigherChannel.FiniteInterlacing n lam mu) : AllRankGTCompressedResolvent.signedCharacteristicProjector (HigherChannel.ambientShift n lam) (AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam) (Fin.last r, false) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTerminalNegativeProjectorVanishing.gtAxisCompressedSignedProjectorCoefficient_last_false_eq_zero {r n : ℕ} (hn : 2 * (r + 1) + 4 ≤ n + 1) (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hdom : Antitone lam) (hzero : lam (Fin.last (r + 1)) = 0) (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (p q : ↥(HarmonicYoungSpace mu)) : AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedSignedProjectorCoefficient lam mu h hgram p q (Fin.last (r + 1), false) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTAbsentWallCharacteristicFactor.ambientShift_last_eq_wallShift_of_last_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (hlast : lam (Fin.last (r + 1)) = 0) : HigherChannel.ambientShift (n + 1) lam (Fin.last (r + 1)) = HigherChannel.wallShift (n + 1) (r + 1)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTAbsentWallCharacteristicFactor.signedNode_last_false_eq_neg_wallShift {r n : ℕ} (lam : Fin (r + 2) → ℕ) (hlast : lam (Fin.last (r + 1)) = 0) : HigherChannel.signedNode (HigherChannel.ambientShift (n + 1) lam) (Fin.last (r + 1), false) = -HigherChannel.wallShift (n + 1) (r + 1)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTAbsentWallCharacteristicFactor.gtAxisCompressedCharacteristicMinor_eval_neg_wallShift {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (hlast : lam (Fin.last (r + 1)) = 0) (p q : ↥(HarmonicYoungSpace mu)) : Polynomial.eval (-HigherChannel.wallShift (n + 1) (r + 1)) (AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedCharacteristicMinor lam mu h hgram p q) = Polynomial.eval (-HigherChannel.wallShift (n + 1) (r + 1)) (Polynomial.derivative (HigherYoungAllRankGTCharacteristicResidue.gtChannelCharacteristicPolynomial (n + 1) lam)) * AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedSignedProjectorCoefficient lam mu h hgram p q (Fin.last (r + 1), false)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTAbsentWallCharacteristicFactor.gtAxisCompressedCharacteristicMinor_eval_neg_wallShift_eq_zero_iff {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (hlast : lam (Fin.last (r + 1)) = 0) (p q : ↥(HarmonicYoungSpace mu)) : Polynomial.eval (-HigherChannel.wallShift (n + 1) (r + 1)) (AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedCharacteristicMinor lam mu h hgram p q) = 0 ↔ AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedSignedProjectorCoefficient lam mu h hgram p q (Fin.last (r + 1), false) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTAbsentWallCharacteristicFactor.gtAxisCompressedCharacteristicMinor_eval_neg_wallShift_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (hlast : lam (Fin.last (r + 1)) = 0) (p q : ↥(HarmonicYoungSpace mu)) (hforbidden : AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedSignedProjectorCoefficient lam mu h hgram p q (Fin.last (r + 1), false) = 0) : Polynomial.eval (-HigherChannel.wallShift (n + 1) (r + 1)) (AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedCharacteristicMinor lam mu h hgram p q) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTAbsentWallCharacteristicFactor.gtAxisCompressedCharacteristicMinor_eval_neg_wallShift_eq_zero_of_last_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (hlast : lam (Fin.last (r + 1)) = 0) (p q : ↥(HarmonicYoungSpace mu)) : Polynomial.eval (-HigherChannel.wallShift (n + 1) (r + 1)) (AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedCharacteristicMinor lam mu h hgram p q) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTPhysicalInvalidRowProjectorVanishing.interlaces_of_appendZeroWeight {r : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces (ThreeRowYoungBranching.appendZeroWeight lam) (ThreeRowYoungBranching.appendZeroWeight mu)) : HigherRepresentationGraph.Interlaces lam mu

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTPhysicalInvalidRowProjectorVanishing.pieri_crossGram_intertwines_of_skew {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (i : HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.PaddedPieriChannel (ThreeRowYoungBranching.appendZeroWeight lam)) (A : ↥(HarmonicYoungSpace (HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.paddedPieriSource (ThreeRowYoungBranching.appendZeroWeight lam) i)) →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean (n + 1)) ↥(HarmonicYoungSpace (ThreeRowYoungBranching.appendZeroWeight lam))) (B : ↥(HarmonicYoungSpace (ThreeRowYoungBranching.appendZeroWeight (ThreeRowYoungBranching.appendZeroWeight mu))) →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean (n + 1)) ↥(HarmonicYoungSpace (ThreeRowYoungBranching.appendZeroWeight lam))) (R : ↥(HarmonicYoungSpace (HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.paddedPieriSource (ThreeRowYoungBranching.appendZeroWeight lam) i)) →ₗ[ℝ] ↥(HarmonicYoungSpace (HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.paddedPieriSource (ThreeRowYoungBranching.appendZeroWeight lam) i))) (T : ↥(HarmonicYoungSpace (ThreeRowYoungBranching.appendZeroWeight (ThreeRowYoungBranching.appendZeroWeight mu))) →ₗ[ℝ] ↥(HarmonicYoungSpace (ThreeRowYoungBranching.appendZeroWeight (ThreeRowYoungBranching.appendZeroWeight mu)))) (S : TensorProduct ℝ (SpherePacking.Euclidean (n + 1)) ↥(HarmonicYoungSpace (ThreeRowYoungBranching.appendZeroWeight lam)) →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean (n + 1)) ↥(HarmonicYoungSpace (ThreeRowYoungBranching.appendZeroWeight lam))) (hR : LinearMap.adjoint R = -R) (hS : LinearMap.adjoint S = -S) (hA : A ∘ₗ R = S ∘ₗ A) (hB : B ∘ₗ T = S ∘ₗ B) : (LinearMap.adjoint A ∘ₗ B) ∘ₗ T = R ∘ₗ LinearMap.adjoint A ∘ₗ B

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTPhysicalInvalidRowProjectorVanishing.physicalPaddedPieriChannel_adjoint_canonicalAxis_eq_zero_of_not_interlaces {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hdom : Antitone lam) (hn : 2 * (r + 2) + 5 ≤ n + 1) (i : HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.PaddedPieriChannel (ThreeRowYoungBranching.appendZeroWeight lam)) (hbad : ¬HigherRepresentationGraph.Interlaces (HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.paddedPieriSource (ThreeRowYoungBranching.appendZeroWeight lam) i) (ThreeRowYoungBranching.appendZeroWeight mu)) (p : ↥(HarmonicYoungSpace mu)) : (LinearMap.adjoint (AllRankGTTransportedPieriOrthogonality.physicalPaddedPieriChannel ⋯ lam ⋯ i).toLinearMap) ((AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor lam mu h hgram) p) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTPhysicalInvalidRowProjectorVanishing.canonicalAxis_mem_retainedPhysicalPieriSpan {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hdom : Antitone lam) (hn : 2 * (r + 2) + 5 ≤ n + 1) (p : ↥(HarmonicYoungSpace mu)) : (AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor lam mu h hgram) p ∈ ⨆ (i : { j : HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.PaddedPieriChannel (ThreeRowYoungBranching.appendZeroWeight lam) // AllRankGTRelativeCasimirZeroRowTransport.retainedPaddedPieriChannel lam j }), (AllRankGTTransportedPieriOrthogonality.physicalPaddedPieriChannel ⋯ lam ⋯ ↑i).range

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTPhysicalInvalidRowProjectorVanishing.signedCharacteristicProjector_canonicalAxis_eq_zero_of_matching_noninterlacing {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (hn : 2 * (r + 2) + 5 ≤ n + 1) (selected : Fin (r + 2) × Bool) (hbad : ∀ (i : { j : HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.PaddedPieriChannel (ThreeRowYoungBranching.appendZeroWeight lam) // AllRankGTRelativeCasimirZeroRowTransport.retainedPaddedPieriChannel lam j }), AllRankGTRelativeCasimirZeroRowTransport.retainedPaddedPieriSignedNode lam i = selected → ¬HigherRepresentationGraph.Interlaces (AllRankGTRelativeCasimirZeroRowTransport.retainedPaddedPieriPhysicalSource lam i) mu) (p : ↥(HarmonicYoungSpace mu)) : (AllRankGTCompressedResolvent.signedCharacteristicProjector (HigherChannel.ambientShift (n + 1) lam) (AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam) selected) ((AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor lam mu h hgram) p) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTPhysicalInvalidRowProjectorVanishing.retainedPhysicalSource_not_interlaces_of_invalid_negative {r : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (row : Fin (r + 1)) (hbad : ¬HigherRepresentationGraph.Interlaces lam (HigherChannel.raiseWeight mu row)) (i : { j : HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.PaddedPieriChannel (ThreeRowYoungBranching.appendZeroWeight lam) // AllRankGTRelativeCasimirZeroRowTransport.retainedPaddedPieriChannel lam j }) (hi : AllRankGTRelativeCasimirZeroRowTransport.retainedPaddedPieriSignedNode lam i = (row.castSucc, false)) : ¬HigherRepresentationGraph.Interlaces (AllRankGTRelativeCasimirZeroRowTransport.retainedPaddedPieriPhysicalSource lam i) mu

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTPhysicalInvalidRowProjectorVanishing.retainedPhysicalSource_not_interlaces_of_invalid_positive {r : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (row : Fin (r + 1)) (hbad : mu row = 0 ∨ ¬HigherRepresentationGraph.Interlaces lam (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight mu row)) (i : { j : HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.PaddedPieriChannel (ThreeRowYoungBranching.appendZeroWeight lam) // AllRankGTRelativeCasimirZeroRowTransport.retainedPaddedPieriChannel lam j }) (hi : AllRankGTRelativeCasimirZeroRowTransport.retainedPaddedPieriSignedNode lam i = (row.succ, true)) : ¬HigherRepresentationGraph.Interlaces (AllRankGTRelativeCasimirZeroRowTransport.retainedPaddedPieriPhysicalSource lam i) mu

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTPhysicalInvalidRowProjectorVanishing.signedCharacteristicProjector_canonicalAxis_invalid_negative_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (hn : 2 * (r + 2) + 5 ≤ n + 1) (row : Fin (r + 1)) (hbad : ¬HigherRepresentationGraph.Interlaces lam (HigherChannel.raiseWeight mu row)) (p : ↥(HarmonicYoungSpace mu)) : (AllRankGTCompressedResolvent.signedCharacteristicProjector (HigherChannel.ambientShift (n + 1) lam) (AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam) (row.castSucc, false)) ((AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor lam mu h hgram) p) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTPhysicalInvalidRowProjectorVanishing.signedCharacteristicProjector_canonicalAxis_invalid_positive_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (hn : 2 * (r + 2) + 5 ≤ n + 1) (row : Fin (r + 1)) (hbad : mu row = 0 ∨ ¬HigherRepresentationGraph.Interlaces lam (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight mu row)) (p : ↥(HarmonicYoungSpace mu)) : (AllRankGTCompressedResolvent.signedCharacteristicProjector (HigherChannel.ambientShift (n + 1) lam) (AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam) (row.succ, true)) ((AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor lam mu h hgram) p) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTPhysicalInvalidRowProjectorVanishing.gtAxisCompressedSignedProjectorCoefficient_invalid_negative_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (hn : 2 * (r + 2) + 5 ≤ n + 1) (row : Fin (r + 1)) (hbad : ¬HigherRepresentationGraph.Interlaces lam (HigherChannel.raiseWeight mu row)) (p q : ↥(HarmonicYoungSpace mu)) : AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedSignedProjectorCoefficient lam mu h hgram p q (row.castSucc, false) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTPhysicalInvalidRowProjectorVanishing.gtAxisCompressedSignedProjectorCoefficient_invalid_positive_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (hn : 2 * (r + 2) + 5 ≤ n + 1) (row : Fin (r + 1)) (hbad : mu row = 0 ∨ ¬HigherRepresentationGraph.Interlaces lam (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight mu row)) (p q : ↥(HarmonicYoungSpace mu)) : AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedSignedProjectorCoefficient lam mu h hgram p q (row.succ, true) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTPhysicalInvalidRowProjectorVanishing.gtAxisCompressedCharacteristicMinor_eval_negativeStabilizerNode_eq_zero_of_invalid {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (hn : 2 * (r + 2) + 5 ≤ n + 1) (row : Fin (r + 1)) (hbad : ¬HigherRepresentationGraph.Interlaces lam (HigherChannel.raiseWeight mu row)) (p q : ↥(HarmonicYoungSpace mu)) : Polynomial.eval (HigherYoungAllRankGTArrowheadSchurComplement.gtStabilizerArrowheadNode (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) mu) (Sum.inr (row, false))) (AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedCharacteristicMinor lam mu h hgram p q) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTPhysicalInvalidRowProjectorVanishing.gtAxisCompressedCharacteristicMinor_eval_positiveStabilizerNode_eq_zero_of_invalid {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (hn : 2 * (r + 2) + 5 ≤ n + 1) (row : Fin (r + 1)) (hbad : mu row = 0 ∨ ¬HigherRepresentationGraph.Interlaces lam (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight mu row)) (p q : ↥(HarmonicYoungSpace mu)) : Polynomial.eval (HigherYoungAllRankGTArrowheadSchurComplement.gtStabilizerArrowheadNode (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) mu) (Sum.inr (row, true))) (AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedCharacteristicMinor lam mu h hgram p q) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCharacteristicDeterminant.nodal_erase_coeff_card_pred {ι : Type u_1} [Fintype ι] [DecidableEq ι] (nodes : ι → ℝ) (i : ι) : (Lagrange.nodal (Finset.univ.erase i) nodes).coeff (Fintype.card ι - 1) = 1

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCharacteristicDeterminant.gtAxisCompressedCharacteristicMinor_coeff_card_pred {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (p q : ↥(HarmonicYoungSpace mu)) : (AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedCharacteristicMinor lam mu h hgram p q).coeff (Fintype.card (Fin (r + 2) × Bool) - 1) = inner ℝ p q

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCharacteristicDeterminant.polynomial_eq_C_mul_nodal_of_roots_and_topCoeff {ι : Type u_1} [Fintype ι] (nodes : ι → ℝ) (hinj : Function.Injective nodes) (P : Polynomial ℝ) (c : ℝ) (hdeg : P.degree < ↑(Fintype.card ι) + 1) (hcoeff : P.coeff (Fintype.card ι) = c) (hroot : ∀ (i : ι), Polynomial.eval (nodes i) P = 0) : P = Polynomial.C c * Lagrange.nodal Finset.univ nodes

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCharacteristicDeterminant.gtStabilizerArrowheadNode_injective_of_gap {r : ℕ} (rho : ℝ) (M : Fin r → ℝ) (hrho : 0 < rho) (hgap : ∀ (i : Fin r), rho + 1 / 2 ≤ M i) (hinj : Function.Injective M) : Function.Injective (HigherYoungAllRankGTArrowheadSchurComplement.gtStabilizerArrowheadNode rho M)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCharacteristicDeterminant.gtStabilizerArrowheadNode_injective_of_interlacing {r n : ℕ} {lam : Fin (r + 2) → ℕ} {mu : Fin (r + 1) → ℕ} (h : HigherChannel.FiniteInterlacing (n + 1) lam mu) : Function.Injective (HigherYoungAllRankGTArrowheadSchurComplement.gtStabilizerArrowheadNode (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) mu))

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCharacteristicDeterminant.gtAxisCompressedCharacteristicMinor_eq_stabilizerArrowheadMinor_of_roots {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (p q : ↥(HarmonicYoungSpace mu)) (hroot : ∀ (j : Unit ⊕ Fin (r + 1) × Bool), Polynomial.eval (HigherYoungAllRankGTArrowheadSchurComplement.gtStabilizerArrowheadNode (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) mu) j) (AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedCharacteristicMinor lam mu h hgram p q) = 0) : AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedCharacteristicMinor lam mu h hgram p q = Polynomial.C (inner ℝ p q) * HigherYoungAllRankGTArrowheadSchurComplement.gtStabilizerArrowheadMinor (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) mu)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCharacteristicDeterminant.gtAxisCompressedCharacteristicMinor_eq_channelNumerator_of_roots {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (p q : ↥(HarmonicYoungSpace mu)) (hroot : ∀ (j : Unit ⊕ Fin (r + 1) × Bool), Polynomial.eval (HigherYoungAllRankGTArrowheadSchurComplement.gtStabilizerArrowheadNode (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) mu) j) (AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedCharacteristicMinor lam mu h hgram p q) = 0) : AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedCharacteristicMinor lam mu h hgram p q = Polynomial.C (inner ℝ p q) * HigherChannel.channelNumeratorPolynomial (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) mu)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCharacteristicMinorOfValidRoots.gtAxisCompressedCharacteristicMinor_eq_channelNumerator_of_validRoots {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (hn : 2 * (r + 2) + 5 ≤ n + 1) (p q : ↥(HarmonicYoungSpace mu)) (hwall : Polynomial.eval (-HigherChannel.wallShift (n + 1) (r + 1)) (AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedCharacteristicMinor lam mu h hgram p q) = 0) (hnegative : ∀ (row : Fin (r + 1)), HigherRepresentationGraph.Interlaces lam (HigherChannel.raiseWeight mu row) → Polynomial.eval (HigherYoungAllRankGTArrowheadSchurComplement.gtStabilizerArrowheadNode (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) mu) (Sum.inr (row, false))) (AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedCharacteristicMinor lam mu h hgram p q) = 0) (hpositive : ∀ (row : Fin (r + 1)), 0 < mu row → HigherRepresentationGraph.Interlaces lam (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight mu row) → Polynomial.eval (HigherYoungAllRankGTArrowheadSchurComplement.gtStabilizerArrowheadNode (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) mu) (Sum.inr (row, true))) (AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedCharacteristicMinor lam mu h hgram p q) = 0) : AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedCharacteristicMinor lam mu h hgram p q = Polynomial.C (inner ℝ p q) * HigherChannel.channelNumeratorPolynomial (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) mu)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTStabilizerCasimirShift.stabilizerShift_succ_eq_ambientShift {r n : ℕ} (mu : Fin (r + 1) → ℕ) (row : Fin (r + 1)) : HigherChannel.stabilizerShift (n + 1) mu row = HigherChannel.ambientShift n mu row

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTStabilizerCasimirShift.gtStabilizerCasimir_raiseBranch_eigenvalue {r n : ℕ} (mu : Fin (r + 1) → ℕ) (row : Fin (r + 1)) : (MixedSignature.allRankCasimirEigenvalue n mu - MixedSignature.allRankCasimirEigenvalue n (HigherChannel.raiseWeight mu row)) / 2 = -HigherChannel.stabilizerShift (n + 1) mu row - 1 / 2

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTStabilizerCasimirShift.gtStabilizerCasimir_lowerBranch_eigenvalue {r n : ℕ} (mu nu : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hnu : mu = HigherChannel.raiseWeight nu row) : (MixedSignature.allRankCasimirEigenvalue n mu - MixedSignature.allRankCasimirEigenvalue n nu) / 2 = HigherChannel.stabilizerShift (n + 1) mu row - 1 / 2

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTStabilizerCasimirShift.gtStabilizerRelativeCasimir_raiseTarget_eigenvalue {r n : ℕ} (mu : Fin (r + 1) → ℕ) (row : Fin (r + 1)) : (MixedSignature.allRankCasimirEigenvalue n mu - MixedSignature.allRankCasimirEigenvalue n (HigherChannel.raiseWeight mu row) - 1) / 2 = -HigherChannel.stabilizerShift (n + 1) mu row - 1

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTStabilizerCasimirShift.gtStabilizerRelativeCasimir_lowerTarget_eigenvalue {r n : ℕ} (mu nu : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hnu : mu = HigherChannel.raiseWeight nu row) : (MixedSignature.allRankCasimirEigenvalue n mu - MixedSignature.allRankCasimirEigenvalue n nu - 1) / 2 = HigherChannel.stabilizerShift (n + 1) mu row - 1

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTStabilizerCasimirShift.gtStabilizerShiftedRelativeCasimir_raiseTarget_channel {r n : ℕ} (mu : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (A : ↥(HarmonicYoungSpace mu) →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace (HigherChannel.raiseWeight mu row))) (hA : ∀ (a b : Fin n), A ∘ₗ MixedSignature.youngAmbientRotation mu a b = ClebschRotation.tensorAmbientRotation (HigherChannel.raiseWeight mu row) a b ∘ₗ A) (p : ↥(HarmonicYoungSpace mu)) : (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTStabilizerCasimirShift.gtStabilizerShiftedRelativeCasimir✝ (HigherChannel.raiseWeight mu row)) (A p) = HigherYoungAllRankGTArrowheadSchurComplement.gtStabilizerArrowheadNode (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) mu) (Sum.inr (row, false)) • A p

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTStabilizerCasimirShift.gtStabilizerShiftedRelativeCasimir_lowerTarget_channel {r n : ℕ} (mu nu : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hnu : mu = HigherChannel.raiseWeight nu row) (A : ↥(HarmonicYoungSpace mu) →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace nu)) (hA : ∀ (a b : Fin n), A ∘ₗ MixedSignature.youngAmbientRotation mu a b = ClebschRotation.tensorAmbientRotation nu a b ∘ₗ A) (p : ↥(HarmonicYoungSpace mu)) : (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTStabilizerCasimirShift.gtStabilizerShiftedRelativeCasimir✝ nu) (A p) = HigherYoungAllRankGTArrowheadSchurComplement.gtStabilizerArrowheadNode (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) mu) (Sum.inr (row, true)) • A p

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseEuclidean_castSucc (n : ℕ) (x : SpherePacking.Euclidean n) (i : Fin n) : ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseEuclidean✝ n) x).ofLp i.castSucc = x.ofLp i

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseEuclidean_last (n : ℕ) (x : SpherePacking.Euclidean n) : ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseEuclidean✝ n) x).ofLp (Fin.last n) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseEuclidean_inner (n : ℕ) (x y : SpherePacking.Euclidean n) : inner ℝ ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseEuclidean✝ n) x) ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseEuclidean✝ n) y) = inner ℝ x y

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseEuclideanIsometry_castSucc (n : ℕ) (x : SpherePacking.Euclidean n) (i : Fin n) : ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseEuclideanIsometry✝ n) x).ofLp i.castSucc = x.ofLp i

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseEuclideanIsometry_last (n : ℕ) (x : SpherePacking.Euclidean n) : ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseEuclideanIsometry✝ n) x).ofLp (Fin.last n) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseEuclideanIsometry_orthogonal_last (n : ℕ) (x : SpherePacking.Euclidean n) : inner ℝ ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseEuclideanIsometry✝ n) x) ((EuclideanSpace.basisFun (Fin (n + 1)) ℝ) (Fin.last n)) = 0

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseTensorEmbedding_tmul {r n : ℕ} (lam : Fin (r + 2) → ℕ) (nu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam nu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam nu h) (v : SpherePacking.Euclidean n) (p : ↥(HarmonicYoungSpace nu)) : (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseTensorEmbedding✝ lam nu h hgram) (v ⊗ₜ[ℝ] p) = (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseEuclideanIsometry✝ n) v ⊗ₜ[ℝ] (AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFibre lam nu h hgram) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseTensorEmbedding_axis_inner_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (nu mu : Fin (r + 1) → ℕ) (hnu : HigherRepresentationGraph.Interlaces lam nu) (hnuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam nu hnu) (hmu : HigherRepresentationGraph.Interlaces lam mu) (hmuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu hmu) (x : TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace nu)) (q : ↥(HarmonicYoungSpace mu)) : inner ℝ ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseTensorEmbedding✝ lam nu hnu hnuGram) x) ((AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor lam mu hmu hmuGram) q) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseNegativeSector_axis_inner_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hnu : HigherRepresentationGraph.Interlaces lam (HigherChannel.raiseWeight mu row)) (hnuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam (HigherChannel.raiseWeight mu row) hnu) (hmu : HigherRepresentationGraph.Interlaces lam mu) (hmuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu hmu) (p q : ↥(HarmonicYoungSpace mu)) : inner ℝ ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseNegativeSector✝ lam mu row hnu hnuGram) p) ((AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor lam mu hmu hmuGram) q) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransversePositiveSector_axis_inner_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu nu : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hmunu : mu = HigherChannel.raiseWeight nu row) (hnu : HigherRepresentationGraph.Interlaces lam nu) (hnuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam nu hnu) (hmu : HigherRepresentationGraph.Interlaces lam mu) (hmuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu hmu) (p q : ↥(HarmonicYoungSpace mu)) : inner ℝ ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransversePositiveSector✝ lam mu nu row hmunu hnu hnuGram) p) ((AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor lam mu hmu hmuGram) q) = 0

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseTangentialCompression.gtTransverseEuclideanIsometry_rotation_intertwine (n : ℕ) (a b : Fin n) : (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseEuclideanIsometry✝ n).toLinearMap ∘ₗ ClebschRotation.euclideanAmbientRotation a b = ClebschRotation.euclideanAmbientRotation a.castSucc b.castSucc ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseEuclideanIsometry✝ n).toLinearMap

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseTangentialCompression.gtTransverseEuclideanIsometry_rotation_adjoint_compression (n : ℕ) (a b : Fin n) : LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseEuclideanIsometry✝ n).toLinearMap ∘ₗ ClebschRotation.euclideanAmbientRotation a.castSucc b.castSucc ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseEuclideanIsometry✝ n).toLinearMap = ClebschRotation.euclideanAmbientRotation a b

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseTangentialCompression.gtTransverseEuclideanIsometry_adjoint_basisFun_last (n : ℕ) : (LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseEuclideanIsometry✝ n).toLinearMap) ((EuclideanSpace.basisFun (Fin (n + 1)) ℝ) (Fin.last n)) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseTangentialCompression.gtTransverseEuclideanIsometry_cross_rotation_compression (n : ℕ) (a : Fin n) : LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseEuclideanIsometry✝ n).toLinearMap ∘ₗ ClebschRotation.euclideanAmbientRotation a.castSucc (Fin.last n) ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseEuclideanIsometry✝ n).toLinearMap = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseTangentialCompression.gtTransverseEuclideanIsometry_cross_rotation_compression_swap (n : ℕ) (a : Fin n) : LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseEuclideanIsometry✝ n).toLinearMap ∘ₗ ClebschRotation.euclideanAmbientRotation (Fin.last n) a.castSucc ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseEuclideanIsometry✝ n).toLinearMap = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseTangentialCompression.gtTransverseTensorEmbedding_rotationTerm_adjoint_compression {r n : ℕ} (lam : Fin (r + 2) → ℕ) (nu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam nu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam nu h) (a b : Fin (n + 1)) : LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseTensorEmbedding✝ lam nu h hgram).toLinearMap ∘ₗ TensorProduct.map (ClebschRotation.euclideanAmbientRotation a b) (MixedSignature.youngAmbientRotation lam a b) ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseTensorEmbedding✝ lam nu h hgram).toLinearMap = TensorProduct.map (LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseEuclideanIsometry✝ n).toLinearMap ∘ₗ ClebschRotation.euclideanAmbientRotation a b ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseEuclideanIsometry✝ n).toLinearMap) (LinearMap.adjoint (AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFibre lam nu h hgram).toLinearMap ∘ₗ MixedSignature.youngAmbientRotation lam a b ∘ₗ (AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFibre lam nu h hgram).toLinearMap)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseTangentialCompression.gtTransverseTensorEmbedding_tangentialTerm_adjoint_compression {r n : ℕ} (lam : Fin (r + 2) → ℕ) (nu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam nu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam nu h) (a b : Fin n) : LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseTensorEmbedding✝ lam nu h hgram).toLinearMap ∘ₗ TensorProduct.map (ClebschRotation.euclideanAmbientRotation a.castSucc b.castSucc) (MixedSignature.youngAmbientRotation lam a.castSucc b.castSucc) ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseTensorEmbedding✝ lam nu h hgram).toLinearMap = TensorProduct.map (ClebschRotation.euclideanAmbientRotation a b) (MixedSignature.youngAmbientRotation nu a b)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseTangentialCompression.gtTransverseTensorEmbedding_crossTerm_adjoint_compression {r n : ℕ} (lam : Fin (r + 2) → ℕ) (nu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam nu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam nu h) (a : Fin n) : LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseTensorEmbedding✝ lam nu h hgram).toLinearMap ∘ₗ TensorProduct.map (ClebschRotation.euclideanAmbientRotation a.castSucc (Fin.last n)) (MixedSignature.youngAmbientRotation lam a.castSucc (Fin.last n)) ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseTensorEmbedding✝ lam nu h hgram).toLinearMap = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseTangentialCompression.gtTransverseTensorEmbedding_crossTerm_adjoint_compression_swap {r n : ℕ} (lam : Fin (r + 2) → ℕ) (nu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam nu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam nu h) (a : Fin n) : LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseTensorEmbedding✝ lam nu h hgram).toLinearMap ∘ₗ TensorProduct.map (ClebschRotation.euclideanAmbientRotation (Fin.last n) a.castSucc) (MixedSignature.youngAmbientRotation lam (Fin.last n) a.castSucc) ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseTensorEmbedding✝ lam nu h hgram).toLinearMap = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseTangentialCompression.gtTransverseTensorEmbedding_lastTerm_adjoint_compression {r n : ℕ} (lam : Fin (r + 2) → ℕ) (nu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam nu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam nu h) : LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseTensorEmbedding✝ lam nu h hgram).toLinearMap ∘ₗ TensorProduct.map (ClebschRotation.euclideanAmbientRotation (Fin.last n) (Fin.last n)) (MixedSignature.youngAmbientRotation lam (Fin.last n) (Fin.last n)) ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseTensorEmbedding✝ lam nu h hgram).toLinearMap = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseTangentialCompression.gtTransverseTensorEmbedding_mixedRotation_adjoint_compression {r n : ℕ} (lam : Fin (r + 2) → ℕ) (nu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam nu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam nu h) : LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseTensorEmbedding✝ lam nu h hgram).toLinearMap ∘ₗ AllRankGTRelativeCasimirPureAxis.gtMixedRotationOperator lam ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseTensorEmbedding✝ lam nu h hgram).toLinearMap = AllRankGTRelativeCasimirPureAxis.gtMixedRotationOperator nu

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseTensorRelativeCompression.gtRelativeCasimir_eq_scalar_sub_mixed {r n : ℕ} (lam : Fin (r + 1) → ℕ) : AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam = ((↑n - 2) / 2) • LinearMap.id - 2⁻¹ • AllRankGTRelativeCasimirPureAxis.gtMixedRotationOperator lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseTensorRelativeCompression.gtRelativeCasimir_transverse_compression_of_mixed {r n : ℕ} (lam : Fin (r + 2) → ℕ) (nu : Fin (r + 1) → ℕ) (I : TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace nu) →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean (n + 1)) ↥(HarmonicYoungSpace lam)) (hisom : LinearMap.adjoint I ∘ₗ I = LinearMap.id) (hmixed : LinearMap.adjoint I ∘ₗ AllRankGTRelativeCasimirPureAxis.gtMixedRotationOperator lam ∘ₗ I = AllRankGTRelativeCasimirPureAxis.gtMixedRotationOperator nu) : LinearMap.adjoint I ∘ₗ AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam ∘ₗ I = MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTStabilizerCasimirShift.gtStabilizerShiftedRelativeCasimir✝ nu

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseTensorRelativeCompression.gtRelativeCasimir_gtTransverseTensorEmbedding_adjoint_compression_of_mixed {r n : ℕ} (lam : Fin (r + 2) → ℕ) (nu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam nu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam nu h) (hmixed : LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseTensorEmbedding✝ lam nu h hgram).toLinearMap ∘ₗ AllRankGTRelativeCasimirPureAxis.gtMixedRotationOperator lam ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseTensorEmbedding✝ lam nu h hgram).toLinearMap = AllRankGTRelativeCasimirPureAxis.gtMixedRotationOperator nu) : LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseTensorEmbedding✝ lam nu h hgram).toLinearMap ∘ₗ AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseTensorEmbedding✝ lam nu h hgram).toLinearMap = MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTStabilizerCasimirShift.gtStabilizerShiftedRelativeCasimir✝ nu

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseTensorRelativeCompression.gtTransverseNegativeSector_relativeCasimir_adjoint_compression_of_mixed {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hnu : HigherRepresentationGraph.Interlaces lam (HigherChannel.raiseWeight mu row)) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam (HigherChannel.raiseWeight mu row) hnu) (hmixed : LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseTensorEmbedding✝ lam (HigherChannel.raiseWeight mu row) hnu hgram).toLinearMap ∘ₗ AllRankGTRelativeCasimirPureAxis.gtMixedRotationOperator lam ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseTensorEmbedding✝ lam (HigherChannel.raiseWeight mu row) hnu hgram).toLinearMap = AllRankGTRelativeCasimirPureAxis.gtMixedRotationOperator (HigherChannel.raiseWeight mu row)) (p : ↥(HarmonicYoungSpace mu)) : (LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseTensorEmbedding✝ lam (HigherChannel.raiseWeight mu row) hnu hgram).toLinearMap) ((AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam) ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseNegativeSector✝ lam mu row hnu hgram) p)) = HigherYoungAllRankGTArrowheadSchurComplement.gtStabilizerArrowheadNode (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) mu) (Sum.inr (row, false)) • (youngClebschRaise (HigherChannel.raiseWeight mu row) mu ⋯ row) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseTensorRelativeCompression.gtTransversePositiveSector_relativeCasimir_adjoint_compression_of_mixed {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu nu : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hmu : mu = HigherChannel.raiseWeight nu row) (hnu : HigherRepresentationGraph.Interlaces lam nu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam nu hnu) (hmixed : LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseTensorEmbedding✝ lam nu hnu hgram).toLinearMap ∘ₗ AllRankGTRelativeCasimirPureAxis.gtMixedRotationOperator lam ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseTensorEmbedding✝ lam nu hnu hgram).toLinearMap = AllRankGTRelativeCasimirPureAxis.gtMixedRotationOperator nu) (p : ↥(HarmonicYoungSpace mu)) : (LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseTensorEmbedding✝ lam nu hnu hgram).toLinearMap) ((AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam) ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransversePositiveSector✝ lam mu nu row hmu hnu hgram) p)) = HigherYoungAllRankGTArrowheadSchurComplement.gtStabilizerArrowheadNode (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) mu) (Sum.inr (row, true)) • (youngClebschLower nu mu ⋯ row) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseTensorRelativeCompression.gtTransverseNegativeSector_relativeCasimir_adjoint_compression {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hnu : HigherRepresentationGraph.Interlaces lam (HigherChannel.raiseWeight mu row)) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam (HigherChannel.raiseWeight mu row) hnu) (p : ↥(HarmonicYoungSpace mu)) : (LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseTensorEmbedding✝ lam (HigherChannel.raiseWeight mu row) hnu hgram).toLinearMap) ((AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam) ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseNegativeSector✝ lam mu row hnu hgram) p)) = HigherYoungAllRankGTArrowheadSchurComplement.gtStabilizerArrowheadNode (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) mu) (Sum.inr (row, false)) • (youngClebschRaise (HigherChannel.raiseWeight mu row) mu ⋯ row) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseTensorRelativeCompression.gtTransversePositiveSector_relativeCasimir_adjoint_compression {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu nu : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hmu : mu = HigherChannel.raiseWeight nu row) (hnu : HigherRepresentationGraph.Interlaces lam nu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam nu hnu) (p : ↥(HarmonicYoungSpace mu)) : (LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseTensorEmbedding✝ lam nu hnu hgram).toLinearMap) ((AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam) ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransversePositiveSector✝ lam mu nu row hmu hnu hgram) p)) = HigherYoungAllRankGTArrowheadSchurComplement.gtStabilizerArrowheadNode (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) mu) (Sum.inr (row, true)) • (youngClebschLower nu mu ⋯ row) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWignerEckartPhase.gtTransverseNegativeSector_inner {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (kappa : Fin r → ℕ) (row : Fin (r + 1)) (hnu : HigherRepresentationGraph.Interlaces lam (HigherChannel.raiseWeight mu row)) (hnuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam (HigherChannel.raiseWeight mu row) hnu) (hfinite : HigherChannel.FiniteInterlacing n mu kappa) (hraise : HigherChannel.FiniteInterlacing n (HigherChannel.raiseWeight mu row) kappa) (p q : ↥(HarmonicYoungSpace mu)) : inner ℝ ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseNegativeSector✝ lam mu row hnu hnuGram) p) ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseNegativeSector✝ lam mu row hnu hnuGram) q) = ArbitraryRankInternalRowLowerGram.internalRowLowerGramScalar (HigherChannel.raiseWeight mu row) row * HigherChannel.weylEdgeRatio n mu row * inner ℝ p q

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWignerEckartPhase.gtTransverseNegativeSector_gram_pos {r n : ℕ} (mu : Fin (r + 1) → ℕ) (kappa : Fin r → ℕ) (row : Fin (r + 1)) (hfinite : HigherChannel.FiniteInterlacing n mu kappa) (hraise : HigherChannel.FiniteInterlacing n (HigherChannel.raiseWeight mu row) kappa) : 0 < ArbitraryRankInternalRowLowerGram.internalRowLowerGramScalar (HigherChannel.raiseWeight mu row) row * HigherChannel.weylEdgeRatio n mu row

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWignerEckartPhase.normalizedGTTransverseNegativeSector_toLinearMap {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (kappa : Fin r → ℕ) (row : Fin (r + 1)) (hnu : HigherRepresentationGraph.Interlaces lam (HigherChannel.raiseWeight mu row)) (hnuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam (HigherChannel.raiseWeight mu row) hnu) (hfinite : HigherChannel.FiniteInterlacing n mu kappa) (hraise : HigherChannel.FiniteInterlacing n (HigherChannel.raiseWeight mu row) kappa) : (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWignerEckartPhase.normalizedGTTransverseNegativeSector✝ lam mu kappa row hnu hnuGram hfinite hraise).toLinearMap = (√(ArbitraryRankInternalRowLowerGram.internalRowLowerGramScalar (HigherChannel.raiseWeight mu row) row * HigherChannel.weylEdgeRatio n mu row))⁻¹ • MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseNegativeSector✝ lam mu row hnu hnuGram

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWignerEckartPhase.gtTransversePositiveSector_inner {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu nu : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hmunu : mu = HigherChannel.raiseWeight nu row) (hmu : HigherRepresentationGraph.Interlaces lam mu) (hnu : HigherRepresentationGraph.Interlaces lam nu) (hnuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam nu hnu) (p q : ↥(HarmonicYoungSpace mu)) : inner ℝ ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransversePositiveSector✝ lam mu nu row hmunu hnu hnuGram) p) ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransversePositiveSector✝ lam mu nu row hmunu hnu hnuGram) q) = ArbitraryRankInternalRowLowerGram.internalRowLowerGramScalar mu row * inner ℝ p q

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWignerEckartPhase.gtTransversePositiveSector_gram_pos {r : ℕ} (nu : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hdominant : Antitone nu) : 0 < ArbitraryRankInternalRowLowerGram.internalRowLowerGramScalar (HigherChannel.raiseWeight nu row) row

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWignerEckartPhase.normalizedGTTransversePositiveSector_toLinearMap {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu nu : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hmunu : mu = HigherChannel.raiseWeight nu row) (hmu : HigherRepresentationGraph.Interlaces lam mu) (hnu : HigherRepresentationGraph.Interlaces lam nu) (hnuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam nu hnu) : (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWignerEckartPhase.normalizedGTTransversePositiveSector✝ lam mu nu row hmunu hmu hnu hnuGram).toLinearMap = (√(ArbitraryRankInternalRowLowerGram.internalRowLowerGramScalar mu row))⁻¹ • MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransversePositiveSector✝ lam mu nu row hmunu hnu hnuGram

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTNormalizedTransverseSector.isometric_scaled_sector_adjoint_compression {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [NormedAddCommGroup Y] [InnerProductSpace ℝ Y] [NormedAddCommGroup Z] [InnerProductSpace ℝ Z] [FiniteDimensional ℝ X] [FiniteDimensional ℝ Y] [FiniteDimensional ℝ Z] (I : X →ₗᵢ[ℝ] Y) (C : Z →ₗ[ℝ] X) (B : Z →ₗᵢ[ℝ] Y) (T : Module.End ℝ Y) (phase node : ℝ) (hphase : B.toLinearMap = phase • I.toLinearMap ∘ₗ C) (hnode : ∀ (p : Z), (LinearMap.adjoint I.toLinearMap) (T (I (C p))) = node • C p) : LinearMap.adjoint B.toLinearMap ∘ₗ T ∘ₗ B.toLinearMap = node • LinearMap.id

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTNormalizedTransverseSector.normalizedGTTransverseNegativeSector_relativeCasimir_adjoint_compression {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (kappa : Fin r → ℕ) (row : Fin (r + 1)) (hnu : HigherRepresentationGraph.Interlaces lam (HigherChannel.raiseWeight mu row)) (hnuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam (HigherChannel.raiseWeight mu row) hnu) (hfinite : HigherChannel.FiniteInterlacing n mu kappa) (hraise : HigherChannel.FiniteInterlacing n (HigherChannel.raiseWeight mu row) kappa) : LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWignerEckartPhase.normalizedGTTransverseNegativeSector✝ lam mu kappa row hnu hnuGram hfinite hraise).toLinearMap ∘ₗ AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWignerEckartPhase.normalizedGTTransverseNegativeSector✝ lam mu kappa row hnu hnuGram hfinite hraise).toLinearMap = HigherYoungAllRankGTArrowheadSchurComplement.gtStabilizerArrowheadNode (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) mu) (Sum.inr (row, false)) • LinearMap.id

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTNormalizedTransverseSector.normalizedGTTransversePositiveSector_relativeCasimir_adjoint_compression {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu nu : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hmunu : mu = HigherChannel.raiseWeight nu row) (hmu : HigherRepresentationGraph.Interlaces lam mu) (hnu : HigherRepresentationGraph.Interlaces lam nu) (hnuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam nu hnu) : LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWignerEckartPhase.normalizedGTTransversePositiveSector✝ lam mu nu row hmunu hmu hnu hnuGram).toLinearMap ∘ₗ AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWignerEckartPhase.normalizedGTTransversePositiveSector✝ lam mu nu row hmunu hmu hnu hnuGram).toLinearMap = HigherYoungAllRankGTArrowheadSchurComplement.gtStabilizerArrowheadNode (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) mu) (Sum.inr (row, true)) • LinearMap.id

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTNormalizedTransverseRotationIntertwining.gtTransverseTensorEmbedding_rotation_intertwine {r n : ℕ} (lam : Fin (r + 2) → ℕ) (nu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam nu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam nu h) (a b : Fin n) : (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseTensorEmbedding✝ lam nu h hgram).toLinearMap ∘ₗ ClebschRotation.tensorAmbientRotation nu a b = ClebschRotation.tensorAmbientRotation lam a.castSucc b.castSucc ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseTensorEmbedding✝ lam nu h hgram).toLinearMap

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTNormalizedTransverseRotationIntertwining.gtTransverseNegativeSector_rotation_intertwine {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hnu : HigherRepresentationGraph.Interlaces lam (HigherChannel.raiseWeight mu row)) (hnuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam (HigherChannel.raiseWeight mu row) hnu) (a b : Fin n) : MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseNegativeSector✝ lam mu row hnu hnuGram ∘ₗ MixedSignature.youngAmbientRotation mu a b = ClebschRotation.tensorAmbientRotation lam a.castSucc b.castSucc ∘ₗ MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseNegativeSector✝ lam mu row hnu hnuGram

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTNormalizedTransverseRotationIntertwining.gtTransversePositiveSector_rotation_intertwine {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu nu : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hmu : mu = HigherChannel.raiseWeight nu row) (hnu : HigherRepresentationGraph.Interlaces lam nu) (hnuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam nu hnu) (a b : Fin n) : MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransversePositiveSector✝ lam mu nu row hmu hnu hnuGram ∘ₗ MixedSignature.youngAmbientRotation mu a b = ClebschRotation.tensorAmbientRotation lam a.castSucc b.castSucc ∘ₗ MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransversePositiveSector✝ lam mu nu row hmu hnu hnuGram

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTNormalizedTransverseRotationIntertwining.normalizedGTTransverseNegativeSector_rotation_intertwine {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (kappa : Fin r → ℕ) (row : Fin (r + 1)) (hnu : HigherRepresentationGraph.Interlaces lam (HigherChannel.raiseWeight mu row)) (hnuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam (HigherChannel.raiseWeight mu row) hnu) (hfinite : HigherChannel.FiniteInterlacing n mu kappa) (hraise : HigherChannel.FiniteInterlacing n (HigherChannel.raiseWeight mu row) kappa) (a b : Fin n) : (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWignerEckartPhase.normalizedGTTransverseNegativeSector✝ lam mu kappa row hnu hnuGram hfinite hraise).toLinearMap ∘ₗ MixedSignature.youngAmbientRotation mu a b = ClebschRotation.tensorAmbientRotation lam a.castSucc b.castSucc ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWignerEckartPhase.normalizedGTTransverseNegativeSector✝ lam mu kappa row hnu hnuGram hfinite hraise).toLinearMap

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTNormalizedTransverseRotationIntertwining.normalizedGTTransversePositiveSector_rotation_intertwine {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu nu : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hmunu : mu = HigherChannel.raiseWeight nu row) (hmu : HigherRepresentationGraph.Interlaces lam mu) (hnu : HigherRepresentationGraph.Interlaces lam nu) (hnuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam nu hnu) (a b : Fin n) : (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWignerEckartPhase.normalizedGTTransversePositiveSector✝ lam mu nu row hmunu hmu hnu hnuGram).toLinearMap ∘ₗ MixedSignature.youngAmbientRotation mu a b = ClebschRotation.tensorAmbientRotation lam a.castSucc b.castSucc ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWignerEckartPhase.normalizedGTTransversePositiveSector✝ lam mu nu row hmunu hmu hnu hnuGram).toLinearMap

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseAppendedChannelOrthogonality.paddedPhysicalStabilizerTensor_rotation_intertwine {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (B : ↥(HarmonicYoungSpace mu) →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean (n + 1)) ↥(HarmonicYoungSpace lam)) (hB : ∀ (a b : Fin n), B ∘ₗ MixedSignature.youngAmbientRotation mu a b = ClebschRotation.tensorAmbientRotation lam a.castSucc b.castSucc ∘ₗ B) (a b : Fin n) : MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseAppendedChannelOrthogonality.paddedPhysicalStabilizerTensor✝ lam mu B ∘ₗ MixedSignature.youngAmbientRotation (ThreeRowYoungBranching.appendZeroWeight (ThreeRowYoungBranching.appendZeroWeight mu)) a b = ClebschRotation.tensorAmbientRotation (ThreeRowYoungBranching.appendZeroWeight lam) a.castSucc b.castSucc ∘ₗ MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseAppendedChannelOrthogonality.paddedPhysicalStabilizerTensor✝ lam mu B

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseAppendedChannelOrthogonality.appendedFullBranchPieriLower_adjoint_paddedPhysicalStabilizerTensor_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (hmu : Antitone mu) (B : ↥(HarmonicYoungSpace mu) →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean (n + 1)) ↥(HarmonicYoungSpace lam)) (hB : ∀ (a b : Fin n), B ∘ₗ MixedSignature.youngAmbientRotation mu a b = ClebschRotation.tensorAmbientRotation lam a.castSucc b.castSucc ∘ₗ B) (hdominant : Antitone (ThreeRowYoungBranching.appendZeroWeight lam)) (hsource : Antitone (HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight lam) (Fin.last (r + 2)))) (hn : 2 * (r + 2) + 5 ≤ n + 1) (nu : BranchingDimension.FullBranchWeight (HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight lam) (Fin.last (r + 2)))) : LinearMap.adjoint (AllRankGTAppendedClebschOrthogonality.appendedFullBranchPieriLower lam hdominant hsource hn nu) ∘ₗ MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseAppendedChannelOrthogonality.paddedPhysicalStabilizerTensor✝ lam mu B = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseAppendedChannelOrthogonality.appendedFullBranchPieriLower_paddedPhysicalStabilizerTensor_inner_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (hmu : Antitone mu) (B : ↥(HarmonicYoungSpace mu) →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean (n + 1)) ↥(HarmonicYoungSpace lam)) (hB : ∀ (a b : Fin n), B ∘ₗ MixedSignature.youngAmbientRotation mu a b = ClebschRotation.tensorAmbientRotation lam a.castSucc b.castSucc ∘ₗ B) (hdominant : Antitone (ThreeRowYoungBranching.appendZeroWeight lam)) (hsource : Antitone (HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight lam) (Fin.last (r + 2)))) (hn : 2 * (r + 2) + 5 ≤ n + 1) (nu : BranchingDimension.FullBranchWeight (HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight lam) (Fin.last (r + 2)))) (p : ↥(HarmonicYoungSpace (ThreeRowYoungBranching.appendZeroWeight (ThreeRowYoungBranching.appendZeroWeight mu)))) (q : ↥(HarmonicYoungSpace (BranchingDimension.fullBranchSignature nu))) : inner ℝ ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseAppendedChannelOrthogonality.paddedPhysicalStabilizerTensor✝ lam mu B) p) ((AllRankGTAppendedClebschOrthogonality.appendedFullBranchPieriLower lam hdominant hsource hn nu) q) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseAppendedChannelOrthogonality.appendedPaddedPieriLower_adjoint_paddedPhysicalStabilizerTensor_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (hmu : Antitone mu) (B : ↥(HarmonicYoungSpace mu) →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean (n + 1)) ↥(HarmonicYoungSpace lam)) (hB : ∀ (a b : Fin n), B ∘ₗ MixedSignature.youngAmbientRotation mu a b = ClebschRotation.tensorAmbientRotation lam a.castSucc b.castSucc ∘ₗ B) (hdominant : Antitone (ThreeRowYoungBranching.appendZeroWeight lam)) (hsource : Antitone (HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight lam) (Fin.last (r + 2)))) (hn : 2 * (r + 2) + 5 ≤ n + 1) : LinearMap.adjoint (AllRankPaddedLowerClebschIntertwining.normalizedPaddedPieriLower (ThreeRowYoungBranching.appendZeroWeight lam) hdominant (Fin.last (r + 2)) hsource).toLinearMap ∘ₗ MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseAppendedChannelOrthogonality.paddedPhysicalStabilizerTensor✝ lam mu B = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseAppendedChannelOrthogonality.paddedOrthogonalTensorPieriChannel_appended_stabilizerIntertwiner_orthogonal {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (hmu : Antitone mu) (B : ↥(HarmonicYoungSpace mu) →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean (n + 1)) ↥(HarmonicYoungSpace lam)) (hB : ∀ (a b : Fin n), B ∘ₗ MixedSignature.youngAmbientRotation mu a b = ClebschRotation.tensorAmbientRotation lam a.castSucc b.castSucc ∘ₗ B) (hdominant : Antitone (ThreeRowYoungBranching.appendZeroWeight lam)) (hsource : Antitone (HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight lam) (Fin.last (r + 2)))) (hn : 2 * (r + 2) + 5 ≤ n + 1) (p : ↥(HarmonicYoungSpace mu)) (q : ↥(HarmonicYoungSpace (HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight lam) (Fin.last (r + 2))))) : inner ℝ (B p) ((AllRankGTRelativeCasimirZeroRowTransport.zeroRowTransportPaddedPieriChannel lam (HigherYoungAllRankOrthogonalTensorPieriActualChannels.paddedOrthogonalTensorPieriChannel ⋯ (ThreeRowYoungBranching.appendZeroWeight lam) hdominant (Sum.inl ⟨Fin.last (r + 2), hsource⟩))) q) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseAppendedChannelOrthogonality.paddedOrthogonalTensorPieriChannel_appended_normalizedGTTransverseNegativeSector_orthogonal {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (kappa : Fin r → ℕ) (row : Fin (r + 1)) (hnu : HigherRepresentationGraph.Interlaces lam (HigherChannel.raiseWeight mu row)) (hnuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam (HigherChannel.raiseWeight mu row) hnu) (hfinite : HigherChannel.FiniteInterlacing n mu kappa) (hraise : HigherChannel.FiniteInterlacing n (HigherChannel.raiseWeight mu row) kappa) (hdominant : Antitone (ThreeRowYoungBranching.appendZeroWeight lam)) (hsource : Antitone (HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight lam) (Fin.last (r + 2)))) (hn : 2 * (r + 2) + 5 ≤ n + 1) (p : ↥(HarmonicYoungSpace mu)) (q : ↥(HarmonicYoungSpace (HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight lam) (Fin.last (r + 2))))) : inner ℝ ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWignerEckartPhase.normalizedGTTransverseNegativeSector✝ lam mu kappa row hnu hnuGram hfinite hraise) p) ((AllRankGTRelativeCasimirZeroRowTransport.zeroRowTransportPaddedPieriChannel lam (HigherYoungAllRankOrthogonalTensorPieriActualChannels.paddedOrthogonalTensorPieriChannel ⋯ (ThreeRowYoungBranching.appendZeroWeight lam) hdominant (Sum.inl ⟨Fin.last (r + 2), hsource⟩))) q) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseAppendedChannelOrthogonality.paddedOrthogonalTensorPieriChannel_appended_normalizedGTTransversePositiveSector_orthogonal {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu nu : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hmunu : mu = HigherChannel.raiseWeight nu row) (hmu : HigherRepresentationGraph.Interlaces lam mu) (hnu : HigherRepresentationGraph.Interlaces lam nu) (hnuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam nu hnu) (hdominant : Antitone (ThreeRowYoungBranching.appendZeroWeight lam)) (hsource : Antitone (HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight lam) (Fin.last (r + 2)))) (hn : 2 * (r + 2) + 5 ≤ n + 1) (p : ↥(HarmonicYoungSpace mu)) (q : ↥(HarmonicYoungSpace (HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight lam) (Fin.last (r + 2))))) : inner ℝ ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWignerEckartPhase.normalizedGTTransversePositiveSector✝ lam mu nu row hmunu hmu hnu hnuGram) p) ((AllRankGTRelativeCasimirZeroRowTransport.zeroRowTransportPaddedPieriChannel lam (HigherYoungAllRankOrthogonalTensorPieriActualChannels.paddedOrthogonalTensorPieriChannel ⋯ (ThreeRowYoungBranching.appendZeroWeight lam) hdominant (Sum.inl ⟨Fin.last (r + 2), hsource⟩))) q) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseSectorSignedSpan.gtSignedEigenvectorSpan_mem_of_appendedPhysicalPaddedPieriChannel_orthogonal {r n : ℕ} (hn : 2 * (r + 1) + 4 ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone (ThreeRowYoungBranching.appendZeroWeight lam)) (v : TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace lam)) (happended : ∀ (hsource : Antitone (HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight lam) (Fin.last (r + 1)))) (q : ↥(HarmonicYoungSpace (HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight lam) (Fin.last (r + 1))))), inner ℝ v ((AllRankGTTransportedPieriOrthogonality.physicalPaddedPieriChannel hn lam hdom (Sum.inl ⟨Fin.last (r + 1), hsource⟩)) q) = 0) : v ∈ AllRankGTCompressedResolventSpectral.gtSignedEigenvectorSpan lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseSectorSignedSpan.gtPhysicalStabilizerIntertwiner_mem_gtSignedEigenvectorSpan {r n : ℕ} (hn : 2 * (r + 2) + 5 ≤ n + 1) (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (hmu : Antitone mu) (B : ↥(HarmonicYoungSpace mu) →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean (n + 1)) ↥(HarmonicYoungSpace lam)) (hB : ∀ (a b : Fin n), B ∘ₗ MixedSignature.youngAmbientRotation mu a b = ClebschRotation.tensorAmbientRotation lam a.castSucc b.castSucc ∘ₗ B) (hdom : Antitone (ThreeRowYoungBranching.appendZeroWeight lam)) (p : ↥(HarmonicYoungSpace mu)) : B p ∈ AllRankGTCompressedResolventSpectral.gtSignedEigenvectorSpan lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTNormalizedTransverseCharacteristicAnnihilation.normalizedGTTransverseNegativeSector_mem_gtSignedEigenvectorSpan {r n : ℕ} (hn : 2 * (r + 2) + 5 ≤ n + 1) (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (kappa : Fin r → ℕ) (row : Fin (r + 1)) (hnu : HigherRepresentationGraph.Interlaces lam (HigherChannel.raiseWeight mu row)) (hnuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam (HigherChannel.raiseWeight mu row) hnu) (hfinite : HigherChannel.FiniteInterlacing n mu kappa) (hraise : HigherChannel.FiniteInterlacing n (HigherChannel.raiseWeight mu row) kappa) (p : ↥(HarmonicYoungSpace mu)) : (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWignerEckartPhase.normalizedGTTransverseNegativeSector✝ lam mu kappa row hnu hnuGram hfinite hraise) p ∈ AllRankGTCompressedResolventSpectral.gtSignedEigenvectorSpan lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTNormalizedTransverseCharacteristicAnnihilation.normalizedGTTransversePositiveSector_mem_gtSignedEigenvectorSpan {r n : ℕ} (hn : 2 * (r + 2) + 5 ≤ n + 1) (lam : Fin (r + 2) → ℕ) (mu nu : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hmunu : mu = HigherChannel.raiseWeight nu row) (hmu : HigherRepresentationGraph.Interlaces lam mu) (hnu : HigherRepresentationGraph.Interlaces lam nu) (hnuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam nu hnu) (p : ↥(HarmonicYoungSpace mu)) : (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWignerEckartPhase.normalizedGTTransversePositiveSector✝ lam mu nu row hmunu hmu hnu hnuGram) p ∈ AllRankGTCompressedResolventSpectral.gtSignedEigenvectorSpan lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTNormalizedTransverseCharacteristicAnnihilation.normalizedGTTransverseNegativeSector_characteristic_aeval_eq_zero {r n : ℕ} (hn : 2 * (r + 2) + 5 ≤ n + 1) (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (kappa : Fin r → ℕ) (row : Fin (r + 1)) (hnu : HigherRepresentationGraph.Interlaces lam (HigherChannel.raiseWeight mu row)) (hnuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam (HigherChannel.raiseWeight mu row) hnu) (hfinite : HigherChannel.FiniteInterlacing n mu kappa) (hraise : HigherChannel.FiniteInterlacing n (HigherChannel.raiseWeight mu row) kappa) (p : ↥(HarmonicYoungSpace mu)) : ((Polynomial.aeval (AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam)) (HigherYoungAllRankGTCharacteristicResidue.gtChannelCharacteristicPolynomial (n + 1) lam)) ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWignerEckartPhase.normalizedGTTransverseNegativeSector✝ lam mu kappa row hnu hnuGram hfinite hraise) p) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTNormalizedTransverseCharacteristicAnnihilation.normalizedGTTransversePositiveSector_characteristic_aeval_eq_zero {r n : ℕ} (hn : 2 * (r + 2) + 5 ≤ n + 1) (lam : Fin (r + 2) → ℕ) (mu nu : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hmunu : mu = HigherChannel.raiseWeight nu row) (hmu : HigherRepresentationGraph.Interlaces lam mu) (hnu : HigherRepresentationGraph.Interlaces lam nu) (hnuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam nu hnu) (p : ↥(HarmonicYoungSpace mu)) : ((Polynomial.aeval (AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam)) (HigherYoungAllRankGTCharacteristicResidue.gtChannelCharacteristicPolynomial (n + 1) lam)) ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWignerEckartPhase.normalizedGTTransversePositiveSector✝ lam mu nu row hmunu hmu hnu hnuGram) p) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.exists_fullBranchSignature_wall_of_last_pos {r : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hlast : 0 < lam (Fin.last (r + 1))) : ∃ (nu : BranchingDimension.FullBranchWeight lam), BranchingDimension.fullBranchSignature nu = HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight mu) (Fin.last (r + 1))

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtWallFullBranch_signature {r : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hlast : 0 < lam (Fin.last (r + 1))) : BranchingDimension.fullBranchSignature (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtWallFullBranch✝ lam mu h hlast) = HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight mu) (Fin.last (r + 1))

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallSectorGram.gtWallSectorGram {r : ℕ} (n : ℕ) (mu : Fin (r + 1) → ℕ) : ℝ

The gt wall sector gram used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallSectorGram.gtWallZeroRow_finiteInterlacing {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 1) + 5 ≤ n + 1) : HigherChannel.FiniteInterlacing n (ThreeRowYoungBranching.appendZeroWeight mu) mu

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallSectorGram.gtWallRaisedZeroRow_finiteInterlacing {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (hlast : 0 < lam (Fin.last (r + 1))) : HigherChannel.FiniteInterlacing n (HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight mu) (Fin.last (r + 1))) mu

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallSectorGram.gtWallSectorGram_pos {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (hlast : 0 < lam (Fin.last (r + 1))) : 0 < gtWallSectorGram n mu

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallSectorGram.gtTransverseWallSector_inner {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (hlast : 0 < lam (Fin.last (r + 1))) (p q : ↥(HarmonicYoungSpace mu)) : inner ℝ ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtTransverseWallSector✝ lam mu h hn hlast) p) ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtTransverseWallSector✝ lam mu h hn hlast) q) = gtWallSectorGram n mu * inner ℝ p q

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.stabilizerIsometry_rotation_adjoint_compression {s r n : ℕ} (lam : Fin (r + 1) → ℕ) (nu : Fin (s + 1) → ℕ) (F : ↥(HarmonicYoungSpace nu) →ₗᵢ[ℝ] ↥(HarmonicYoungSpace lam)) (hF : ∀ (a b : Fin n), F.toLinearMap ∘ₗ MixedSignature.youngAmbientRotation nu a b = MixedSignature.youngAmbientRotation lam a.castSucc b.castSucc ∘ₗ F.toLinearMap) (a b : Fin n) : LinearMap.adjoint F.toLinearMap ∘ₗ MixedSignature.youngAmbientRotation lam a.castSucc b.castSucc ∘ₗ F.toLinearMap = MixedSignature.youngAmbientRotation nu a b

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.transverseTensorEmbeddingOfStabilizerIsometry_rotationTerm {s r n : ℕ} (lam : Fin (r + 1) → ℕ) (nu : Fin (s + 1) → ℕ) (F : ↥(HarmonicYoungSpace nu) →ₗᵢ[ℝ] ↥(HarmonicYoungSpace lam)) (a b : Fin (n + 1)) : LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.transverseTensorEmbeddingOfStabilizerIsometry✝ lam nu F).toLinearMap ∘ₗ TensorProduct.map (ClebschRotation.euclideanAmbientRotation a b) (MixedSignature.youngAmbientRotation lam a b) ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.transverseTensorEmbeddingOfStabilizerIsometry✝ lam nu F).toLinearMap = TensorProduct.map (LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseEuclideanIsometry✝ n).toLinearMap ∘ₗ ClebschRotation.euclideanAmbientRotation a b ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseEuclideanIsometry✝ n).toLinearMap) (LinearMap.adjoint F.toLinearMap ∘ₗ MixedSignature.youngAmbientRotation lam a b ∘ₗ F.toLinearMap)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.transverseTensorEmbeddingOfStabilizerIsometry_mixedRotation {s r n : ℕ} (lam : Fin (r + 1) → ℕ) (nu : Fin (s + 1) → ℕ) (F : ↥(HarmonicYoungSpace nu) →ₗᵢ[ℝ] ↥(HarmonicYoungSpace lam)) (hF : ∀ (a b : Fin n), F.toLinearMap ∘ₗ MixedSignature.youngAmbientRotation nu a b = MixedSignature.youngAmbientRotation lam a.castSucc b.castSucc ∘ₗ F.toLinearMap) : LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.transverseTensorEmbeddingOfStabilizerIsometry✝ lam nu F).toLinearMap ∘ₗ AllRankGTRelativeCasimirPureAxis.gtMixedRotationOperator lam ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.transverseTensorEmbeddingOfStabilizerIsometry✝ lam nu F).toLinearMap = AllRankGTRelativeCasimirPureAxis.gtMixedRotationOperator nu

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.transverseTensorEmbeddingOfStabilizerIsometry_relativeCasimir {s r n : ℕ} (lam : Fin (r + 1) → ℕ) (nu : Fin (s + 1) → ℕ) (F : ↥(HarmonicYoungSpace nu) →ₗᵢ[ℝ] ↥(HarmonicYoungSpace lam)) (hF : ∀ (a b : Fin n), F.toLinearMap ∘ₗ MixedSignature.youngAmbientRotation nu a b = MixedSignature.youngAmbientRotation lam a.castSucc b.castSucc ∘ₗ F.toLinearMap) : LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.transverseTensorEmbeddingOfStabilizerIsometry✝ lam nu F).toLinearMap ∘ₗ AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.transverseTensorEmbeddingOfStabilizerIsometry✝ lam nu F).toLinearMap = MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTStabilizerCasimirShift.gtStabilizerShiftedRelativeCasimir✝ nu

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.stabilizerShift_appendZeroWeight_last_add_half_eq_wall {r n : ℕ} (mu : Fin (r + 1) → ℕ) : HigherChannel.stabilizerShift (n + 1) (ThreeRowYoungBranching.appendZeroWeight mu) (Fin.last (r + 1)) + 1 / 2 = HigherChannel.wallShift (n + 1) (r + 1)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtStabilizerShiftedRelativeCasimir_terminal_youngClebschRaise {r n : ℕ} (mu : Fin (r + 1) → ℕ) (p : ↥(HarmonicYoungSpace (ThreeRowYoungBranching.appendZeroWeight mu))) : (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTStabilizerCasimirShift.gtStabilizerShiftedRelativeCasimir✝ (HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight mu) (Fin.last (r + 1)))) ((youngClebschRaise (HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight mu) (Fin.last (r + 1))) (ThreeRowYoungBranching.appendZeroWeight mu) ⋯ (Fin.last (r + 1))) p) = -HigherChannel.wallShift (n + 1) (r + 1) • (youngClebschRaise (HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight mu) (Fin.last (r + 1))) (ThreeRowYoungBranching.appendZeroWeight mu) ⋯ (Fin.last (r + 1))) p

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtTransverseWallTensorEmbedding_tmul {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (hlast : 0 < lam (Fin.last (r + 1))) (v : SpherePacking.Euclidean n) (p : ↥(HarmonicYoungSpace (HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight mu) (Fin.last (r + 1))))) : (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtTransverseWallTensorEmbedding✝ lam mu h hn hlast) (v ⊗ₜ[ℝ] p) = (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseEuclideanIsometry✝ n) v ⊗ₜ[ℝ] (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtWallCanonicalFullBranchFibre✝ lam mu h hn hlast) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtTransverseWallTensorEmbedding_axis_inner_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (hlast : 0 < lam (Fin.last (r + 1))) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (x : TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace (HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight mu) (Fin.last (r + 1))))) (q : ↥(HarmonicYoungSpace mu)) : inner ℝ ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtTransverseWallTensorEmbedding✝ lam mu h hn hlast) x) ((AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor lam mu h hgram) q) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtTransverseWallSector_axis_inner_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (hlast : 0 < lam (Fin.last (r + 1))) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (p q : ↥(HarmonicYoungSpace mu)) : inner ℝ ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtTransverseWallSector✝ lam mu h hn hlast) p) ((AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor lam mu h hgram) q) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtWallCanonicalFullBranchFibre_rotation_intertwine {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (hlast : 0 < lam (Fin.last (r + 1))) (a b : Fin n) : (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtWallCanonicalFullBranchFibre✝ lam mu h hn hlast).toLinearMap ∘ₗ MixedSignature.youngAmbientRotation (HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight mu) (Fin.last (r + 1))) a b = MixedSignature.youngAmbientRotation lam a.castSucc b.castSucc ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtWallCanonicalFullBranchFibre✝ lam mu h hn hlast).toLinearMap

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtTransverseWallTensorEmbedding_relativeCasimir_compression {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (hlast : 0 < lam (Fin.last (r + 1))) : LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtTransverseWallTensorEmbedding✝ lam mu h hn hlast).toLinearMap ∘ₗ AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtTransverseWallTensorEmbedding✝ lam mu h hn hlast).toLinearMap = MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTStabilizerCasimirShift.gtStabilizerShiftedRelativeCasimir✝ (HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight mu) (Fin.last (r + 1)))

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtTransverseWallSector_relativeCasimir_compression {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (hlast : 0 < lam (Fin.last (r + 1))) (p : ↥(HarmonicYoungSpace mu)) : (LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtTransverseWallTensorEmbedding✝ lam mu h hn hlast).toLinearMap) ((AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam) ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtTransverseWallSector✝ lam mu h hn hlast) p)) = -HigherChannel.wallShift (n + 1) (r + 1) • (youngClebschRaise (HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight mu) (Fin.last (r + 1))) (ThreeRowYoungBranching.appendZeroWeight mu) ⋯ (Fin.last (r + 1))) ((ThreeRowYoungBranching.appendZeroRowIsometryEquiv mu) p)

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallSectorIsometry.normalizedGTTransverseWallSector_toLinearMap {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (hlast : 0 < lam (Fin.last (r + 1))) : (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallSectorIsometry.normalizedGTTransverseWallSector✝ lam mu h hn hlast).toLinearMap = (√(AllRankGTWallSectorGram.gtWallSectorGram n mu))⁻¹ • MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtTransverseWallSector✝ lam mu h hn hlast

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallSectorIsometry.normalizedGTTransverseWallSector_apply {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (hlast : 0 < lam (Fin.last (r + 1))) (p : ↥(HarmonicYoungSpace mu)) : (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallSectorIsometry.normalizedGTTransverseWallSector✝ lam mu h hn hlast) p = (√(AllRankGTWallSectorGram.gtWallSectorGram n mu))⁻¹ • (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtTransverseWallSector✝ lam mu h hn hlast) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallSectorIsometry.normalizedGTTransverseWallSector_axis_inner_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (hlast : 0 < lam (Fin.last (r + 1))) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (p q : ↥(HarmonicYoungSpace mu)) : inner ℝ ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallSectorIsometry.normalizedGTTransverseWallSector✝ lam mu h hn hlast) p) ((AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor lam mu h hgram) q) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallSectorIsometry.canonicalAxis_inner_normalizedGTTransverseWallSector_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (hlast : 0 < lam (Fin.last (r + 1))) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (p q : ↥(HarmonicYoungSpace mu)) : inner ℝ ((AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor lam mu h hgram) p) ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallSectorIsometry.normalizedGTTransverseWallSector✝ lam mu h hn hlast) q) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTNormalizedWallCharacteristicAnnihilation.normalizedGTTransverseWallSector_rotation_intertwine {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (hlast : 0 < lam (Fin.last (r + 1))) (a b : Fin n) : (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallSectorIsometry.normalizedGTTransverseWallSector✝ lam mu h hn hlast).toLinearMap ∘ₗ MixedSignature.youngAmbientRotation mu a b = ClebschRotation.tensorAmbientRotation lam a.castSucc b.castSucc ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallSectorIsometry.normalizedGTTransverseWallSector✝ lam mu h hn hlast).toLinearMap

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTNormalizedWallCharacteristicAnnihilation.normalizedGTTransverseWallSector_mem_gtSignedEigenvectorSpan {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (hstable : 2 * (r + 2) + 5 ≤ n + 1) (hlast : 0 < lam (Fin.last (r + 1))) (p : ↥(HarmonicYoungSpace mu)) : (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallSectorIsometry.normalizedGTTransverseWallSector✝ lam mu h hn hlast) p ∈ AllRankGTCompressedResolventSpectral.gtSignedEigenvectorSpan lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTNormalizedWallCharacteristicAnnihilation.normalizedGTTransverseWallSector_characteristic_aeval_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (hstable : 2 * (r + 2) + 5 ≤ n + 1) (hlast : 0 < lam (Fin.last (r + 1))) (p : ↥(HarmonicYoungSpace mu)) : ((Polynomial.aeval (AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam)) (HigherYoungAllRankGTCharacteristicResidue.gtChannelCharacteristicPolynomial (n + 1) lam)) ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallSectorIsometry.normalizedGTTransverseWallSector✝ lam mu h hn hlast) p) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTPresentWallSignedNodeSeparation.wallShift_lt_ambientShift_of_last_pos {r n : ℕ} {lam : Fin (r + 2) → ℕ} {mu : Fin (r + 1) → ℕ} (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (hlast : 0 < lam (Fin.last (r + 1))) (row : Fin (r + 2)) : HigherChannel.wallShift (n + 1) (r + 1) < HigherChannel.ambientShift (n + 1) lam row

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTPresentWallSignedNodeSeparation.presentWall_ne_signedAmbientNode {r n : ℕ} {lam : Fin (r + 2) → ℕ} {mu : Fin (r + 1) → ℕ} (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (hlast : 0 < lam (Fin.last (r + 1))) (z : Fin (r + 2) × Bool) : -HigherChannel.wallShift (n + 1) (r + 1) ≠ HigherChannel.signedNode (HigherChannel.ambientShift (n + 1) lam) z

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseInternalEmbedding_tmul {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hn : 2 * r + 5 ≤ n + 1) (mu : BranchingDimension.FullBranchWeight lam) (v : SpherePacking.Euclidean n) (p : ↥(HarmonicYoungSpace (BranchingDimension.fullBranchSignature mu))) : (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseInternalEmbedding✝ lam hn mu) (v ⊗ₜ[ℝ] p) = v ⊗ₜ[ℝ] (HigherYoungAllRankCanonicalGelfandTsetlinCompleteness.canonicalFullBranchFibre lam hn mu) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseInternalEmbedding_orthogonal {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hn : 2 * r + 5 ≤ n + 1) (mu nu : BranchingDimension.FullBranchWeight lam) (hne : mu ≠ nu) (x : TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace (BranchingDimension.fullBranchSignature mu))) (y : TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace (BranchingDimension.fullBranchSignature nu))) : inner ℝ ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseInternalEmbedding✝ lam hn mu) x) ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseInternalEmbedding✝ lam hn nu) y) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseInternalEmbedding_finrank_sum {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hn : 2 * r + 5 ≤ n + 1) (hdom : Antitone lam) : Module.finrank ℝ (TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace lam)) = ∑ mu : BranchingDimension.FullBranchWeight lam, Module.finrank ℝ (TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace (BranchingDimension.fullBranchSignature mu)))

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseInternalEmbedding_iSup_range_eq_top {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hn : 2 * r + 5 ≤ n + 1) (hdom : Antitone lam) : ⨆ (mu : BranchingDimension.FullBranchWeight lam), (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseInternalEmbedding✝ lam hn mu).range = ⊤

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseEmbedding_eq_comp {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hn : 2 * r + 5 ≤ n + 1) (mu : BranchingDimension.FullBranchWeight lam) : (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseEmbedding✝ lam hn mu).toLinearMap = (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseAmbientInclusion✝ lam).toLinearMap ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseInternalEmbedding✝ lam hn mu).toLinearMap

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseEmbedding_orthogonal {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hn : 2 * r + 5 ≤ n + 1) (mu nu : BranchingDimension.FullBranchWeight lam) (hne : mu ≠ nu) (x : TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace (BranchingDimension.fullBranchSignature mu))) (y : TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace (BranchingDimension.fullBranchSignature nu))) : inner ℝ ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseEmbedding✝ lam hn mu) x) ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseEmbedding✝ lam hn nu) y) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseEmbedding_iSup_range {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hn : 2 * r + 5 ≤ n + 1) (hdom : Antitone lam) : ⨆ (mu : BranchingDimension.FullBranchWeight lam), (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseEmbedding✝ lam hn mu).range = (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseAmbientInclusion✝ lam).range

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTActualAxisTransverseDecomposition.euclidean_eq_gtTransverse_add_last_axis {n : ℕ} (v : SpherePacking.Euclidean (n + 1)) : v = (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseEuclideanIsometry✝ n) (WithLp.toLp 2 fun (i : Fin n) => v.ofLp i.castSucc) + v.ofLp (Fin.last n) • (EuclideanSpace.basisFun (Fin (n + 1)) ℝ) (Fin.last n)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTActualAxisTransverseDecomposition.gtFullAxisAmbientInclusion_sup_transverse_range_eq_top {r n : ℕ} (lam : Fin (r + 1) → ℕ) : (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTActualAxisTransverseDecomposition.gtFullAxisAmbientInclusion✝ lam).range ⊔ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseAmbientInclusion✝ lam).range = ⊤

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTActualAxisTransverseDecomposition.gtFullAxisEmbedding_apply {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hn : 2 * r + 5 ≤ n + 1) (mu : BranchingDimension.FullBranchWeight lam) (p : ↥(HarmonicYoungSpace (BranchingDimension.fullBranchSignature mu))) : (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTActualAxisTransverseDecomposition.gtFullAxisEmbedding✝ lam hn mu) p = (EuclideanSpace.basisFun (Fin (n + 1)) ℝ) (Fin.last n) ⊗ₜ[ℝ] (HigherYoungAllRankCanonicalGelfandTsetlinCompleteness.canonicalFullBranchFibre lam hn mu) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTActualAxisTransverseDecomposition.gtFullAxisEmbedding_orthogonal {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hn : 2 * r + 5 ≤ n + 1) (mu nu : BranchingDimension.FullBranchWeight lam) (hne : mu ≠ nu) (p : ↥(HarmonicYoungSpace (BranchingDimension.fullBranchSignature mu))) (q : ↥(HarmonicYoungSpace (BranchingDimension.fullBranchSignature nu))) : inner ℝ ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTActualAxisTransverseDecomposition.gtFullAxisEmbedding✝ lam hn mu) p) ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTActualAxisTransverseDecomposition.gtFullAxisEmbedding✝ lam hn nu) q) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTActualAxisTransverseDecomposition.gtFullAxisEmbedding_inner_transverse_eq_zero {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hn : 2 * r + 5 ≤ n + 1) (mu nu : BranchingDimension.FullBranchWeight lam) (p : ↥(HarmonicYoungSpace (BranchingDimension.fullBranchSignature mu))) (x : TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace (BranchingDimension.fullBranchSignature nu))) : inner ℝ ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTActualAxisTransverseDecomposition.gtFullAxisEmbedding✝ lam hn mu) p) ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseEmbedding✝ lam hn nu) x) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTActualAxisTransverseDecomposition.gtFullAxisEmbedding_iSup_range {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hn : 2 * r + 5 ≤ n + 1) (hdom : Antitone lam) : ⨆ (mu : BranchingDimension.FullBranchWeight lam), (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTActualAxisTransverseDecomposition.gtFullAxisEmbedding✝ lam hn mu).range = (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTActualAxisTransverseDecomposition.gtFullAxisAmbientInclusion✝ lam).range

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTActualAxisTransverseDecomposition.gtFullAxisTransverse_iSup_range_eq_top {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hn : 2 * r + 5 ≤ n + 1) (hdom : Antitone lam) : (⨆ (mu : BranchingDimension.FullBranchWeight lam), (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTActualAxisTransverseDecomposition.gtFullAxisEmbedding✝ lam hn mu).range) ⊔ ⨆ (mu : BranchingDimension.FullBranchWeight lam), (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseEmbedding✝ lam hn mu).range = ⊤

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTPhysicalCompleteBlockReconstruction.inner_eq_zero_of_mem_iSup_range_of_adjoint_eq_zero {ι : Type u_1} {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] (E : ι → Type u_3) [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace ℝ (E i)] [∀ (i : ι), FiniteDimensional ℝ (E i)] (A : (i : ι) → E i →ₗ[ℝ] V) (y : V) (hzero : ∀ (i : ι), (LinearMap.adjoint (A i)) y = 0) (x : V) (hx : x ∈ ⨆ (i : ι), (A i).range) : inner ℝ x y = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTPhysicalCompleteBlockReconstruction.eq_zero_of_iSup_range_sup_eq_top_of_adjoint_eq_zero {ι : Type u_1} {κ : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] (E : ι → Type u_4) (F : κ → Type u_5) [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace ℝ (E i)] [∀ (i : ι), FiniteDimensional ℝ (E i)] [(j : κ) → NormedAddCommGroup (F j)] [(j : κ) → InnerProductSpace ℝ (F j)] [∀ (j : κ), FiniteDimensional ℝ (F j)] (A : (i : ι) → E i →ₗ[ℝ] V) (B : (j : κ) → F j →ₗ[ℝ] V) (hcomplete : (⨆ (i : ι), (A i).range) ⊔ ⨆ (j : κ), (B j).range = ⊤) (y : V) (haxis : ∀ (i : ι), (LinearMap.adjoint (A i)) y = 0) (htransverse : ∀ (j : κ), (LinearMap.adjoint (B j)) y = 0) : y = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTPhysicalCompleteBlockReconstruction.eq_of_iSup_range_sup_eq_top_of_adjoint_eq {ι : Type u_1} {κ : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] (E : ι → Type u_4) (F : κ → Type u_5) [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace ℝ (E i)] [∀ (i : ι), FiniteDimensional ℝ (E i)] [(j : κ) → NormedAddCommGroup (F j)] [(j : κ) → InnerProductSpace ℝ (F j)] [∀ (j : κ), FiniteDimensional ℝ (F j)] (A : (i : ι) → E i →ₗ[ℝ] V) (B : (j : κ) → F j →ₗ[ℝ] V) (hcomplete : (⨆ (i : ι), (A i).range) ⊔ ⨆ (j : κ), (B j).range = ⊤) (x y : V) (haxis : ∀ (i : ι), (LinearMap.adjoint (A i)) x = (LinearMap.adjoint (A i)) y) (htransverse : ∀ (j : κ), (LinearMap.adjoint (B j)) x = (LinearMap.adjoint (B j)) y) : x = y

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTPhysicalRetainedAdditiveColumn.linearMap_comp_eq_smul_add_of_complete_adjoint_block_rows {ι : Type u_1} {κ : Type u_2} {E : Type u_3} {F : Type u_4} {V : Type u_5} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] (X : ι → Type u_6) (Y : κ → Type u_7) [(i : ι) → NormedAddCommGroup (X i)] [(i : ι) → InnerProductSpace ℝ (X i)] [∀ (i : ι), FiniteDimensional ℝ (X i)] [(j : κ) → NormedAddCommGroup (Y j)] [(j : κ) → InnerProductSpace ℝ (Y j)] [∀ (j : κ), FiniteDimensional ℝ (Y j)] (C : (i : ι) → X i →ₗ[ℝ] V) (D : (j : κ) → Y j →ₗ[ℝ] V) (hcomplete : (⨆ (i : ι), (C i).range) ⊔ ⨆ (j : κ), (D j).range = ⊤) (T : Module.End ℝ V) (B : E →ₗ[ℝ] V) (A : F →ₗ[ℝ] V) (K : E →ₗ[ℝ] F) (d : ℝ) (haxis : ∀ (i : ι), LinearMap.adjoint (C i) ∘ₗ T ∘ₗ B = d • LinearMap.adjoint (C i) ∘ₗ B + (LinearMap.adjoint (C i) ∘ₗ A) ∘ₗ K) (htransverse : ∀ (j : κ), LinearMap.adjoint (D j) ∘ₗ T ∘ₗ B = d • LinearMap.adjoint (D j) ∘ₗ B + (LinearMap.adjoint (D j) ∘ₗ A) ∘ₗ K) : T ∘ₗ B = d • B + A ∘ₗ K

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTPhysicalRetainedAdditiveColumn.gtRelativeCasimir_comp_eq_smul_add_of_full_axis_transverse_rows {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hn : 2 * r + 5 ≤ n + 1) (hdom : Antitone lam) {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean (n + 1)) ↥(HarmonicYoungSpace lam)) (A : F →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean (n + 1)) ↥(HarmonicYoungSpace lam)) (K : E →ₗ[ℝ] F) (d : ℝ) (haxis : ∀ (mu : BranchingDimension.FullBranchWeight lam), LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTActualAxisTransverseDecomposition.gtFullAxisEmbedding✝ lam hn mu).toLinearMap ∘ₗ AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam ∘ₗ B = d • LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTActualAxisTransverseDecomposition.gtFullAxisEmbedding✝ lam hn mu).toLinearMap ∘ₗ B + (LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTActualAxisTransverseDecomposition.gtFullAxisEmbedding✝ lam hn mu).toLinearMap ∘ₗ A) ∘ₗ K) (htransverse : ∀ (mu : BranchingDimension.FullBranchWeight lam), LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseEmbedding✝ lam hn mu).toLinearMap ∘ₗ AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam ∘ₗ B = d • LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseEmbedding✝ lam hn mu).toLinearMap ∘ₗ B + (LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseEmbedding✝ lam hn mu).toLinearMap ∘ₗ A) ∘ₗ K) : AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam ∘ₗ B = d • B + A ∘ₗ K

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTPhysicalRetainedAdditiveColumn.gtRelativeCasimir_comp_eq_smul_add_of_orthogonal_full_block_rows {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hn : 2 * r + 5 ≤ n + 1) (hdom : Antitone lam) {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean (n + 1)) ↥(HarmonicYoungSpace lam)) (A : F →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean (n + 1)) ↥(HarmonicYoungSpace lam)) (K : E →ₗ[ℝ] F) (d : ℝ) (haxisOrth : ∀ (mu : BranchingDimension.FullBranchWeight lam), LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTActualAxisTransverseDecomposition.gtFullAxisEmbedding✝ lam hn mu).toLinearMap ∘ₗ B = 0) (htransverseOrth : ∀ (mu : BranchingDimension.FullBranchWeight lam), LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseEmbedding✝ lam hn mu).toLinearMap ∘ₗ A = 0) (haxis : ∀ (mu : BranchingDimension.FullBranchWeight lam), LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTActualAxisTransverseDecomposition.gtFullAxisEmbedding✝ lam hn mu).toLinearMap ∘ₗ AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam ∘ₗ B = (LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTActualAxisTransverseDecomposition.gtFullAxisEmbedding✝ lam hn mu).toLinearMap ∘ₗ A) ∘ₗ K) (htransverse : ∀ (mu : BranchingDimension.FullBranchWeight lam), LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseEmbedding✝ lam hn mu).toLinearMap ∘ₗ AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam ∘ₗ B = d • LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseEmbedding✝ lam hn mu).toLinearMap ∘ₗ B) : AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam ∘ₗ B = d • B + A ∘ₗ K

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTPhysicalPaddedPieriFullEigen.physicalPaddedPieriChannel_relativeCasimir {r n : ℕ} (hn : 2 * (r + 1) + 4 ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone (ThreeRowYoungBranching.appendZeroWeight lam)) (i : HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.PaddedPieriChannel (ThreeRowYoungBranching.appendZeroWeight lam)) (p : ↥(HarmonicYoungSpace (HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.paddedPieriSource (ThreeRowYoungBranching.appendZeroWeight lam) i))) : (AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam) ((AllRankGTTransportedPieriOrthogonality.physicalPaddedPieriChannel hn lam hdom i) p) = HigherChannel.signedNode (HigherChannel.ambientShift n (ThreeRowYoungBranching.appendZeroWeight lam)) (AllRankGTInvalidNonterminalProjectorVanishing.paddedPieriSignedChannel (ThreeRowYoungBranching.appendZeroWeight lam) i) • (AllRankGTTransportedPieriOrthogonality.physicalPaddedPieriChannel hn lam hdom i) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTSelectedMuAxisProjectionVanishing.physicalPaddedPieriChannel_rotation_intertwine {r n : ℕ} (hn : 2 * (r + 1) + 4 ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone (ThreeRowYoungBranching.appendZeroWeight lam)) (i : HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.PaddedPieriChannel (ThreeRowYoungBranching.appendZeroWeight lam)) (a b : Fin n) : (AllRankGTTransportedPieriOrthogonality.physicalPaddedPieriChannel hn lam hdom i).toLinearMap ∘ₗ MixedSignature.youngAmbientRotation (HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.paddedPieriSource (ThreeRowYoungBranching.appendZeroWeight lam) i) a b = ClebschRotation.tensorAmbientRotation lam a b ∘ₗ (AllRankGTTransportedPieriOrthogonality.physicalPaddedPieriChannel hn lam hdom i).toLinearMap

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTSelectedMuAxisProjectionVanishing.gtRelativeCasimir_tensorAmbientRotation_commute {r n : ℕ} (hn : 2 * (r + 1) + 4 ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone (ThreeRowYoungBranching.appendZeroWeight lam)) (a b : Fin n) : AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam ∘ₗ ClebschRotation.tensorAmbientRotation lam a b = ClebschRotation.tensorAmbientRotation lam a b ∘ₗ AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTSelectedMuAxisProjectionVanishing.gtFullAxisEmbedding_rotation_intertwine {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hn : 2 * r + 5 ≤ n + 1) (nu : BranchingDimension.FullBranchWeight lam) (a b : Fin n) : (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTActualAxisTransverseDecomposition.gtFullAxisEmbedding✝ lam hn nu).toLinearMap ∘ₗ MixedSignature.youngAmbientRotation (BranchingDimension.fullBranchSignature nu) a b = ClebschRotation.tensorAmbientRotation lam a.castSucc b.castSucc ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTActualAxisTransverseDecomposition.gtFullAxisEmbedding✝ lam hn nu).toLinearMap

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTSelectedMuAxisProjectionVanishing.gtFullAxisEmbedding_selected_range_eq_canonicalAxis {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (hmu : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu hmu) : (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTActualAxisTransverseDecomposition.gtFullAxisEmbedding✝ lam hn (BranchingDimension.fullBranchOfInterlaces mu hmu)).range = (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTValidTransverseArrowheadRow.canonicalGelfandTsetlinAxisIsometry✝ lam mu hmu hgram).range

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTSelectedMuAxisProjectionVanishing.gtFullAxisEmbedding_adjoint_relativeCasimir_stabilizerSector_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (hmu : HigherRepresentationGraph.Interlaces lam mu) (hstable : 2 * (r + 2) + 5 ≤ n + 1) (nu : BranchingDimension.FullBranchWeight lam) (hne : BranchingDimension.fullBranchSignature nu ≠ ThreeRowYoungBranching.appendZeroWeight mu) (B : ↥(HarmonicYoungSpace mu) →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean (n + 1)) ↥(HarmonicYoungSpace lam)) (hB : ∀ (a b : Fin n), B ∘ₗ MixedSignature.youngAmbientRotation mu a b = ClebschRotation.tensorAmbientRotation lam a.castSucc b.castSucc ∘ₗ B) (p : ↥(HarmonicYoungSpace mu)) : (LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTActualAxisTransverseDecomposition.gtFullAxisEmbedding✝ lam ⋯ nu).toLinearMap) ((AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam) (B p)) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTFullTransverseSameSignatureRow.tensor_mapIsometry_range_eq_of_second_range_eq {E : Type u_1} {F : Type u_2} {X : Type u_3} {Y : Type u_4} {Z : Type u_5} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [NormedAddCommGroup X] [InnerProductSpace ℝ X] [NormedAddCommGroup Y] [InnerProductSpace ℝ Y] [NormedAddCommGroup Z] [InnerProductSpace ℝ Z] (e : E →ₗᵢ[ℝ] F) (g : X →ₗᵢ[ℝ] Z) (h : Y →ₗᵢ[ℝ] Z) (heq : g.range = h.range) : (TensorProduct.mapIsometry e g).range = (TensorProduct.mapIsometry e h).range

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTFullTransverseSameSignatureRow.adjoint_eigen_of_range_le {X : Type u_1} {Y : Type u_2} {H : Type u_3} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [FiniteDimensional ℝ X] [NormedAddCommGroup Y] [InnerProductSpace ℝ Y] [FiniteDimensional ℝ Y] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [FiniteDimensional ℝ H] (I : X →ₗ[ℝ] H) (J : Y →ₗ[ℝ] H) (hrange : J.range ≤ I.range) (T : Module.End ℝ H) (x : H) (d : ℝ) (hI : (LinearMap.adjoint I) (T x) = d • (LinearMap.adjoint I) x) : (LinearMap.adjoint J) (T x) = d • (LinearMap.adjoint J) x

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTFullTransverseSameSignatureRow.gtTransverseTensorEmbedding_range_eq_selectedFull {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (hdom : Antitone lam) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) : (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseTensorEmbedding✝ lam mu h hgram).range = (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseEmbedding✝ lam hn (BranchingDimension.fullBranchOfInterlaces mu h)).range

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTFullTransverseSameSignatureRow.negativeSector_shortTensor_adjoint_eigen {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (kappa : Fin r → ℕ) (row : Fin (r + 1)) (hnu : HigherRepresentationGraph.Interlaces lam (HigherChannel.raiseWeight mu row)) (hnuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam (HigherChannel.raiseWeight mu row) hnu) (hfinite : HigherChannel.FiniteInterlacing n mu kappa) (hraise : HigherChannel.FiniteInterlacing n (HigherChannel.raiseWeight mu row) kappa) (p : ↥(HarmonicYoungSpace mu)) : have I := MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseTensorEmbedding✝ lam (HigherChannel.raiseWeight mu row) hnu hnuGram; have B := MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWignerEckartPhase.normalizedGTTransverseNegativeSector✝ lam mu kappa row hnu hnuGram hfinite hraise; have d := HigherYoungAllRankGTArrowheadSchurComplement.gtStabilizerArrowheadNode (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) mu) (Sum.inr (row, false)); (LinearMap.adjoint I.toLinearMap) ((AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam) (B p)) = d • (LinearMap.adjoint I.toLinearMap) (B p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTFullTransverseSameSignatureRow.negativeSector_selectedFullTensor_adjoint_eigen {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (kappa : Fin r → ℕ) (row : Fin (r + 1)) (hnu : HigherRepresentationGraph.Interlaces lam (HigherChannel.raiseWeight mu row)) (hnuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam (HigherChannel.raiseWeight mu row) hnu) (hfinite : HigherChannel.FiniteInterlacing n mu kappa) (hraise : HigherChannel.FiniteInterlacing n (HigherChannel.raiseWeight mu row) kappa) (hn : 2 * (r + 1) + 5 ≤ n + 1) (p : ↥(HarmonicYoungSpace mu)) : have J := MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseEmbedding✝ lam hn (BranchingDimension.fullBranchOfInterlaces (HigherChannel.raiseWeight mu row) hnu); have B := MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWignerEckartPhase.normalizedGTTransverseNegativeSector✝ lam mu kappa row hnu hnuGram hfinite hraise; have d := HigherYoungAllRankGTArrowheadSchurComplement.gtStabilizerArrowheadNode (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) mu) (Sum.inr (row, false)); (LinearMap.adjoint J.toLinearMap) ((AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam) (B p)) = d • (LinearMap.adjoint J.toLinearMap) (B p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTFullTransverseSameSignatureRow.positiveSector_shortTensor_adjoint_eigen {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu nu : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hmunu : mu = HigherChannel.raiseWeight nu row) (hmu : HigherRepresentationGraph.Interlaces lam mu) (hnu : HigherRepresentationGraph.Interlaces lam nu) (hnuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam nu hnu) (p : ↥(HarmonicYoungSpace mu)) : have I := MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseTensorEmbedding✝ lam nu hnu hnuGram; have B := MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWignerEckartPhase.normalizedGTTransversePositiveSector✝ lam mu nu row hmunu hmu hnu hnuGram; have d := HigherYoungAllRankGTArrowheadSchurComplement.gtStabilizerArrowheadNode (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) mu) (Sum.inr (row, true)); (LinearMap.adjoint I.toLinearMap) ((AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam) (B p)) = d • (LinearMap.adjoint I.toLinearMap) (B p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTFullTransverseSameSignatureRow.positiveSector_selectedFullTensor_adjoint_eigen {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu nu : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hmunu : mu = HigherChannel.raiseWeight nu row) (hmu : HigherRepresentationGraph.Interlaces lam mu) (hnu : HigherRepresentationGraph.Interlaces lam nu) (hnuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam nu hnu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (p : ↥(HarmonicYoungSpace mu)) : have J := MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseEmbedding✝ lam hn (BranchingDimension.fullBranchOfInterlaces nu hnu); have B := MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWignerEckartPhase.normalizedGTTransversePositiveSector✝ lam mu nu row hmunu hmu hnu hnuGram; have d := HigherYoungAllRankGTArrowheadSchurComplement.gtStabilizerArrowheadNode (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) mu) (Sum.inr (row, true)); (LinearMap.adjoint J.toLinearMap) ((AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam) (B p)) = d • (LinearMap.adjoint J.toLinearMap) (B p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallFullTransverseFactorization.gtWallCanonicalFullBranchFibre_range_eq_fullBranch {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (hlast : 0 < lam (Fin.last (r + 1))) : (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtWallCanonicalFullBranchFibre✝ lam mu h hn hlast).range = (HigherYoungAllRankCanonicalGelfandTsetlinCompleteness.canonicalFullBranchFibre lam hn (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtWallFullBranch✝ lam mu h hlast)).range

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallFullTransverseFactorization.gtTransverseWallTensorEmbedding_range_eq_fullTransverse {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (hlast : 0 < lam (Fin.last (r + 1))) : (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtTransverseWallTensorEmbedding✝ lam mu h hn hlast).range = (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseEmbedding✝ lam hn (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtWallFullBranch✝ lam mu h hlast)).range

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallFullTransverseFactorization.normalizedGTTransverseWallSector_range_le_fullTransverse {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (hlast : 0 < lam (Fin.last (r + 1))) : (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallSectorIsometry.normalizedGTTransverseWallSector✝ lam mu h hn hlast).range ≤ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseEmbedding✝ lam hn (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtWallFullBranch✝ lam mu h hlast)).range

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransversePhysicalDiagonalColumn.normalizedWallSector_shortTensor_adjoint_eigen {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (hlast : 0 < lam (Fin.last (r + 1))) (p : ↥(HarmonicYoungSpace mu)) : have I := MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtTransverseWallTensorEmbedding✝ lam mu h hn hlast; have B := MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallSectorIsometry.normalizedGTTransverseWallSector✝ lam mu h hn hlast; have d := -HigherChannel.wallShift (n + 1) (r + 1); (LinearMap.adjoint I.toLinearMap) ((AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam) (B p)) = d • (LinearMap.adjoint I.toLinearMap) (B p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransversePhysicalDiagonalColumn.normalizedWallSector_selectedFullTensor_adjoint_eigen {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (hlast : 0 < lam (Fin.last (r + 1))) (p : ↥(HarmonicYoungSpace mu)) : have J := MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseEmbedding✝ lam hn (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtWallFullBranch✝ lam mu h hlast); have B := MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallSectorIsometry.normalizedGTTransverseWallSector✝ lam mu h hn hlast; have d := -HigherChannel.wallShift (n + 1) (r + 1); (LinearMap.adjoint J.toLinearMap) ((AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam) (B p)) = d • (LinearMap.adjoint J.toLinearMap) (B p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWrongBranchCompression.transverseStabilizerIsometry_adjoint_comp_of_orthogonal {s t r n : ℕ} (lam : Fin (r + 1) → ℕ) (source : Fin (s + 1) → ℕ) (target : Fin (t + 1) → ℕ) (F : ↥(HarmonicYoungSpace source) →ₗᵢ[ℝ] ↥(HarmonicYoungSpace lam)) (G : ↥(HarmonicYoungSpace target) →ₗᵢ[ℝ] ↥(HarmonicYoungSpace lam)) (horth : LinearMap.adjoint F.toLinearMap ∘ₗ G.toLinearMap = 0) : LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.transverseTensorEmbeddingOfStabilizerIsometry✝ lam source F).toLinearMap ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.transverseTensorEmbeddingOfStabilizerIsometry✝ lam target G).toLinearMap = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWrongBranchCompression.transverseStabilizerIsometry_rotationTerm_cross {s t r n : ℕ} (lam : Fin (r + 1) → ℕ) (source : Fin (s + 1) → ℕ) (target : Fin (t + 1) → ℕ) (F : ↥(HarmonicYoungSpace source) →ₗᵢ[ℝ] ↥(HarmonicYoungSpace lam)) (G : ↥(HarmonicYoungSpace target) →ₗᵢ[ℝ] ↥(HarmonicYoungSpace lam)) (a b : Fin (n + 1)) : LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.transverseTensorEmbeddingOfStabilizerIsometry✝ lam source F).toLinearMap ∘ₗ TensorProduct.map (ClebschRotation.euclideanAmbientRotation a b) (MixedSignature.youngAmbientRotation lam a b) ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.transverseTensorEmbeddingOfStabilizerIsometry✝ lam target G).toLinearMap = TensorProduct.map (LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseEuclideanIsometry✝ n).toLinearMap ∘ₗ ClebschRotation.euclideanAmbientRotation a b ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseEuclideanIsometry✝ n).toLinearMap) (LinearMap.adjoint F.toLinearMap ∘ₗ MixedSignature.youngAmbientRotation lam a b ∘ₗ G.toLinearMap)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWrongBranchCompression.transverseStabilizerIsometry_mixedRotation_cross_eq_zero {s t r n : ℕ} (lam : Fin (r + 1) → ℕ) (source : Fin (s + 1) → ℕ) (target : Fin (t + 1) → ℕ) (F : ↥(HarmonicYoungSpace source) →ₗᵢ[ℝ] ↥(HarmonicYoungSpace lam)) (G : ↥(HarmonicYoungSpace target) →ₗᵢ[ℝ] ↥(HarmonicYoungSpace lam)) (horth : LinearMap.adjoint F.toLinearMap ∘ₗ G.toLinearMap = 0) (hG : ∀ (a b : Fin n), G.toLinearMap ∘ₗ MixedSignature.youngAmbientRotation target a b = MixedSignature.youngAmbientRotation lam a.castSucc b.castSucc ∘ₗ G.toLinearMap) : LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.transverseTensorEmbeddingOfStabilizerIsometry✝ lam source F).toLinearMap ∘ₗ AllRankGTRelativeCasimirPureAxis.gtMixedRotationOperator lam ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.transverseTensorEmbeddingOfStabilizerIsometry✝ lam target G).toLinearMap = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWrongBranchCompression.transverseStabilizerIsometry_relativeCasimir_cross_eq_zero {s t r n : ℕ} (lam : Fin (r + 1) → ℕ) (source : Fin (s + 1) → ℕ) (target : Fin (t + 1) → ℕ) (F : ↥(HarmonicYoungSpace source) →ₗᵢ[ℝ] ↥(HarmonicYoungSpace lam)) (G : ↥(HarmonicYoungSpace target) →ₗᵢ[ℝ] ↥(HarmonicYoungSpace lam)) (horth : LinearMap.adjoint F.toLinearMap ∘ₗ G.toLinearMap = 0) (hG : ∀ (a b : Fin n), G.toLinearMap ∘ₗ MixedSignature.youngAmbientRotation target a b = MixedSignature.youngAmbientRotation lam a.castSucc b.castSucc ∘ₗ G.toLinearMap) : LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.transverseTensorEmbeddingOfStabilizerIsometry✝ lam source F).toLinearMap ∘ₗ AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.transverseTensorEmbeddingOfStabilizerIsometry✝ lam target G).toLinearMap = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWrongBranchCompression.canonicalFullBranchFibre_adjoint_comp_of_ne {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hn : 2 * r + 5 ≤ n + 1) (branch selected : BranchingDimension.FullBranchWeight lam) (hne : branch ≠ selected) : LinearMap.adjoint (HigherYoungAllRankCanonicalGelfandTsetlinCompleteness.canonicalFullBranchFibre lam hn branch).toLinearMap ∘ₗ (HigherYoungAllRankCanonicalGelfandTsetlinCompleteness.canonicalFullBranchFibre lam hn selected).toLinearMap = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWrongBranchCompression.canonicalFullBranchFibre_adjoint_canonicalGelfandTsetlinFibre_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (branch : BranchingDimension.FullBranchWeight lam) (hwrong : branch ≠ BranchingDimension.fullBranchOfInterlaces mu h) : LinearMap.adjoint (HigherYoungAllRankCanonicalGelfandTsetlinCompleteness.canonicalFullBranchFibre lam hn branch).toLinearMap ∘ₗ (AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFibre lam mu h hgram).toLinearMap = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWrongBranchCompression.gtFullTransverseEmbedding_relativeCasimir_cross_physical_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (branch : BranchingDimension.FullBranchWeight lam) (hwrong : branch ≠ BranchingDimension.fullBranchOfInterlaces mu h) : LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseEmbedding✝ lam hn branch).toLinearMap ∘ₗ AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseTensorEmbedding✝ lam mu h hgram).toLinearMap = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWrongBranchCompression.gtFullTransverseEmbedding_negativeRelativeCasimir_eq_zero_of_wrong_branch {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hnu : HigherRepresentationGraph.Interlaces lam (HigherChannel.raiseWeight mu row)) (hnuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam (HigherChannel.raiseWeight mu row) hnu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (branch : BranchingDimension.FullBranchWeight lam) (hwrong : branch ≠ BranchingDimension.fullBranchOfInterlaces (HigherChannel.raiseWeight mu row) hnu) (p : ↥(HarmonicYoungSpace mu)) : (LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseEmbedding✝ lam hn branch).toLinearMap) ((AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam) ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseNegativeSector✝ lam mu row hnu hnuGram) p)) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWrongBranchCompression.gtFullTransverseEmbedding_positiveRelativeCasimir_eq_zero_of_wrong_branch {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu nu : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hmunu : mu = HigherChannel.raiseWeight nu row) (hnu : HigherRepresentationGraph.Interlaces lam nu) (hnuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam nu hnu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (branch : BranchingDimension.FullBranchWeight lam) (hwrong : branch ≠ BranchingDimension.fullBranchOfInterlaces nu hnu) (p : ↥(HarmonicYoungSpace mu)) : (LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseEmbedding✝ lam hn branch).toLinearMap) ((AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam) ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransversePositiveSector✝ lam mu nu row hmunu hnu hnuGram) p)) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWrongBranchCompression.gtFullTransverseEmbedding_normalizedNegativeRelativeCasimir_eq_zero_of_wrong_branch {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (kappa : Fin r → ℕ) (row : Fin (r + 1)) (hnu : HigherRepresentationGraph.Interlaces lam (HigherChannel.raiseWeight mu row)) (hnuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam (HigherChannel.raiseWeight mu row) hnu) (hfinite : HigherChannel.FiniteInterlacing n mu kappa) (hraise : HigherChannel.FiniteInterlacing n (HigherChannel.raiseWeight mu row) kappa) (hn : 2 * (r + 1) + 5 ≤ n + 1) (branch : BranchingDimension.FullBranchWeight lam) (hwrong : branch ≠ BranchingDimension.fullBranchOfInterlaces (HigherChannel.raiseWeight mu row) hnu) (p : ↥(HarmonicYoungSpace mu)) : (LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseEmbedding✝ lam hn branch).toLinearMap) ((AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam) ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWignerEckartPhase.normalizedGTTransverseNegativeSector✝ lam mu kappa row hnu hnuGram hfinite hraise) p)) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWrongBranchCompression.gtFullTransverseEmbedding_normalizedPositiveRelativeCasimir_eq_zero_of_wrong_branch {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu nu : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hmunu : mu = HigherChannel.raiseWeight nu row) (hmu : HigherRepresentationGraph.Interlaces lam mu) (hnu : HigherRepresentationGraph.Interlaces lam nu) (hnuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam nu hnu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (branch : BranchingDimension.FullBranchWeight lam) (hwrong : branch ≠ BranchingDimension.fullBranchOfInterlaces nu hnu) (p : ↥(HarmonicYoungSpace mu)) : (LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseEmbedding✝ lam hn branch).toLinearMap) ((AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam) ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWignerEckartPhase.normalizedGTTransversePositiveSector✝ lam mu nu row hmunu hmu hnu hnuGram) p)) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCrossOrthogonality.canonicalFullBranchFibre_adjoint_wallCanonicalFullBranchFibre_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (hlast : 0 < lam (Fin.last (r + 1))) (branch : BranchingDimension.FullBranchWeight lam) (hwrong : branch ≠ MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtWallFullBranch✝ lam mu h hlast) : LinearMap.adjoint (HigherYoungAllRankCanonicalGelfandTsetlinCompleteness.canonicalFullBranchFibre lam hn branch).toLinearMap ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtWallCanonicalFullBranchFibre✝ lam mu h hn hlast).toLinearMap = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCrossOrthogonality.gtFullTransverseEmbedding_adjoint_wallTensorEmbedding_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (hlast : 0 < lam (Fin.last (r + 1))) (branch : BranchingDimension.FullBranchWeight lam) (hwrong : branch ≠ MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtWallFullBranch✝ lam mu h hlast) : LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseEmbedding✝ lam hn branch).toLinearMap ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtTransverseWallTensorEmbedding✝ lam mu h hn hlast).toLinearMap = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCrossOrthogonality.gtFullTransverseEmbedding_relativeCasimir_cross_wallTensorEmbedding_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (hlast : 0 < lam (Fin.last (r + 1))) (branch : BranchingDimension.FullBranchWeight lam) (hwrong : branch ≠ MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtWallFullBranch✝ lam mu h hlast) : LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseEmbedding✝ lam hn branch).toLinearMap ∘ₗ AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtTransverseWallTensorEmbedding✝ lam mu h hn hlast).toLinearMap = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCrossOrthogonality.gtFullTransverseEmbedding_adjoint_wallSector_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (hlast : 0 < lam (Fin.last (r + 1))) (branch : BranchingDimension.FullBranchWeight lam) (hwrong : branch ≠ MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtWallFullBranch✝ lam mu h hlast) : LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseEmbedding✝ lam hn branch).toLinearMap ∘ₗ MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtTransverseWallSector✝ lam mu h hn hlast = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCrossOrthogonality.gtFullTransverseEmbedding_relativeCasimir_cross_wallSector_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (hlast : 0 < lam (Fin.last (r + 1))) (branch : BranchingDimension.FullBranchWeight lam) (hwrong : branch ≠ MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtWallFullBranch✝ lam mu h hlast) : LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseEmbedding✝ lam hn branch).toLinearMap ∘ₗ AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam ∘ₗ MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtTransverseWallSector✝ lam mu h hn hlast = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCrossOrthogonality.gtFullTransverseEmbedding_adjoint_normalizedWallSector_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (hlast : 0 < lam (Fin.last (r + 1))) (branch : BranchingDimension.FullBranchWeight lam) (hwrong : branch ≠ MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtWallFullBranch✝ lam mu h hlast) : LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseEmbedding✝ lam hn branch).toLinearMap ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallSectorIsometry.normalizedGTTransverseWallSector✝ lam mu h hn hlast).toLinearMap = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCrossOrthogonality.gtFullTransverseEmbedding_relativeCasimir_cross_normalizedWallSector_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (hlast : 0 < lam (Fin.last (r + 1))) (branch : BranchingDimension.FullBranchWeight lam) (hwrong : branch ≠ MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallTransverseCompression.gtWallFullBranch✝ lam mu h hlast) : LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseEmbedding✝ lam hn branch).toLinearMap ∘ₗ AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam ∘ₗ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallSectorIsometry.normalizedGTTransverseWallSector✝ lam mu h hn hlast).toLinearMap = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTPhysicalWallAdditiveColumn.gtRelativeCasimir_normalizedWallSector_additiveColumn {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hn : 2 * (r + 2) + 5 ≤ n + 1) (hlast : 0 < lam (Fin.last (r + 1))) : have hw := ⋯; have B := MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTWallSectorIsometry.normalizedGTTransverseWallSector✝ lam mu h hw hlast; AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam ∘ₗ B.toLinearMap = -HigherChannel.wallShift (n + 1) (r + 1) • B.toLinearMap + AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor lam mu h hgram ∘ₗ MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirCrossBlock.gtTransverseAxisCrossBlock✝ lam mu h hgram B.toLinearMap

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseEigenNodeSeparation.negativeStabilizerNode_ne_signedAmbientNode_of_valid_raise {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (row : Fin (r + 1)) (hraise : HigherRepresentationGraph.Interlaces lam (HigherChannel.raiseWeight mu row)) (channel : Fin (r + 2) × Bool) : HigherYoungAllRankGTArrowheadSchurComplement.gtStabilizerArrowheadNode (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) mu) (Sum.inr (row, false)) ≠ HigherChannel.signedNode (HigherChannel.ambientShift (n + 1) lam) channel

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseEigenNodeSeparation.positiveStabilizerNode_ne_signedAmbientNode_of_valid_lower {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu nu : Fin (r + 1) → ℕ) (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (row : Fin (r + 1)) (hlower : mu = HigherChannel.raiseWeight nu row) (hnu : HigherRepresentationGraph.Interlaces lam nu) (channel : Fin (r + 2) × Bool) : HigherYoungAllRankGTArrowheadSchurComplement.gtStabilizerArrowheadNode (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) mu) (Sum.inr (row, true)) ≠ HigherChannel.signedNode (HigherChannel.ambientShift (n + 1) lam) channel

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTFullySelectedTransverseBranchProjection.gtFullTransverseEmbedding_range_eq_selectedTransverseTensorEmbedding {r n : ℕ} (lam : Fin (r + 2) → ℕ) (tau : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam tau) (hn : 2 * (r + 1) + 5 ≤ n + 1) (hdom : Antitone lam) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam tau h) : (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseEmbedding✝ lam hn (BranchingDimension.fullBranchOfInterlaces tau h)).range = (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCasimirEmbedding.gtTransverseTensorEmbedding✝ lam tau h hgram).range

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTPhysicalSelectedTwoBlockClosure.linearIsometry_range_starProjection {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [FiniteDimensional ℝ E] [FiniteDimensional ℝ H] (F : E →ₗᵢ[ℝ] H) (x : H) : F.range.starProjection x = F ((LinearMap.adjoint F.toLinearMap) x)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTPhysicalSelectedTwoBlockClosure.mem_submodule_of_complete_orthogonal_two_family_projections {ι : Type u_1} {κ : Type u_2} {H : Type u_3} [Finite ι] [Finite κ] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [FiniteDimensional ℝ H] (U : ι → Submodule ℝ H) (V : κ → Submodule ℝ H) (hU : ∀ (i j : ι), i ≠ j → U i ⟂ U j) (hV : ∀ (i j : κ), i ≠ j → V i ⟂ V j) (hUV : ∀ (i : ι) (j : κ), U i ⟂ V j) (hcomplete : (⨆ (i : ι), U i) ⊔ ⨆ (j : κ), V j = ⊤) (S : Submodule ℝ H) (x : H) (haxis : ∀ (i : ι), (U i).starProjection x ∈ S) (htransverse : ∀ (j : κ), (V j).starProjection x ∈ S) : x ∈ S

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTPhysicalSelectedTwoBlockClosure.gtPhysicalTensor_mem_submodule_of_full_axis_transverse_projection {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hn : 2 * r + 5 ≤ n + 1) (hdom : Antitone lam) (S : Submodule ℝ (TensorProduct ℝ (SpherePacking.Euclidean (n + 1)) ↥(HarmonicYoungSpace lam))) (x : TensorProduct ℝ (SpherePacking.Euclidean (n + 1)) ↥(HarmonicYoungSpace lam)) (haxis : ∀ (mu : BranchingDimension.FullBranchWeight lam), (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTActualAxisTransverseDecomposition.gtFullAxisEmbedding✝ lam hn mu) ((LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTActualAxisTransverseDecomposition.gtFullAxisEmbedding✝ lam hn mu).toLinearMap) x) ∈ S) (htransverse : ∀ (mu : BranchingDimension.FullBranchWeight lam), (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseEmbedding✝ lam hn mu) ((LinearMap.adjoint (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseEmbedding✝ lam hn mu).toLinearMap) x) ∈ S) : x ∈ S

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseSelectedClebschRange.linearIsometry_projection_mem_range_of_adjoint_coordinate_mem {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [NormedAddCommGroup Y] [InnerProductSpace ℝ Y] [NormedAddCommGroup Z] [InnerProductSpace ℝ Z] [FiniteDimensional ℝ X] [FiniteDimensional ℝ Y] (F : X →ₗᵢ[ℝ] Y) (B : Z →ₗ[ℝ] Y) (hBF : B.range ≤ F.range) (v : Y) (hcoordinate : (LinearMap.adjoint F.toLinearMap) v ∈ (LinearMap.adjoint F.toLinearMap ∘ₗ B).range) : F ((LinearMap.adjoint F.toLinearMap) v) ∈ B.range

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseSelectedClebschRange.linearIsometry_projection_mem_range_of_adjoint_scalar {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [NormedAddCommGroup Y] [InnerProductSpace ℝ Y] [NormedAddCommGroup Z] [InnerProductSpace ℝ Z] [FiniteDimensional ℝ X] [FiniteDimensional ℝ Y] (F : X →ₗᵢ[ℝ] Y) (B : Z →ₗ[ℝ] Y) (hBF : B.range ≤ F.range) (v : Y) (p : Z) (d : ℝ) (hcoordinate : (LinearMap.adjoint F.toLinearMap) v = d • (LinearMap.adjoint F.toLinearMap) (B p)) : F ((LinearMap.adjoint F.toLinearMap) v) ∈ B.range

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseSelectedClebschRange.linearMap_range_le_isometry_of_scaled_factor_of_range_eq {W : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [NormedAddCommGroup W] [InnerProductSpace ℝ W] [NormedAddCommGroup X] [InnerProductSpace ℝ X] [NormedAddCommGroup Y] [InnerProductSpace ℝ Y] [NormedAddCommGroup Z] [InnerProductSpace ℝ Z] (F : X →ₗᵢ[ℝ] Y) (E : W →ₗᵢ[ℝ] Y) (B : Z →ₗ[ℝ] Y) (C : Z →ₗ[ℝ] W) (phase : ℝ) (hrange : F.range = E.range) (hfactor : B = phase • E.toLinearMap ∘ₗ C) : B.range ≤ F.range

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseRetainedTwoBlockClosure.normalizedGTTransverseNegativeSector_range_le_selectedFullTransverse {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (kappa : Fin r → ℕ) (row : Fin (r + 1)) (hnu : HigherRepresentationGraph.Interlaces lam (HigherChannel.raiseWeight mu row)) (hnuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam (HigherChannel.raiseWeight mu row) hnu) (hfinite : HigherChannel.FiniteInterlacing n mu kappa) (hraise : HigherChannel.FiniteInterlacing n (HigherChannel.raiseWeight mu row) kappa) (hn : 2 * (r + 1) + 5 ≤ n + 1) : (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWignerEckartPhase.normalizedGTTransverseNegativeSector✝ lam mu kappa row hnu hnuGram hfinite hraise).range ≤ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseEmbedding✝ lam hn (BranchingDimension.fullBranchOfInterlaces (HigherChannel.raiseWeight mu row) hnu)).range

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseRetainedTwoBlockClosure.normalizedGTTransversePositiveSector_range_le_selectedFullTransverse {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu nu : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hmunu : mu = HigherChannel.raiseWeight nu row) (hmu : HigherRepresentationGraph.Interlaces lam mu) (hnu : HigherRepresentationGraph.Interlaces lam nu) (hnuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam nu hnu) (hn : 2 * (r + 1) + 5 ≤ n + 1) : (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWignerEckartPhase.normalizedGTTransversePositiveSector✝ lam mu nu row hmunu hmu hnu hnuGram).range ≤ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseFullBranchDecomposition.gtFullTransverseEmbedding✝ lam hn (BranchingDimension.fullBranchOfInterlaces nu hnu)).range

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseRetainedTwoBlockClosure.gtTransverseNegativeSector_relativeCasimir_mem_axis_sup_sector {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (kappa : Fin r → ℕ) (row : Fin (r + 1)) (hmu : HigherRepresentationGraph.Interlaces lam mu) (hmuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu hmu) (hnu : HigherRepresentationGraph.Interlaces lam (HigherChannel.raiseWeight mu row)) (hnuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam (HigherChannel.raiseWeight mu row) hnu) (hfinite : HigherChannel.FiniteInterlacing n mu kappa) (hraise : HigherChannel.FiniteInterlacing n (HigherChannel.raiseWeight mu row) kappa) (hstable : 2 * (r + 2) + 5 ≤ n + 1) (p : ↥(HarmonicYoungSpace mu)) : (AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam) ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWignerEckartPhase.normalizedGTTransverseNegativeSector✝ lam mu kappa row hnu hnuGram hfinite hraise) p) ∈ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTValidTransverseArrowheadRow.canonicalGelfandTsetlinAxisIsometry✝ lam mu hmu hmuGram).range ⊔ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWignerEckartPhase.normalizedGTTransverseNegativeSector✝ lam mu kappa row hnu hnuGram hfinite hraise).range

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseRetainedTwoBlockClosure.gtTransversePositiveSector_relativeCasimir_mem_axis_sup_sector {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu nu : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hmunu : mu = HigherChannel.raiseWeight nu row) (hmu : HigherRepresentationGraph.Interlaces lam mu) (hmuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu hmu) (hnu : HigherRepresentationGraph.Interlaces lam nu) (hnuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam nu hnu) (hstable : 2 * (r + 2) + 5 ≤ n + 1) (p : ↥(HarmonicYoungSpace mu)) : (AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam) ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWignerEckartPhase.normalizedGTTransversePositiveSector✝ lam mu nu row hmunu hmu hnu hnuGram) p) ∈ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTValidTransverseArrowheadRow.canonicalGelfandTsetlinAxisIsometry✝ lam mu hmu hmuGram).range ⊔ (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWignerEckartPhase.normalizedGTTransversePositiveSector✝ lam mu nu row hmunu hmu hnu hnuGram).range

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTAxisCompressedValidNodeRoot.signedCharacteristicAdjugate_resolvent_apply {r : ℕ} {V : Type u_1} [AddCommGroup V] [Module ℝ V] (L : Fin (r + 1) → ℝ) (hL : Function.Injective (HigherChannel.signedNode L)) (T : Module.End ℝ V) (z : ℝ) (v : V) (hchar : ((Polynomial.aeval T) (HigherYoungAllRankGTCharacteristicResidue.signedAmbientCharacteristic L)) v = 0) : (z • LinearMap.id - T) ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTAxisCompressedValidNodeRoot.signedCharacteristicAdjugate✝ L T z) v) = Polynomial.eval z (HigherYoungAllRankGTCharacteristicResidue.signedAmbientCharacteristic L) • v

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTAxisCompressedValidNodeRoot.gtAxisCompressedCharacteristicMinor_eval_eq_adjugate_inner {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (p q : ↥(HarmonicYoungSpace mu)) (z : ℝ) : Polynomial.eval z (AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedCharacteristicMinor lam mu h hgram p q) = inner ℝ ((AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor lam mu h hgram) p) ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTAxisCompressedValidNodeRoot.signedCharacteristicAdjugate✝ (HigherChannel.ambientShift (n + 1) lam) (AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam) z) ((AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor lam mu h hgram) q))

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTAxisCompressedValidNodeRoot.gtAxisCompressedCharacteristicMinor_eval_eq_zero_of_arrowhead_operator_row {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (p q : ↥(HarmonicYoungSpace mu)) (B : ↥(HarmonicYoungSpace mu) →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean (n + 1)) ↥(HarmonicYoungSpace lam)) (node : ℝ) (coupling : Module.End ℝ ↥(HarmonicYoungSpace mu)) (hcoupling : Function.Injective ⇑coupling) (horth : (LinearMap.adjoint B) ((AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor lam mu h hgram) q) = 0) (hchar : ((Polynomial.aeval (AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam)) (HigherYoungAllRankGTCharacteristicResidue.gtChannelCharacteristicPolynomial (n + 1) lam)) ((AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor lam mu h hgram) q) = 0) (hrow : ∀ (x : TensorProduct ℝ (SpherePacking.Euclidean (n + 1)) ↥(HarmonicYoungSpace lam)), (LinearMap.adjoint B) ((AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam) x) = node • (LinearMap.adjoint B) x + coupling ((LinearMap.adjoint (AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor lam mu h hgram)) x)) : Polynomial.eval node (AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedCharacteristicMinor lam mu h hgram p q) = 0

theorem MetricCodes.Spherical.HigherYoungAllRankGTCanonicalAxisSignedCharacteristic.gtChannelCharacteristic_aeval_canonicalAxis_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 2) + 5 ≤ n + 1) (hgram : HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (p : ↥(HigherHarmonicYoung.HarmonicYoungSpace mu)) : ((Polynomial.aeval (HigherHarmonicYoung.AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam)) (HigherYoungAllRankGTCharacteristicResidue.gtChannelCharacteristicPolynomial (n + 1) lam)) ((HigherHarmonicYoung.AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor lam mu h hgram) p) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTAmbientCharacteristicAtTransverseNode.signedAmbientCharacteristic_eval_ne_zero_of_forall_ne {r : ℕ} (L : Fin (r + 1) → ℝ) (d : ℝ) (hnode : ∀ (i : Fin (r + 1) × Bool), d ≠ HigherChannel.signedNode L i) : Polynomial.eval d (HigherYoungAllRankGTCharacteristicResidue.signedAmbientCharacteristic L) ≠ 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTAmbientCharacteristicAtTransverseNode.gtChannelCharacteristicPolynomial_eval_ne_zero_of_forall_ne {r n : ℕ} (lam : Fin (r + 1) → ℕ) (d : ℝ) (hnode : ∀ (i : Fin (r + 1) × Bool), d ≠ HigherChannel.signedNode (HigherChannel.ambientShift n lam) i) : Polynomial.eval d (HigherYoungAllRankGTCharacteristicResidue.gtChannelCharacteristicPolynomial n lam) ≠ 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseCouplingNonzero.polynomial_eigenvector_eq_zero_of_annihilating_eval_ne_zero {V : Type u_1} [AddCommGroup V] [Module ℝ V] (T : Module.End ℝ V) (P : Polynomial ℝ) (d : ℝ) (v : V) (heigen : T v = d • v) (hchar : ((Polynomial.aeval T) P) v = 0) (heval : Polynomial.eval d P ≠ 0) : v = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCartanSpectralCouplingNonvanishing.arrowhead_eigen_of_coupling_kernel {E : Type u_1} {F : Type u_2} {V : Type u_3} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [AddCommGroup V] [Module ℝ V] (T : Module.End ℝ V) (B : E →ₗ[ℝ] V) (A : F →ₗ[ℝ] V) (K : E →ₗ[ℝ] F) (d : ℝ) (hrow : T ∘ₗ B = d • B + A ∘ₗ K) (p : E) (hp : K p = 0) : T (B p) = d • B p

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCartanSpectralCouplingNonvanishing.arrowhead_coupling_eq_zero_of_apply_eq_zero {E : Type u_1} {F : Type u_2} {V : Type u_3} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [AddCommGroup V] [Module ℝ V] (T : Module.End ℝ V) (B : E →ₗ[ℝ] V) (hB : Function.Injective ⇑B) (A : F →ₗ[ℝ] V) (K : E →ₗ[ℝ] F) (P : Polynomial ℝ) (d : ℝ) (hrow : T ∘ₗ B = d • B + A ∘ₗ K) (hchar : ∀ (p : E), ((Polynomial.aeval T) P) (B p) = 0) (heval : Polynomial.eval d P ≠ 0) (p : E) (hp : K p = 0) : p = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCartanSpectralCouplingNonvanishing.arrowhead_coupling_injective_of_characteristic {E : Type u_1} {F : Type u_2} {V : Type u_3} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [AddCommGroup V] [Module ℝ V] (T : Module.End ℝ V) (B : E →ₗ[ℝ] V) (hB : Function.Injective ⇑B) (A : F →ₗ[ℝ] V) (K : E →ₗ[ℝ] F) (P : Polynomial ℝ) (d : ℝ) (hrow : T ∘ₗ B = d • B + A ∘ₗ K) (hchar : ∀ (p : E), ((Polynomial.aeval T) P) (B p) = 0) (heval : Polynomial.eval d P ≠ 0) : Function.Injective ⇑K

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCartanSpectralCouplingNonvanishing.arrowhead_isometric_coupling_injective_of_characteristic {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [AddCommGroup F] [Module ℝ F] [NormedAddCommGroup V] [InnerProductSpace ℝ V] (T : Module.End ℝ V) (B : E →ₗᵢ[ℝ] V) (A : F →ₗ[ℝ] V) (K : E →ₗ[ℝ] F) (P : Polynomial ℝ) (d : ℝ) (hrow : T ∘ₗ B.toLinearMap = d • B.toLinearMap + A ∘ₗ K) (hchar : ∀ (p : E), ((Polynomial.aeval T) P) (B p) = 0) (heval : Polynomial.eval d P ≠ 0) : Function.Injective ⇑K

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCartanSpectralCouplingNonvanishing.gtSignedArrowheadCoupling_injective {r n : ℕ} (lam : Fin (r + 1) → ℕ) {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗᵢ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace lam)) (A : F →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace lam)) (K : E →ₗ[ℝ] F) (d : ℝ) (hrow : AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam ∘ₗ B.toLinearMap = d • B.toLinearMap + A ∘ₗ K) (hchar : ∀ (p : E), ((Polynomial.aeval (AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam)) (HigherYoungAllRankGTCharacteristicResidue.gtChannelCharacteristicPolynomial n lam)) (B p) = 0) (hnode : ∀ (i : Fin (r + 1) × Bool), d ≠ HigherChannel.signedNode (HigherChannel.ambientShift n lam) i) : Function.Injective ⇑K

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTValidTransverseMinorRoots.gtAxisCompressedCharacteristicMinor_eval_actualPhysicalNode_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (hn : 2 * (r + 2) + 5 ≤ n + 1) (B : ↥(HarmonicYoungSpace mu) →ₗᵢ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean (n + 1)) ↥(HarmonicYoungSpace lam)) (node : ℝ) (K : Module.End ℝ ↥(HarmonicYoungSpace mu)) (horthogonal : ∀ (p q : ↥(HarmonicYoungSpace mu)), inner ℝ ((AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor lam mu h hgram) p) (B q) = 0) (hcolumn : AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam ∘ₗ B.toLinearMap = node • B.toLinearMap + AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor lam mu h hgram ∘ₗ K) (hsector : ∀ (p : ↥(HarmonicYoungSpace mu)), ((Polynomial.aeval (AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam)) (HigherYoungAllRankGTCharacteristicResidue.gtChannelCharacteristicPolynomial (n + 1) lam)) (B p) = 0) (hnode : ∀ (i : Fin (r + 2) × Bool), node ≠ HigherChannel.signedNode (HigherChannel.ambientShift (n + 1) lam) i) (p q : ↥(HarmonicYoungSpace mu)) : Polynomial.eval node (AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedCharacteristicMinor lam mu h hgram p q) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTAdjacentCommonInterlacing.gtSelectedPrefixWeight_finiteInterlacing {r n : ℕ} (mu : Fin (r + 1) → ℕ) (hn : 2 * r + 4 ≤ n) (hdom : Antitone mu) : HigherChannel.FiniteInterlacing n mu (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTAdjacentCommonInterlacing.gtSelectedPrefixWeight✝ mu)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTAdjacentCommonInterlacing.gtSelectedPrefixWeight_finiteInterlacing_raise {r n : ℕ} (mu : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hn : 2 * r + 4 ≤ n) (hdom : Antitone mu) (hraiseDom : Antitone (HigherChannel.raiseWeight mu row)) : HigherChannel.FiniteInterlacing n (HigherChannel.raiseWeight mu row) (MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTAdjacentCommonInterlacing.gtSelectedPrefixWeight✝ mu)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTValidTransverseSectorFamily.normalizedNegativeSector_canonicalAxis_inner_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (kappa : Fin r → ℕ) (hmu : HigherRepresentationGraph.Interlaces lam mu) (hmuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu hmu) (row : Fin (r + 1)) (hnu : HigherRepresentationGraph.Interlaces lam (HigherChannel.raiseWeight mu row)) (hnuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam (HigherChannel.raiseWeight mu row) hnu) (hfinite : HigherChannel.FiniteInterlacing n mu kappa) (hraise : HigherChannel.FiniteInterlacing n (HigherChannel.raiseWeight mu row) kappa) (p q : ↥(HarmonicYoungSpace mu)) : inner ℝ ((AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor lam mu hmu hmuGram) p) ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWignerEckartPhase.normalizedGTTransverseNegativeSector✝ lam mu kappa row hnu hnuGram hfinite hraise) q) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTValidTransverseSectorFamily.normalizedPositiveSector_canonicalAxis_inner_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu nu : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hmunu : mu = HigherChannel.raiseWeight nu row) (hmu : HigherRepresentationGraph.Interlaces lam mu) (hmuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu hmu) (hnu : HigherRepresentationGraph.Interlaces lam nu) (hnuGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam nu hnu) (p q : ↥(HarmonicYoungSpace mu)) : inner ℝ ((AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor lam mu hmu hmuGram) p) ((MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseWignerEckartPhase.normalizedGTTransversePositiveSector✝ lam mu nu row hmunu hmu hnu hnuGram) q) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTUnconditionalCharacteristicMinor.isometricSector_operator_column_of_mem_axis_sector {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] [FiniteDimensional ℝ V] [FiniteDimensional ℝ H] (A B : V →ₗᵢ[ℝ] H) (T : Module.End ℝ H) (d : ℝ) (horth : LinearMap.adjoint A.toLinearMap ∘ₗ B.toLinearMap = 0) (hdiag : LinearMap.adjoint B.toLinearMap ∘ₗ T ∘ₗ B.toLinearMap = d • LinearMap.id) (hclosed : ∀ (p : V), T (B p) ∈ A.range ⊔ B.range) : T ∘ₗ B.toLinearMap = d • B.toLinearMap + A.toLinearMap ∘ₗ LinearMap.adjoint A.toLinearMap ∘ₗ T ∘ₗ B.toLinearMap

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTUnconditionalCharacteristicMinor.gtAxisCompressedCharacteristicMinor_eval_negativeValidNode_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (hn : 2 * (r + 2) + 5 ≤ n + 1) (row : Fin (r + 1)) (hnu : HigherRepresentationGraph.Interlaces lam (HigherChannel.raiseWeight mu row)) (p q : ↥(HarmonicYoungSpace mu)) : Polynomial.eval (HigherYoungAllRankGTArrowheadSchurComplement.gtStabilizerArrowheadNode (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) mu) (Sum.inr (row, false))) (AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedCharacteristicMinor lam mu h hgram p q) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTUnconditionalCharacteristicMinor.gtAxisCompressedCharacteristicMinor_eval_positiveValidNode_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu nu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (hn : 2 * (r + 2) + 5 ≤ n + 1) (row : Fin (r + 1)) (hmunu : mu = HigherChannel.raiseWeight nu row) (hnu : HigherRepresentationGraph.Interlaces lam nu) (p q : ↥(HarmonicYoungSpace mu)) : Polynomial.eval (HigherYoungAllRankGTArrowheadSchurComplement.gtStabilizerArrowheadNode (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) mu) (Sum.inr (row, true))) (AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedCharacteristicMinor lam mu h hgram p q) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTUnconditionalCharacteristicMinor.gtAxisCompressedCharacteristicMinor_eval_wallNode_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (hn : 2 * (r + 2) + 5 ≤ n + 1) (p q : ↥(HarmonicYoungSpace mu)) : Polynomial.eval (-HigherChannel.wallShift (n + 1) (r + 1)) (AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedCharacteristicMinor lam mu h hgram p q) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTUnconditionalCharacteristicMinor.gtAxisCompressedCharacteristicMinor_eq_channelNumerator {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (hn : 2 * (r + 2) + 5 ≤ n + 1) (p q : ↥(HarmonicYoungSpace mu)) : AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedCharacteristicMinor lam mu h hgram p q = Polynomial.C (inner ℝ p q) * HigherChannel.channelNumeratorPolynomial (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) mu)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTUnconditionalCharacteristicMinor.fixedLevelHierarchyCodeBound : HigherHierarchy.FixedLevelHierarchyCodeBound

theorem MetricCodes.Spherical.HigherHierarchy.main_general {s : ℝ} (hs : 0 < s) (hs' : s < 1) : (∀ {r : ℕ} {R : ℝ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ), Interlacing a b → s < 2 * Gamma a b → Phi a b < R → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (C : SpherePacking.SphericalCode n s), ↑C.points.card < 2 ^ (R * ↑n)) ∧ sphericalCodeRate s ≤ closedHierarchyVariationalRate s

theorem MetricCodes.Spherical.HigherHierarchy.strict_hierarchy {s : ℝ} (hs : 0 < s) (hs' : s < 1) : (∀ (r : ℕ), levelRate (r + 1) s < levelRate r s ∧ localizedLevelRate (r + 1) s < localizedLevelRate r s) ∧ sphericalCodeRate s ≤ localizedHierarchyRate s ∧ localizedHierarchyRate s < localizedLevelRate 1 s ∧ localizedLevelRate 1 s < localizedRowRate s ∧ localizedRowRate s < localizedLevelRate 0 s ∧ localizedLevelRate 0 s = classicalLocalizedRate s

noncomputable def SpherePacking.kissingNumber (n : ℕ) : ℕ∞

The kissing number used in the spherical-code argument.

Equations

• SpherePacking.kissingNumber n = SpherePacking.sphericalCodeNumber n (1 / 2)

theorem MetricCodes.Johnson.main_binary_theorem {δ : ℝ} (hδ : 0 < δ) (hhalf : δ < 1 / 2) : Hamming.binaryRate δ ≤ combinedVariationalRate δ ∧ combinedVariationalRate δ < mrrwRate δ

theorem MetricCodes.Spherical.HigherHierarchy.NumericalMaximum.eventually_kissingNumber_lt_published : ∀ᶠ (n : ℕ) in Filter.atTop, ↑(SpherePacking.kissingNumber n).toNat ≤ 2 ^ (0.39661 * ↑n)