OAI/Geometry/HarmonicGrowth/LieSaturation.lean

GitHub source file

126 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicCounterexample.Control.skewUnit line 22
2. def OAI.HarmonicCounterexample.Control.symmetricUnit line 24
3. def OAI.HarmonicCounterexample.Control.diagonalDifference line 26
4. def OAI.HarmonicCounterexample.Control.nullRank line 28
5. lemma OAI.HarmonicCounterexample.Control.single_bracket line 30
6. lemma OAI.HarmonicCounterexample.Control.skew_symmetric_bracket line 41
7. lemma OAI.HarmonicCounterexample.Control.skew_path_bracket line 46
8. lemma OAI.HarmonicCounterexample.Control.skew_diagonal_bracket line 51
9. lemma OAI.HarmonicCounterexample.Control.diagonalDifference_eq_diagonal line 69
10. lemma OAI.HarmonicCounterexample.Control.double_skew_null_difference line 75
11. lemma OAI.HarmonicCounterexample.Control.diagonal_two_mem line 86
12. theorem OAI.HarmonicCounterexample.Control.tracefree_mem_of_units line 99

    Source documentation

    Off-diagonal units and diagonal differences span the actual trace-zero matrices, with no dimension or simplicity assumption.

    theorem tracefree_mem_of_units (L : LieSubalgebra ℂ (Matrix ι ι ℂ)) (a : ι)
        (hoff : ∀ i j,i ≠ j → single i j (1:ℂ) ∈ L)
        (hdiag : ∀ i,diagonalDifference i a ∈ L) {X : Matrix ι ι ℂ} (hX : trace X=0) : X ∈ L := by
    …

    Mentions: OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.Control.diagonalDifference

13. lemma OAI.HarmonicCounterexample.Control.unsmul_mem line 126
14. theorem OAI.HarmonicCounterexample.Control.tracefree_mem_of_skews_and_null line 134

    Source documentation

    The full trace-free algebra already follows by brackets from all skew operators and one null rank-one operator. This is a direct algebraic replacement for the manuscript's second use of special-orthogonal exponentials.

    theorem tracefree_mem_of_skews_and_null (L : LieSubalgebra ℂ (Matrix ι ι ℂ))
        (a b c : ι) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c)
        (hskew : ∀ i j,skewUnit i j ∈ L) (hn : nullRank a b ∈ L)
        {X : Matrix ι ι ℂ} (hX : trace X=0) : X ∈ L := by
    …

    Mentions: OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.Control.skewUnit, OAI.HarmonicCounterexample.Control.nullRank

15. lemma OAI.HarmonicCounterexample.Control.outer_bilinear_matrix line 202
16. lemma OAI.HarmonicCounterexample.Control.wedge_basis_matrix line 211
17. lemma OAI.HarmonicCounterexample.Control.outer_null_basis_matrix line 221
18. theorem OAI.HarmonicCounterexample.Control.tracefree_mem_of_bilinear_wedges_null line 258

    Source documentation

    Full complex special-linear saturation from all actual bilinear wedges and one nonzero null rank one. All coordinate changes and brackets are proved.

    theorem tracefree_mem_of_bilinear_wedges_null
        (L : LieSubalgebra ℂ (Module.End ℂ W))
        (B : W →ₗ[ℂ] W →ₗ[ℂ] ℂ) (hB : ∀ x y,B x y = B y x)
        (hinj : Function.Injective B) (hdim : 3 ≤ finrank ℂ W)
        (hskew : ∀ u v,wedgeLeft B u v ∈ L)
        (u : W) (hu : B u u=0) (hn : u ≠ 0) (hU : outer B u u ∈ L)
        {X : Module.End ℂ W} (hX : LinearMap.trace ℂ W X = 0) : X ∈ L := by
    …

    Mentions: OAI.HarmonicCounterexample.Control.wedgeLeft, OAI.HarmonicCounterexample.Control.outer

