OAI/Geometry/HarmonicGrowth/ComplexHarmonics.lean

GitHub source file

116 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicCounterexample.ComplexAngular.factorialWeight line 21

   Source documentation

   The bilinear Fischer form, over the actual complex polynomial algebra.

   def factorialWeight (d : σ →₀ ℕ) : ℂ := ∏ i : σ,(d i).factorial

2. def OAI.HarmonicCounterexample.ComplexAngular.fischer line 23
3. lemma OAI.HarmonicCounterexample.ComplexAngular.fischer_monomial line 27
4. lemma OAI.HarmonicCounterexample.ComplexAngular.fischer_apply line 35
5. lemma OAI.HarmonicCounterexample.ComplexAngular.fischer_symm line 40
6. lemma OAI.HarmonicCounterexample.ComplexAngular.factorialWeight_add_single line 53
7. lemma OAI.HarmonicCounterexample.ComplexAngular.fischer_mul_X line 68
8. def OAI.HarmonicCounterexample.ComplexAngular.conjugate line 78
9. lemma OAI.HarmonicCounterexample.ComplexAngular.coeff_conjugate line 81
10. lemma OAI.HarmonicCounterexample.ComplexAngular.conjugate_involutive line 85
11. lemma OAI.HarmonicCounterexample.ComplexAngular.conjugate_pderiv line 90
12. lemma OAI.HarmonicCounterexample.ComplexAngular.factorialWeight_re line 93
13. lemma OAI.HarmonicCounterexample.ComplexAngular.factorialWeight_im line 98
14. lemma OAI.HarmonicCounterexample.ComplexAngular.factorialWeight_re_pos line 102
15. lemma OAI.HarmonicCounterexample.ComplexAngular.fischer_conjugate_re line 106
16. lemma OAI.HarmonicCounterexample.ComplexAngular.fischer_definite line 116
17. abbrev OAI.HarmonicCounterexample.ComplexAngular.SplitPolynomial line 148
18. def OAI.HarmonicCounterexample.ComplexAngular.quadric line 151

    Source documentation

    The isotropic quadratic in independent z and bar-z variables.

    def quadric (ι : Type*) [Fintype ι] : SplitPolynomial ι :=
    …

    Mentions: OAI.HarmonicCounterexample.ComplexAngular.SplitPolynomial

19. def OAI.HarmonicCounterexample.ComplexAngular.mixedLaplacian line 154
20. lemma OAI.HarmonicCounterexample.ComplexAngular.mixedLaplacian_apply line 157
21. lemma OAI.HarmonicCounterexample.ComplexAngular.fischer_quadric line 161
22. lemma OAI.HarmonicCounterexample.ComplexAngular.conjugate_quadric line 169
23. lemma OAI.HarmonicCounterexample.ComplexAngular.conjugate_mixedLaplacian line 172
24. theorem OAI.HarmonicCounterexample.ComplexAngular.harmonic_quadric_multiple line 178

    Source documentation

    A harmonic multiple of the isotropic quadratic is zero. Positivity is proved in the actual coefficient algebra by the Hermitian Fischer form.

    theorem harmonic_quadric_multiple {P : SplitPolynomial ι}
        (hP : mixedLaplacian P = 0) (hdiv : quadric ι ∣ P) : P = 0 := by
    …

    Mentions: OAI.HarmonicCounterexample.ComplexAngular.SplitPolynomial, OAI.HarmonicCounterexample.ComplexAngular.mixedLaplacian, OAI.HarmonicCounterexample.ComplexAngular.quadric

25. lemma OAI.HarmonicCounterexample.ComplexAngular.quadric_irreducible line 186
26. theorem OAI.HarmonicCounterexample.ComplexAngular.quadric_dvd_of_vanishing line 206

    Source documentation

    The orbit-spanning divisibility step from the manuscript, now obtained from the pinned Nullstellensatz and a proved irreducible actual quadric.

    theorem quadric_dvd_of_vanishing [Nontrivial ι] (P : SplitPolynomial ι)
        (hP : ∀ a : (ι ⊕ ι) → ℂ,MvPolynomial.eval a (quadric ι) = 0 →
          MvPolynomial.eval a P = 0) : quadric ι ∣ P := by
    …

    Mentions: OAI.HarmonicCounterexample.ComplexAngular.SplitPolynomial, OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.ComplexAngular.quadric