19. lemma OAI.HarmonicCounterexample.ComplexAngular.linearForm_single_coordinate line 316
20. lemma OAI.HarmonicCounterexample.ComplexAngular.quadric_eval_single_inl line 320
21. def OAI.HarmonicCounterexample.ComplexAngular.coordinatePower line 324
22. lemma OAI.HarmonicCounterexample.ComplexAngular.coordinatePower_val line 327
23. lemma OAI.HarmonicCounterexample.ComplexAngular.eval_coordinatePower line 332
24. lemma OAI.HarmonicCounterexample.ComplexAngular.coordinatePowers_independent line 338
25. lemma OAI.HarmonicCounterexample.ComplexAngular.harmonicSpace_finrank_lower line 348
26. theorem OAI.HarmonicCounterexample.Control.harmonicAngularLie_has_specialLinear line 375

    Source documentation

    One-block complex Lie saturation on the genuine harmonic polynomials in sixteen Cartesian dimensions, for every degree l>=2. No abstract-irreducibility, orbit-spanning, or desired Lie-equality assumption is used.

    theorem harmonicAngularLie_has_specialLinear (l : ℕ) (hl : 2 ≤ l)
        {X : Module.End ℂ (harmonicSpace (Fin 8) l)}
        (hX : LinearMap.trace ℂ (harmonicSpace (Fin 8) l) X=0) :
        X ∈ harmonicAngularLie l := by
    …

    Mentions: OAI.HarmonicCounterexample.Control.harmonicAngularLie

27. lemma OAI.HarmonicCounterexample.Control.complex_smul_real_parts line 413
28. def OAI.HarmonicCounterexample.Control.complexLieEnvelope line 423

    Source documentation

    The complex scalar envelope of an actual real Lie algebra, with explicit real and imaginary witnesses.

    def complexLieEnvelope (L : LieSubalgebra ℝ A) : LieSubalgebra ℂ A where
    …

29. lemma OAI.HarmonicCounterexample.Control.subset_complexLieEnvelope line 446
30. lemma OAI.HarmonicCounterexample.Control.lieSpan_complex_decomposition line 449
31. theorem OAI.HarmonicCounterexample.Control.real_lieSpan_of_complex line 460

    Source documentation

    Faithful real descent. A conjugation-fixed element of a complex generated Lie algebra is already in the real generated algebra, provided all generators are fixed by the same actual algebra conjugation.

    theorem real_lieSpan_of_complex (s : Set A)
        (τ : A →ₗ[ℝ] A)
        (hτI : ∀ x,τ (Complex.I • x) = -Complex.I • τ x)
        (hτlie : ∀ x y,τ ⁅x,y⁆ = ⁅τ x,τ y⁆)
        (hs : ∀ x ∈ s,τ x=x) {x : A}
        (hx : x ∈ LieSubalgebra.lieSpan ℂ A s) (hτx : τ x=x) :
        x ∈ LieSubalgebra.lieSpan ℝ A s := by
    …

32. def OAI.HarmonicCounterexample.Control.conjugatedBasis line 515
33. lemma OAI.HarmonicCounterexample.Control.conjugatedBasis_repr line 518
34. lemma OAI.HarmonicCounterexample.Control.conjugatedBasis_apply line 521
35. lemma OAI.HarmonicCounterexample.Control.trace_conj_semilinear line 529
36. def OAI.HarmonicCounterexample.Control.realEndConjugation line 543
37. lemma OAI.HarmonicCounterexample.Control.realEndConjugation_I line 551
38. lemma OAI.HarmonicCounterexample.Control.realEndConjugation_lie line 557
39. lemma OAI.HarmonicCounterexample.ComplexAngular.conjugate_swapPolynomial line 584
40. def OAI.HarmonicCounterexample.ComplexAngular.realConjugatePolynomial line 590

    Source documentation

    Conjugation in split coordinates of a real Cartesian polynomial: it also interchanges z and bar-z, rather than merely conjugating their coefficients.

    def realConjugatePolynomial : SplitPolynomial ι ≃ₗ⋆[ℂ] SplitPolynomial ι where
    …

    Mentions: OAI.HarmonicCounterexample.ComplexAngular.SplitPolynomial

41. lemma OAI.HarmonicCounterexample.ComplexAngular.realConjugatePolynomial_pderiv line 602
42. lemma OAI.HarmonicCounterexample.ComplexAngular.realConjugatePolynomial_X line 610
43. lemma OAI.HarmonicCounterexample.ComplexAngular.realConjugatePolynomial_mul line 617
44. lemma OAI.HarmonicCounterexample.ComplexAngular.realConjugatePolynomial_mem_harmonicSpace line 623
45. def OAI.HarmonicCounterexample.ComplexAngular.spaceRealConjugation line 627
46. lemma OAI.HarmonicCounterexample.Berger.ComplexStructure.splitFieldMatrix_conjugate line 654
47. lemma OAI.HarmonicCounterexample.ComplexAngular.realConjugatePolynomial_linearField line 684
48. lemma OAI.HarmonicCounterexample.ComplexAngular.spaceRealConjugation_harmonicField line 697
49. lemma OAI.HarmonicCounterexample.ComplexAngular.spaceRealConjugation_conj_harmonicField line 704
50. lemma OAI.HarmonicCounterexample.Control.traceFreeEnd_conj line 730
51. def OAI.HarmonicCounterexample.Control.harmonicRealAngularLie line 739

    Source documentation

    The genuine REAL generated algebra on the real-Cartesian form of the complex harmonic space; only real control times and linear combinations occur.

    def harmonicRealAngularLie (l : ℕ) : LieSubalgebra ℝ
        (Module.End ℂ (harmonicSpace (Fin 8) l)) :=
    …

52. theorem OAI.HarmonicCounterexample.Control.harmonicRealAngularLie_has_specialLinear line 746

    Source documentation

    Real descent for the actual one-block angular algebra. Every trace-zero operator preserving the real Cartesian form is generated using real scalars.

    theorem harmonicRealAngularLie_has_specialLinear (l : ℕ) (hl : 2 ≤ l)
        {X : Module.End ℂ (harmonicSpace (Fin 8) l)}
        (hX : LinearMap.trace ℂ (harmonicSpace (Fin 8) l) X=0)
        (hr : (spaceRealConjugation l).conj X=X) :
        X ∈ harmonicRealAngularLie l := by
    …

    Mentions: OAI.HarmonicCounterexample.Control.harmonicRealAngularLie

53. lemma OAI.HarmonicCounterexample.Control.filterEntry_mem_submodule line 783
54. theorem OAI.HarmonicCounterexample.Control.isolate_entry_submodule line 791

    Source documentation

    Finite joint-eigenvalue interpolation isolates a genuine directed matrix entry. Zeros of the input require no spectral separation. This is the precise linear-algebra step used after the torus Fourier projection in the manuscript.

    theorem isolate_entry_submodule (L : Submodule 𝕜 (Matrix ι ι 𝕜))
        (d : κ → ι → 𝕜) (hd : ∀ a Y, Y ∈ L → ⁅diagonal (d a),Y⁆ ∈ L)
        {X : Matrix ι ι 𝕜} (hX : X ∈ L) (p q : ι)
        (hsep : ∀ i j, (i,j) ≠ (p,q) → X i j ≠ 0 →
          ∃ a, d a p-d a q ≠ d a i-d a j) :
        single p q (X p q) ∈ L := by
    …

    Mentions: OAI.HarmonicCounterexample.a

55. lemma OAI.HarmonicCounterexample.Control.normalize_entry_submodule line 829
56. lemma OAI.HarmonicCounterexample.Control.off_diagonal_weight_separation line 857
57. lemma OAI.HarmonicCounterexample.Control.ideal_offdiagonal_unit line 875
58. lemma OAI.HarmonicCounterexample.Control.trace_single_offdiagonal line 883
59. lemma OAI.HarmonicCounterexample.Control.central_scalar_lie_zero line 886
60. lemma OAI.HarmonicCounterexample.Control.ideal_diagonal_invariant line 889
61. lemma OAI.HarmonicCounterexample.Control.single_lie_single_complex line 901
62. lemma OAI.HarmonicCounterexample.Control.ideal_unit_all_units line 912
63. lemma OAI.HarmonicCounterexample.Control.nonzero_tracefree_has_diagonal_difference line 973
64. lemma OAI.HarmonicCounterexample.Control.ideal_has_unit line 990
65. lemma OAI.HarmonicCounterexample.Control.tracefree_mem_submodule_of_units line 1007
66. theorem OAI.HarmonicCounterexample.Control.specialLinear_ideal_saturation line 1036

    Source documentation

    Simplicity, proved entry by entry: every subspace invariant under all special-linear brackets and containing a nonzero trace-zero matrix contains all trace-zero matrices.

    theorem specialLinear_ideal_saturation (I : Submodule ℂ (Matrix ι ι ℂ))
        (hinv : ∀ (A X : Matrix ι ι ℂ),A.trace=0 → X ∈ I → ⁅A,X⁆ ∈ I)
        {X : Matrix ι ι ℂ} (hX : X ∈ I) (hne : X ≠ 0) (ht : X.trace=0)
        {Y : Matrix ι ι ℂ} (hY : Y.trace=0) : Y ∈ I := by
    …