27. def OAI.HarmonicCounterexample.ComplexAngular.linearForm line 240
28. lemma OAI.HarmonicCounterexample.ComplexAngular.factorialWeight_mul_multinomial line 242
29. lemma OAI.HarmonicCounterexample.ComplexAngular.fischer_linearForm_pow line 252
30. theorem OAI.HarmonicCounterexample.ComplexAngular.harmonic_eq_zero_of_isotropic_pairing line 271

    Source documentation

    No nonzero homogeneous harmonic polynomial can annihilate every isotropic power. This is the actual polynomial producer in the orbit-span argument.

    theorem harmonic_eq_zero_of_isotropic_pairing {P : SplitPolynomial ι} {l : ℕ}
        (hP : P.IsHomogeneous l) (hΔ : mixedLaplacian P = 0)
        (hpair : ∀ a : (ι ⊕ ι) → ℂ,MvPolynomial.eval a (quadric ι) = 0 →
          fischer P (linearForm a ^ l) = 0) : P = 0 := by
    …

    Mentions: OAI.HarmonicCounterexample.ComplexAngular.SplitPolynomial, OAI.HarmonicCounterexample.ComplexAngular.mixedLaplacian, OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.ComplexAngular.quadric, OAI.HarmonicCounterexample.ComplexAngular.fischer, OAI.HarmonicCounterexample.ComplexAngular.linearForm

31. lemma OAI.HarmonicCounterexample.ComplexAngular.linearForm_homogeneous line 302
32. lemma OAI.HarmonicCounterexample.ComplexAngular.pderiv_linearForm line 307
33. lemma OAI.HarmonicCounterexample.ComplexAngular.mixedLaplacian_linearForm_pow line 313
34. lemma OAI.HarmonicCounterexample.ComplexAngular.isotropicPower_harmonic line 330
35. def OAI.HarmonicCounterexample.ComplexAngular.harmonicSpace line 341

    Source documentation

    The actual degree-l complex harmonic polynomial space in independent complex coordinates. It is not postulated as an irreducible representation.

    def harmonicSpace (ι : Type*) [Fintype ι] (l : ℕ) : Submodule ℂ (SplitPolynomial ι) :=
    …

    Mentions: OAI.HarmonicCounterexample.ComplexAngular.SplitPolynomial

36. lemma OAI.HarmonicCounterexample.ComplexAngular.mem_harmonicSpace line 344
37. instance OAI.HarmonicCounterexample.ComplexAngular.harmonicSpace_finite line 347
38. lemma OAI.HarmonicCounterexample.ComplexAngular.conjugate_mem_harmonicSpace line 352
39. def OAI.HarmonicCounterexample.ComplexAngular.spaceFischer line 358
40. lemma OAI.HarmonicCounterexample.ComplexAngular.spaceFischer_surjective line 361
41. def OAI.HarmonicCounterexample.ComplexAngular.isotropicPower line 372
42. theorem OAI.HarmonicCounterexample.ComplexAngular.isotropicPowers_span line 381

    Source documentation

    The full isotropic-power span is proved by actual coefficient duality and the prime quadric ideal, without importing a representation-theoretic axiom.

    theorem isotropicPowers_span [Nontrivial ι] (l : ℕ) :
        Submodule.span ℂ (Set.range (isotropicPower (ι := ι) l)) = ⊤ := by
    …

    Mentions: OAI.HarmonicCounterexample.ComplexAngular.isotropicPower