67. theorem OAI.HarmonicCounterexample.Control.specialLinear_isSimple line 1073
68. lemma OAI.HarmonicCounterexample.Control.specialLinear_finrank_add_one line 1122
69. lemma OAI.HarmonicCounterexample.Control.specialLinear_not_equiv line 1134
70. instance OAI.HarmonicCounterexample.Control.piLieRing line 1164
71. instance OAI.HarmonicCounterexample.Control.piLieAlgebra line 1171
72. theorem OAI.HarmonicCounterexample.Control.pi_lie_apply line 1175
73. def OAI.HarmonicCounterexample.Control.liePiEval line 1181

    Source documentation

    Coordinate projections of the genuine direct-product Lie algebra.

    def liePiEval (i : ι) : (∀ j,L j) →ₗ⁅𝕜⁆ L i where
    …

74. def OAI.HarmonicCounterexample.Control.zeroCoordinatesIdeal line 1185
75. def OAI.HarmonicCounterexample.Control.verticalIdeal line 1222

    Source documentation

    The vertical kernel of a surjective Lie subdirect product.

    def verticalIdeal (S : LieSubalgebra 𝕜 (A × B))
        (hB : ∀ b : B, ∃ a : A, (a,b) ∈ S) : LieIdeal 𝕜 B where
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.a

76. theorem OAI.HarmonicCounterexample.Control.simple_subdirect_eq_top line 1234

    Source documentation

    Goursat's argument for simple, nonisomorphic Lie factors.

    theorem simple_subdirect_eq_top [LieAlgebra.IsSimple 𝕜 A] [LieAlgebra.IsSimple 𝕜 B]
        (hne : ¬ Nonempty (A ≃ₗ⁅𝕜⁆ B)) (S : LieSubalgebra 𝕜 (A × B))
        (hA : ∀ a : A, ∃ b : B, (a,b) ∈ S)
        (hB : ∀ b : B, ∃ a : A, (a,b) ∈ S) : S = ⊤ := by
    …

    Mentions: OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.b

77. theorem OAI.HarmonicCounterexample.Control.simple_pi_subdirect_eq_top line 1309

    Source documentation

    Simple nonisomorphic factors cannot be diagonally coupled: every subdirect product is the whole product. The finite-coordinate proof also explains why pairwise surjectivity suffices for these nonabelian factors.

    theorem simple_pi_subdirect_eq_top [Fintype ι] [DecidableEq ι]
        (hne : ∀ i j,i ≠ j → ¬ Nonempty (L i ≃ₗ⁅𝕜⁆ L j))
        (S : LieSubalgebra 𝕜 (∀ j,L j))
        (hS : ∀ i (x : L i),∃ v ∈ S,v i=x) : S=⊤ := by
    …

78. theorem OAI.HarmonicCounterexample.Control.simultaneous_simple_generation line 1400

    Source documentation

    The same control parameter acts on all blocks. No independent block controls are smuggled into the simultaneous generating set.

    theorem simultaneous_simple_generation (g : κ → ∀ i,L i)
        (hne : ∀ i j,i ≠ j → ¬ Nonempty (L i ≃ₗ⁅𝕜⁆ L j))
        (hblocks : ∀ i,LieSubalgebra.lieSpan 𝕜 (L i) (Set.range fun k => g k i)=⊤) :
        LieSubalgebra.lieSpan 𝕜 (∀ i,L i) (Set.range g)=⊤ := by
    …

79. lemma OAI.HarmonicCounterexample.Control.trace_traceFreeEnd line 1437
80. lemma OAI.HarmonicCounterexample.Control.traceFreeEnd_idempotent line 1442
81. def OAI.HarmonicCounterexample.Control.endTraceFreeLieHom line 1445
82. def OAI.HarmonicCounterexample.Control.endSLMatrixHom line 1450

    Source documentation

    Actual trace-free coordinate matrices in an arbitrary basis.

    def endSLMatrixHom (b : Basis ι ℂ V) : Module.End ℂ V →ₗ⁅ℂ⁆ SpecialLinear.sl ι ℂ where
    …

    Mentions: OAI.HarmonicCounterexample.b