43. theorem OAI.HarmonicCounterexample.ComplexAngular.power_product_zero line 417

    Source documentation

    Algebraic replacement for the manuscript's real-analytic density step. On the actual isotropic-power orbit, the product of two nonzero linear functionals cannot vanish identically. The proof uses the prime quadric.

    theorem power_product_zero (l : ℕ) (f g : Module.Dual ℂ (harmonicSpace ι l))
        (hf : f ≠ 0)
        (h : ∀ a,f (isotropicPower l a)*g (isotropicPower l a) = 0) : g = 0 := by
    …

    Mentions: OAI.HarmonicCounterexample.ComplexAngular.harmonicSpace, OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.ComplexAngular.isotropicPower

44. def OAI.HarmonicCounterexample.Control.outer line 462

    Source documentation

    Genuine rank-one endomorphisms for a bilinear form.

    def outer (B : W →ₗ[𝕜] W →ₗ[𝕜] 𝕜) (u v : W) : Module.End 𝕜 W :=
    …

45. lemma OAI.HarmonicCounterexample.Control.outer_apply line 465
46. def OAI.HarmonicCounterexample.Control.wedgeLeft line 467
47. lemma OAI.HarmonicCounterexample.Control.wedgeLeft_apply line 475
48. lemma OAI.HarmonicCounterexample.Control.wedgeLeft_flip line 478
49. lemma OAI.HarmonicCounterexample.Control.bracket_outer line 481
50. theorem OAI.HarmonicCounterexample.ComplexAngular.wedges_mem_of_isotropic_rankones line 512

    Source documentation

    From all orbit rank-one operators to every skew operator, with neither an unproved density principle nor an assumed Lie saturation step.

    theorem wedges_mem_of_isotropic_rankones
        (L : LieSubalgebra ℂ (Module.End ℂ (harmonicSpace ι l)))
        (B : harmonicSpace ι l →ₗ[ℂ] Module.Dual ℂ (harmonicSpace ι l))
        (hB : ∀ x y,B x y = B y x) (hinj : Function.Injective B)
        (hL : ∀ a,outer B (isotropicPower l a) (isotropicPower l a) ∈ L) :
        ∀ u v,wedgeLeft B u v ∈ L := by
    …

    Mentions: OAI.HarmonicCounterexample.ComplexAngular.harmonicSpace, OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.ComplexAngular.isotropicPower

51. def OAI.HarmonicCounterexample.ComplexAngular.swapPolynomial line 572
52. lemma OAI.HarmonicCounterexample.ComplexAngular.swapPolynomial_involutive line 576
53. lemma OAI.HarmonicCounterexample.ComplexAngular.swapPolynomial_X line 581
54. lemma OAI.HarmonicCounterexample.ComplexAngular.swapPolynomial_pderiv line 584
55. lemma OAI.HarmonicCounterexample.ComplexAngular.pderiv_commute line 589
56. lemma OAI.HarmonicCounterexample.ComplexAngular.swapPolynomial_mixedLaplacian line 602
57. lemma OAI.HarmonicCounterexample.ComplexAngular.fischer_C line 609
58. lemma OAI.HarmonicCounterexample.ComplexAngular.fischer_swapPolynomial line 613
59. lemma OAI.HarmonicCounterexample.ComplexAngular.swapPolynomial_mem_harmonicSpace line 626
60. def OAI.HarmonicCounterexample.ComplexAngular.spaceSwap line 632
61. def OAI.HarmonicCounterexample.ComplexAngular.roundPairing line 643

    Source documentation

    The invariant complex bilinear Fischer form in split coordinates, swapping z and bar-z in the second argument. This is the correct null-vector pairing, not the positive coefficient pairing without this swap.

    def roundPairing (l : ℕ) : harmonicSpace ι l →ₗ[ℂ] Module.Dual ℂ (harmonicSpace ι l) :=
    …

    Mentions: OAI.HarmonicCounterexample.ComplexAngular.harmonicSpace

62. lemma OAI.HarmonicCounterexample.ComplexAngular.roundPairing_apply line 646
63. lemma OAI.HarmonicCounterexample.ComplexAngular.roundPairing_symm line 649
64. lemma OAI.HarmonicCounterexample.ComplexAngular.roundPairing_injective line 653
65. lemma OAI.HarmonicCounterexample.ComplexAngular.eval_swap_linearForm line 659
66. lemma OAI.HarmonicCounterexample.ComplexAngular.roundPairing_isotropicPower line 669
67. lemma OAI.HarmonicCounterexample.ComplexAngular.linearForm_single line 700
68. lemma OAI.HarmonicCounterexample.ComplexAngular.factorialWeight_single line 704
69. lemma OAI.HarmonicCounterexample.ComplexAngular.homogeneous_eval_single line 712
70. lemma OAI.HarmonicCounterexample.Control.eval_linearChange line 741
71. lemma OAI.HarmonicCounterexample.Control.coeff_pure_linearChange line 749
72. lemma OAI.HarmonicCounterexample.Control.matrixUnit_homogeneous_apply line 758
73. lemma OAI.HarmonicCounterexample.ComplexAngular.linearForm_power_homogeneous line 798
74. lemma OAI.HarmonicCounterexample.ComplexAngular.homogeneous_eval_smul line 802
75. def OAI.HarmonicCounterexample.Control.homogeneousPowerRankOne line 838

    Source documentation

    Actual polynomial evaluation rank-one operator.

    def homogeneousPowerRankOne (l : ℕ) (a : (Fin s ⊕ Fin s) → ℂ) :
        Module.End ℂ (homogeneousSubmodule (Fin s ⊕ Fin s) ℂ l) where
    …

    Mentions: OAI.HarmonicCounterexample.a

76. lemma OAI.HarmonicCounterexample.Control.homogeneousPowerRankOne_apply_val line 851
77. def OAI.HarmonicCounterexample.Control.powerRankOneMatrix line 856
78. lemma OAI.HarmonicCounterexample.Control.angular_conjugate_endpoint line 859
79. lemma OAI.HarmonicCounterexample.Control.powerRankOne_smul line 883
80. lemma OAI.HarmonicCounterexample.Control.powerRankOne_zero line 901
81. theorem OAI.HarmonicCounterexample.Control.angularLie_all_rankones line 908

    Source documentation

    All null-cone polynomial evaluation rank-one operators belong to the ACTUAL angular Lie algebra in n=16, for every degree l>=2.

    theorem angularLie_all_rankones (l : ℕ) (hl : 2 ≤ l)
        (a : (Fin 8 ⊕ Fin 8) → ℂ) (ha : ∑ j : Fin 8,a (.inl j)*a (.inr j) = 0) :
        powerRankOneMatrix l a ∈ angularLie l := by
    …

    Mentions: OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.Control.powerRankOneMatrix, OAI.HarmonicCounterexample.Control.angularLie

82. lemma OAI.HarmonicCounterexample.Control.pderiv_commutes line 942
83. lemma OAI.HarmonicCounterexample.Control.pderiv_linearField line 952
84. lemma OAI.HarmonicCounterexample.Control.pderiv_twice_linearField line 964
85. lemma OAI.HarmonicCounterexample.Control.skew_hessian_sum line 973

    Source documentation

    Skew coefficients cancel against a genuinely symmetric Hessian.

    lemma skew_hessian_sum (M : Matrix ι ι 𝕜) (hM : ∀ i j,M i j = -M j i)
        (P : MvPolynomial ι 𝕜) [NoZeroSMulDivisors 𝕜 (MvPolynomial ι 𝕜)]
        [CharZero 𝕜] : ∑ i : ι,∑ j : ι,M i j • pderiv i (pderiv j P) = 0 := by
    …