83. lemma OAI.HarmonicCounterexample.Control.endSLMatrixHom_val line 1461
84. lemma OAI.HarmonicCounterexample.Control.endSLMatrixHom_tracefree_preimage line 1464
85. theorem OAI.HarmonicCounterexample.Control.endSLMatrix_span_top line 1473

    Source documentation

    Coordinate transport of a proved one-block trace-free generation result.

    theorem endSLMatrix_span_top {κ : Type*} (b : Basis ι ℂ V) (g : κ → Module.End ℂ V)
        (hg : ∀ X,LinearMap.trace ℂ V X=0 → X ∈ LieSubalgebra.lieSpan ℂ _ (Set.range g)) :
        LieSubalgebra.lieSpan ℂ (SpecialLinear.sl ι ℂ) (Set.range (fun k => endSLMatrixHom b (g k)))=⊤ := by
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.Control.endSLMatrixHom

86. instance OAI.HarmonicCounterexample.ComplexAngular.complexHomogeneous_finite line 1510
87. lemma OAI.HarmonicCounterexample.ComplexAngular.complexHomogeneous_finrank line 1514
88. def OAI.HarmonicCounterexample.ComplexAngular.subspaceFischer line 1529
89. lemma OAI.HarmonicCounterexample.ComplexAngular.subspaceFischer_injective line 1533
90. lemma OAI.HarmonicCounterexample.ComplexAngular.subspaceFischer_surjective line 1543
91. lemma OAI.HarmonicCounterexample.ComplexAngular.quadric_homogeneous line 1549
92. def OAI.HarmonicCounterexample.ComplexAngular.homogeneousQuadricMultiply line 1554
93. lemma OAI.HarmonicCounterexample.ComplexAngular.homogeneousQuadricMultiply_injective line 1564
94. def OAI.HarmonicCounterexample.ComplexAngular.homogeneousMixedLaplacian line 1569
95. lemma OAI.HarmonicCounterexample.ComplexAngular.homogeneousMixedLaplacian_surjective line 1581
96. def OAI.HarmonicCounterexample.ComplexAngular.harmonicSpaceKernelEquiv line 1598
97. lemma OAI.HarmonicCounterexample.ComplexAngular.harmonicSpace_finrank_add line 1608
98. lemma OAI.HarmonicCounterexample.ComplexAngular.harmonicSpace_finrank_sixteen line 1639
99. lemma OAI.HarmonicCounterexample.ComplexAngular.harmonicSpace_finrank_strictMono line 1653
100. lemma OAI.HarmonicCounterexample.Control.lieSpan_range_smul line 1684
101. abbrev OAI.HarmonicCounterexample.Control.harmonicSL line 1721

     Source documentation

     The actual complex harmonic degree l+2, coordinatized only after its Laplacian kernel and dimension have been proved.

     abbrev harmonicSL (l : ℕ) :=
     …

102. instance OAI.HarmonicCounterexample.Control.harmonicIndex_nonempty line 1724
103. lemma OAI.HarmonicCounterexample.Control.harmonicIndex_card_gt_one line 1730
104. instance OAI.HarmonicCounterexample.Control.harmonicSL_simple line 1736
105. lemma OAI.HarmonicCounterexample.Control.harmonicSL_not_equiv line 1739
106. def OAI.HarmonicCounterexample.Control.harmonicControlMatrix line 1745
107. lemma OAI.HarmonicCounterexample.Control.harmonicControlMatrix_span_top line 1750
108. theorem OAI.HarmonicCounterexample.Control.harmonic_simultaneous_complex_control line 1760

     Source documentation

     Simultaneous complex special-linear controllability of all active degrees 2,...,L+1 in n=16, with arbitrary nonzero degree weights. Each generator uses ONE genuine real orthogonal complex structure shared by ALL degrees.

     theorem harmonic_simultaneous_complex_control (L : ℕ) (c : Fin L → ℂ)
         (hc : ∀ l,c l ≠ 0) :
         LieSubalgebra.lieSpan ℂ (∀ l : Fin L,harmonicSL l.val)
           (Set.range (fun J : ComplexStructure (Fin 8 ⊕ Fin 8) =>
             fun l : Fin L => harmonicControlMatrix l.val (c l) J))=⊤ := by
     …

     Mentions: OAI.HarmonicCounterexample.Control.harmonicSL, OAI.HarmonicCounterexample.Control.harmonicControlMatrix

109. def OAI.HarmonicCounterexample.Control.traceFreeTuple line 1795

     Source documentation

     Coordinate-free trace-zero tuples of actual endomorphisms.

     def traceFreeTuple : LieSubalgebra ℂ (∀ i,Module.End ℂ (V i)) where
     …