86. lemma OAI.HarmonicCounterexample.ComplexAngular.mixedLaplacian_linearField line 1015

    Source documentation

    Preservation of the split Euclidean Laplacian by exactly the split-orthogonal infinitesimal fields, derived from their polynomial action.

    lemma mixedLaplacian_linearField (M : Matrix (ι ⊕ ι) (ι ⊕ ι) ℂ)
        (hM : ∀ i j,M j (Sum.swap i) = -M i (Sum.swap j))
        (P : SplitPolynomial ι) :
        mixedLaplacian (linearField M P) = linearField M (mixedLaplacian P) := by
    …

    Mentions: OAI.HarmonicCounterexample.ComplexAngular.SplitPolynomial, OAI.HarmonicCounterexample.ComplexAngular.mixedLaplacian

87. lemma OAI.HarmonicCounterexample.ComplexAngular.linearField_harmonic line 1038
88. def OAI.HarmonicCounterexample.Control.traceFreeEnd line 1067
89. lemma OAI.HarmonicCounterexample.Control.traceFreeEnd_eq_self line 1074
90. lemma OAI.HarmonicCounterexample.Control.traceFreeEnd_lie line 1077
91. lemma OAI.HarmonicCounterexample.Control.traceFreeEnd_one line 1084
92. lemma OAI.HarmonicCounterexample.Control.traceFreeEnd_sub_scalar line 1091
93. def OAI.HarmonicCounterexample.Control.liftedTraceLie line 1097

    Source documentation

    A matrix acts on the genuine subspace with trace-free restriction in L. The witness is an operator, not the desired controllability conclusion.

    def liftedTraceLie (i : W →ₗ[𝕜] V) (L : LieSubalgebra 𝕜 (Module.End 𝕜 W)) :
        LieSubalgebra 𝕜 (Module.End 𝕜 V) where
    …

94. lemma OAI.HarmonicCounterexample.Control.liftedTraceLie_restriction line 1122
95. lemma OAI.HarmonicCounterexample.ComplexAngular.X_pow_ne_zero_complex line 1153
96. instance OAI.HarmonicCounterexample.ComplexAngular.harmonicSpace_nontrivial line 1156
97. def OAI.HarmonicCounterexample.ComplexAngular.harmonicEmbedding line 1169
98. lemma OAI.HarmonicCounterexample.ComplexAngular.harmonicEmbedding_injective line 1172
99. def OAI.HarmonicCounterexample.ComplexAngular.harmonicField line 1176

    Source documentation

    The genuine harmonic restriction of an orthogonal angular field.

    def harmonicField (l : ℕ) (J : ComplexStructure (Fin 8 ⊕ Fin 8)) :
        Module.End ℂ (harmonicSpace (Fin 8) l) where
    …

    Mentions: OAI.HarmonicCounterexample.ComplexAngular.harmonicSpace

100. lemma OAI.HarmonicCounterexample.ComplexAngular.harmonicField_intertwine line 1183
101. def OAI.HarmonicCounterexample.Control.harmonicAngularLie line 1209

     Source documentation

     Exactly the trace-free squared angular-field Lie algebra on genuine harmonic polynomials. No irreducibility or controllability assumption is used.

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

102. lemma OAI.HarmonicCounterexample.Control.harmonicAngularLie_generator line 1214
103. lemma OAI.HarmonicCounterexample.Control.traceFree_apply line 1218
104. lemma OAI.HarmonicCounterexample.Control.angularRepresentation_toMatrix line 1221
105. lemma OAI.HarmonicCounterexample.Control.angularRepresentation_toEnd line 1226
106. lemma OAI.HarmonicCounterexample.Control.homogeneous_traceFree_restriction line 1232
107. lemma OAI.HarmonicCounterexample.Control.angularLie_harmonic_restriction line 1249

     Source documentation

     Every operator generated on homogeneous polynomials has precisely the trace-free restriction generated on the harmonic subspace.

     lemma angularLie_harmonic_restriction (l : ℕ)
         {A : Matrix (MonomialIndex (Fin 8 ⊕ Fin 8) l) (MonomialIndex (Fin 8 ⊕ Fin 8) l) ℂ}
         (hA : A ∈ angularLie l) :
         (LinearMap.toMatrixAlgEquiv (homogeneousBasis l)).symm A ∈
           liftedTraceLie (harmonicEmbedding l) (harmonicAngularLie l) := by
     …

     Mentions: OAI.HarmonicCounterexample.Control.MonomialIndex, OAI.HarmonicCounterexample.Control.angularLie, OAI.HarmonicCounterexample.Control.homogeneousBasis, OAI.HarmonicCounterexample.Control.liftedTraceLie, OAI.HarmonicCounterexample.Control.harmonicAngularLie