110. def OAI.HarmonicCounterexample.Control.endSLTupleHom line 1805
111. lemma OAI.HarmonicCounterexample.Control.endSLTupleHom_injective_on_tracefree line 1811
112. lemma OAI.HarmonicCounterexample.Control.tuple_tracefree_span_of_matrix_full line 1821
113. lemma OAI.HarmonicCounterexample.Control.VectorRealDescent.complex_smul_real_parts line 1856
114. def OAI.HarmonicCounterexample.Control.VectorRealDescent.complexLieEnvelope line 1866

     Source documentation

     The complex scalar envelope of an actual real Lie algebra, with explicit real and imaginary witnesses.

     def complexLieEnvelope (L : LieSubalgebra ℝ A) : LieSubalgebra ℂ A where
     …

115. lemma OAI.HarmonicCounterexample.Control.VectorRealDescent.subset_complexLieEnvelope line 1889
116. lemma OAI.HarmonicCounterexample.Control.VectorRealDescent.lieSpan_complex_decomposition line 1892
117. theorem OAI.HarmonicCounterexample.Control.VectorRealDescent.real_lieSpan_of_complex line 1903

     Source documentation

     Faithful real descent. A conjugation-fixed element of a complex generated Lie algebra is already in the real generated algebra, provided all generators are fixed by the same actual algebra conjugation.

     theorem real_lieSpan_of_complex (s : Set A)
         (τ : A →ₗ[ℝ] A)
         (hτI : ∀ x,τ (Complex.I • x) = -Complex.I • τ x)
         (hτlie : ∀ x y,τ ⁅x,y⁆ = ⁅τ x,τ y⁆)
         (hs : ∀ x ∈ s,τ x=x) {x : A}
         (hx : x ∈ LieSubalgebra.lieSpan ℂ A s) (hτx : τ x=x) :
         x ∈ LieSubalgebra.lieSpan ℝ A s := by
     …

118. def OAI.HarmonicCounterexample.Control.harmonicTupleGenerator line 1960

     Source documentation

     Shared weighted angular generators as ACTUAL endomorphisms, not just coordinate matrices. Positive source weights are allowed in particular.

     def harmonicTupleGenerator (L : ℕ) (c : Fin L → ℂ)
         (J : ComplexStructure (Fin 8 ⊕ Fin 8)) :
         ∀ l : Fin L,Module.End ℂ (harmonicSpace (Fin 8) (l.val+2)) :=
     …

119. lemma OAI.HarmonicCounterexample.Control.harmonicTupleGenerator_tracefree line 1965
120. theorem OAI.HarmonicCounterexample.Control.harmonic_simultaneous_complex_end line 1972
121. def OAI.HarmonicCounterexample.Control.harmonicTupleConjugation line 1981
122. lemma OAI.HarmonicCounterexample.Control.harmonicTupleConjugation_I line 1987
123. lemma OAI.HarmonicCounterexample.Control.harmonicTupleConjugation_lie line 1993
124. lemma OAI.HarmonicCounterexample.Control.harmonic_weighted_generator_real line 1999
125. lemma OAI.HarmonicCounterexample.Control.harmonicTupleGenerator_real line 2009
126. theorem OAI.HarmonicCounterexample.Control.harmonic_simultaneous_real_end line 2020

     Source documentation

     Actual simultaneous REAL controllability in every finite set of degrees 2,...,L+1, preserving the source's degree-dependent nonzero real weights. The real structure is Cartesian coefficient conjugation in split coordinates; no independent block controls or extra algebra-saturation hypotheses occur.

     theorem harmonic_simultaneous_real_end (L : ℕ) (c : Fin L → ℝ)
         (hc : ∀ l,c l ≠ 0)
         {X : ∀ l : Fin L,Module.End ℂ (harmonicSpace (Fin 8) (l.val+2))}
         (hX : ∀ l,LinearMap.trace ℂ _ (X l)=0)
         (hr : ∀ l,(spaceRealConjugation (l.val+2)).conj (X l)=X l) :
         X ∈ LieSubalgebra.lieSpan ℝ _
           (Set.range (harmonicTupleGenerator L (fun l => (c l:ℂ)))) := by
     …

     Mentions: OAI.HarmonicCounterexample.Control.harmonicTupleGenerator