108. lemma OAI.HarmonicCounterexample.ComplexAngular.roundPairing_power_eval line 1281
109. lemma OAI.HarmonicCounterexample.Control.harmonicRankOne_intertwine line 1311
110. theorem OAI.HarmonicCounterexample.Control.harmonicAngularLie_rankones line 1325

     Source documentation

     Every genuine isotropic-power rank-one operator belongs to the Lie algebra of trace-free squares on the ACTUAL harmonic polynomial space.

     theorem harmonicAngularLie_rankones (l : ℕ) (hl : 2 ≤ l)
         (a : {a : (Fin 8 ⊕ Fin 8) → ℂ | MvPolynomial.eval a (quadric (Fin 8)) = 0}) :
         outer (roundPairing l) (isotropicPower l a) (isotropicPower l a) ∈ harmonicAngularLie l := by
     …

     Mentions: OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.Control.outer, OAI.HarmonicCounterexample.Control.harmonicAngularLie

111. theorem OAI.HarmonicCounterexample.Control.harmonicAngularLie_wedges line 1345

     Source documentation

     Full skew algebra producer on genuine harmonic polynomials, with the correct invariant symmetric form in split coordinates.

     theorem harmonicAngularLie_wedges (l : ℕ) (hl : 2 ≤ l)
         (u v : harmonicSpace (Fin 8) l) :
         wedgeLeft (roundPairing l) u v ∈ harmonicAngularLie l :=
     …

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

112. theorem OAI.HarmonicCounterexample.Control.exists_bilinear_orthonormal_basis line 1372

     Source documentation

     A symmetric nondegenerate complex bilinear form has a genuine normalized basis. This uses square roots in ℂ, not a positive-definiteness assumption.

     theorem exists_bilinear_orthonormal_basis
         (B : W →ₗ[ℂ] W →ₗ[ℂ] ℂ) (hB : ∀ x y,B x y = B y x)
         (hinj : Function.Injective B) :
         ∃ b : Basis (Fin (finrank ℂ W)) ℂ W,
           ∀ i j,B (b i) (b j) = if i=j then 1 else 0 := by
     …

     Mentions: OAI.HarmonicCounterexample.b

113. lemma OAI.HarmonicCounterexample.Control.bilin_basis_repr line 1422
114. lemma OAI.HarmonicCounterexample.Control.bilin_basis_pairing line 1429
115. lemma OAI.HarmonicCounterexample.Control.real_matrix_complex_orthogonal line 1436
116. theorem OAI.HarmonicCounterexample.Control.exists_bilinear_null_basis line 1445

     Source documentation

     An arbitrary nonzero null vector admits genuine normalized bilinear coordinates u=r(e_i+I e_j). The orthogonal change is constructed from its real and imaginary coefficient vectors.

     theorem exists_bilinear_null_basis (B : W →ₗ[ℂ] W →ₗ[ℂ] ℂ) (b : Basis ι ℂ W)
         (hb : ∀ i j,B (b i) (b j) = if i=j then 1 else 0)
         (i j : ι) (hij : i ≠ j) (u : W) (hu : B u u=0) (hn : u ≠ 0) :
         ∃ (b' : Basis ι ℂ W) (r : ℝ),0 < r ∧
           (∀ a c,B (b' a) (b' c) = if a=c then 1 else 0) ∧
            u = (r:ℂ) • (b' i+Complex.I • b' j) := by
     …

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