OAI/Geometry/HarmonicGrowth/LieGeneration.lean

GitHub source file

106 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicCounterexample.Control.bracket_diagonal_apply line 19
2. def OAI.HarmonicCounterexample.Control.filterEntry line 25

   Source documentation

   A normalized factor of a polynomial in a diagonal adjoint operator.

   def filterEntry (d : ι → 𝕜) (p q i j : ι) (X : Matrix ι ι 𝕜) : Matrix ι ι 𝕜 :=
   …

3. lemma OAI.HarmonicCounterexample.Control.filterEntry_apply line 28
4. lemma OAI.HarmonicCounterexample.Control.filterEntry_mem line 34
5. theorem OAI.HarmonicCounterexample.Control.isolate_entry line 42

   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 (L : LieSubalgebra 𝕜 (Matrix ι ι 𝕜))
       (d : κ → ι → 𝕜) (hd : ∀ a,diagonal (d a) ∈ 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

6. lemma OAI.HarmonicCounterexample.Control.normalize_entry line 79
7. theorem OAI.HarmonicCounterexample.Control.weight_separation line 104

   Source documentation

   The joint weight differences of the diagonal quadratic operators are injective as soon as the shift has three nonzero coordinates.

   theorem weight_separation (δ v : ι → 𝕜)
       (a b c : ι) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c)
       (ha : δ a ≠ 0) (hb : δ b ≠ 0) (hc : δ c ≠ 0)
       (h : ∀ i j, i ≠ j → v i * δ j + v j * δ i = 0) : v = 0 := by
   …

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

8. lemma OAI.HarmonicCounterexample.Control.quadratic_weight_difference line 123
9. theorem OAI.HarmonicCounterexample.Control.joint_weight_injective line 128

   Source documentation

   The exact joint eigenvalues in manuscript (control-block-eigenvalues).

   theorem joint_weight_injective (δ : ι → 𝕜)
       (a b c : ι) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c)
       (ha : δ a ≠ 0) (hb : δ b ≠ 0) (hc : δ c ≠ 0)
       {ν μ : ι → 𝕜}
       (h : ∀ i j, i ≠ j →
         ν i*δ j+ν j*δ i+δ i*δ j = μ i*δ j+μ j*δ i+δ i*δ j) : ν = μ := by
   …

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

10. lemma OAI.HarmonicCounterexample.Control.bracket_units line 160
11. theorem OAI.HarmonicCounterexample.Control.unit_mem_of_path line 167

    Source documentation

    Nested brackets along a nonreturning directed path produce the endpoint unit. No associative multiplication closure of the Lie algebra is assumed.

    theorem unit_mem_of_path (L : LieSubalgebra 𝕜 (Matrix ι ι 𝕜))
        (v : ℕ → ι) (r : ℕ) (hr : 0 < r)
        (hne : ∀ j,0 < j → j ≤ r → v j ≠ v 0)
        (hedge : ∀ j,j < r → single (v (j+1)) (v j) (1:𝕜) ∈ L) :
        single (v r) (v 0) (1:𝕜) ∈ L := by
    …

12. lemma OAI.HarmonicCounterexample.Control.diagonal_difference_mem line 185
13. theorem OAI.HarmonicCounterexample.Control.extreme_weight_unique line 212

    Source documentation

    On the extreme weight layer there is no opposite pair. Equality of torus weight and total polynomial degree therefore determines the actual monomial, even among all (not necessarily harmonic) monomials.

    theorem extreme_weight_unique (d e : ι ⊕ ι → ℕ)
        (he : ∀ i,e (.inl i) = 0 ∨ e (.inr i) = 0)
        (hdeg : ∑ a,d a = ∑ a,e a)
        (hweight : ∀ i,(d (.inl i):ℤ)-d (.inr i) = e (.inl i)-e (.inr i)) : d = e := by
    …

    Mentions: OAI.HarmonicCounterexample.a

14. theorem OAI.HarmonicCounterexample.Control.extreme_joint_separation line 227

    Source documentation

    At a three-coordinate shift, linear torus differences and pairwise quadratic torus differences distinguish an extreme-to-extreme entry from EVERY other matrix entry. Thus weight multiplicities in the interior cannot silently turn a block into a rank-one operator.

    theorem extreme_joint_separation
        {𝕜 : Type*} [Field 𝕜] [CharZero 𝕜]
        {μ : Type*} (w : μ → ι → 𝕜) (p q : μ)
        (hp : ∀ x,w x = w p → x = p) (hq : ∀ x,w x = w q → x = q)
        (a b c : ι) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c)
        (ha : w p a-w q a ≠ 0) (hb : w p b-w q b ≠ 0) (hc : w p c-w q c ≠ 0)
        (x y : μ) (hxy : (x,y) ≠ (p,q)) :
        (∃ i,w p i-w q i ≠ w x i-w y i) ∨
        ∃ i j,i ≠ j ∧ w p i*w p j-w q i*w q j ≠ w x i*w x j-w y i*w y j := by
    …

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

15. lemma OAI.HarmonicCounterexample.Control.filterEntry_mem_normalizer line 270
16. theorem OAI.HarmonicCounterexample.Control.isolate_entry_normalizers line 278

    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_normalizers (L : LieSubalgebra 𝕜 (Matrix ι ι 𝕜))
        (d : κ → ι → 𝕜) (hd : ∀ a X, X ∈ L → ⁅diagonal (d a),X⁆ ∈ 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

17. def OAI.HarmonicCounterexample.Control.ExtremeMonomial line 337
18. lemma OAI.HarmonicCounterexample.Control.extreme_monomial_weight_unique line 340
19. theorem OAI.HarmonicCounterexample.Control.angularLie_extreme_entry line 356

    Source documentation

    Every nonzero actual extreme-to-extreme coefficient at a shift with three nonzero coordinates yields a matrix unit in the actual angular Lie algebra.

    theorem angularLie_extreme_entry
        (X : Matrix (MonomialIndex (Fin s ⊕ Fin s) l) (MonomialIndex (Fin s ⊕ Fin s) l) ℂ)
        (hX : X ∈ angularLie l) (μ ν : MonomialIndex (Fin s ⊕ Fin s) l)
        (hμ : ExtremeMonomial μ) (hν : ExtremeMonomial ν)
        (a b c : Fin s) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c)
        (ha : monomialWeight μ.1 a-monomialWeight ν.1 a ≠ 0)
        (hb : monomialWeight μ.1 b-monomialWeight ν.1 b ≠ 0)
        (hc : monomialWeight μ.1 c-monomialWeight ν.1 c ≠ 0)
        (he : X μ ν ≠ 0) : single μ ν (1:ℂ) ∈ angularLie l := by
    …

    Mentions: OAI.HarmonicCounterexample.Control.MonomialIndex, OAI.HarmonicCounterexample.Control.angularLie, OAI.HarmonicCounterexample.Control.ExtremeMonomial, OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.Control.monomialWeight

20. def OAI.HarmonicCounterexample.Control.secondExponent line 402

    Source documentation

    Exponents of a genuine term in the second-order polynomial field.

    def secondExponent (ν : ι →₀ ℕ) (a b c d : ι) : ι →₀ ℕ :=
    …

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

21. lemma OAI.HarmonicCounterexample.Control.split_forces_derivatives line 407

    Source documentation

    A deficit of two forces both differentiated variables. Natural truncated subtraction is handled rather than tacitly converted to a Laurent model.

    lemma split_forces_derivatives (ν : ι →₀ ℕ) (i j k a b c d : ι)
        (hn : 2 ≤ ν i) (hij : i ≠ j) (hik : i ≠ k)
        (he : secondExponent ν a b c d = secondExponent ν i i j k) : a = i ∧ b = i := by
    …

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

22. lemma OAI.HarmonicCounterexample.Control.split_forces_replacements line 421

    Source documentation

    Once the differentiated variables are known, the increment at two distinct coordinates forces precisely the two ordered replacements.

    lemma split_forces_replacements (ν : ι →₀ ℕ) (i j k c d : ι)
        (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k)
        (he : secondExponent ν i i c d = secondExponent ν i i j k) :
        (c = j ∧ d = k) ∨ (c = k ∧ d = j) := by
    …

    Mentions: OAI.HarmonicCounterexample.Control.secondExponent

23. def OAI.HarmonicCounterexample.Control.secondField line 455

    Source documentation

    The genuine second-order contribution, with every ordered differentiation and replacement included.

    def secondField (M : Matrix ι ι 𝕜) (P : MvPolynomial ι 𝕜) : MvPolynomial ι 𝕜 :=
    …

24. lemma OAI.HarmonicCounterexample.Control.linearField_square_second line 459
25. lemma OAI.HarmonicCounterexample.Control.secondField_monomial line 467
26. lemma OAI.HarmonicCounterexample.Control.secondField_coeff line 475
27. lemma OAI.HarmonicCounterexample.Control.secondExponent_split_iff line 502
28. lemma OAI.HarmonicCounterexample.Control.secondField_split_coeff line 515
29. lemma OAI.HarmonicCounterexample.Control.merge_forces_derivatives line 562
30. lemma OAI.HarmonicCounterexample.Control.merge_forces_replacements line 585
31. lemma OAI.HarmonicCounterexample.Control.secondExponent_merge_iff line 596
32. lemma OAI.HarmonicCounterexample.Control.secondField_merge_coeff line 613
33. lemma OAI.HarmonicCounterexample.Control.split_exponent_ne line 657
34. lemma OAI.HarmonicCounterexample.Control.merge_exponent_ne line 667
35. lemma OAI.HarmonicCounterexample.Control.fieldSquare_split_coeff line 676
36. lemma OAI.HarmonicCounterexample.Control.fieldSquare_merge_coeff line 686
37. lemma OAI.HarmonicCounterexample.Control.signedIndex_ne line 716
38. lemma OAI.HarmonicCounterexample.Control.coordinateSign_ne_zero line 720
39. lemma OAI.HarmonicCounterexample.Control.traceFree_offdiagonal line 723
40. lemma OAI.HarmonicCounterexample.Control.angularSquare_entry line 727
41. lemma OAI.HarmonicCounterexample.Control.angularSquare_split_coefficient line 737

    Source documentation

    The manuscript's actual split coefficient. Its nonvanishing is not an assumption about a spectral surrogate.

    lemma angularSquare_split_coefficient (i j k : Fin s)
        (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k) (ε β γ : Bool)
        (μ ν : MonomialIndex (Fin s ⊕ Fin s) l)
        (hn : 2 ≤ ν.1 (signedIndex i ε))
        (hμ : μ.1 = secondExponent ν.1 (signedIndex i ε) (signedIndex i ε)
          (signedIndex j β) (signedIndex k γ)) :
        traceFree (angularRepresentation l (triple i j k).matrix*
          angularRepresentation l (triple i j k).matrix) μ ν =
          Complex.I*coordinateSign (signedIndex i ε)/2*
            (ν.1 (signedIndex i ε):ℂ)*((ν.1 (signedIndex i ε)-1:ℕ):ℂ) := by
    …

    Mentions: OAI.HarmonicCounterexample.Control.MonomialIndex, OAI.HarmonicCounterexample.Control.secondExponent, OAI.HarmonicCounterexample.Control.traceFree, OAI.HarmonicCounterexample.Control.angularRepresentation

42. lemma OAI.HarmonicCounterexample.Control.angularSquare_split_nonzero line 761
43. lemma OAI.HarmonicCounterexample.Control.angularSquare_merge_coefficient line 774
44. lemma OAI.HarmonicCounterexample.Control.angularSquare_merge_nonzero line 798
45. lemma OAI.HarmonicCounterexample.Control.monomialWeight_eq_int line 831
46. lemma OAI.HarmonicCounterexample.Control.split_three_weight_shifts line 837
47. lemma OAI.HarmonicCounterexample.Control.merge_three_weight_shifts line 860
48. theorem OAI.HarmonicCounterexample.Control.angularLie_legal_split line 885

    Source documentation

    Both directions of each legal token split are genuinely generated by squared orthogonal complex structures. Endpoints are actual homogeneous monomials.

    theorem angularLie_legal_split (i j k : Fin s)
        (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k) (ε β γ : Bool)
        (μ ν : MonomialIndex (Fin s ⊕ Fin s) l)
        (hexμ : ExtremeMonomial μ) (hexν : ExtremeMonomial ν)
        (hn : 2 ≤ ν.1 (signedIndex i ε))
        (hμ : μ.1 = secondExponent ν.1 (signedIndex i ε) (signedIndex i ε)
          (signedIndex j β) (signedIndex k γ)) :
        single μ ν (1:ℂ) ∈ angularLie l := by
    …

    Mentions: OAI.HarmonicCounterexample.Control.MonomialIndex, OAI.HarmonicCounterexample.Control.ExtremeMonomial, OAI.HarmonicCounterexample.Control.secondExponent, OAI.HarmonicCounterexample.Control.angularLie

49. theorem OAI.HarmonicCounterexample.Control.angularLie_legal_merge line 898
50. def OAI.HarmonicCounterexample.Control.branchExponent line 932

    Source documentation

    The explicit manuscript token branch, specialized to the n=16 witness.

    def branchExponent (ε : Bool) (h r t : ℕ) : Fin 8 ⊕ Fin 8 →₀ ℕ :=
    …

51. lemma OAI.HarmonicCounterexample.Control.branchExponent_degree line 935
52. def OAI.HarmonicCounterexample.Control.branchMonomial line 940
53. lemma OAI.HarmonicCounterexample.Control.branchMonomial_extreme line 944
54. lemma OAI.HarmonicCounterexample.Control.branchMonomial_coordinate line 957
55. lemma OAI.HarmonicCounterexample.Control.branchMonomial_distinct line 961
56. lemma OAI.HarmonicCounterexample.Control.branchMonomial_pair_count line 968
57. lemma OAI.HarmonicCounterexample.Control.branchMonomial_split line 973
58. lemma OAI.HarmonicCounterexample.Control.branchMonomial_merge line 987
59. lemma OAI.HarmonicCounterexample.Control.angularLie_branch_edges line 1001
60. lemma OAI.HarmonicCounterexample.Control.angularLie_branch_endpoints line 1018
61. def OAI.HarmonicCounterexample.Control.pureMonomial line 1058
62. lemma OAI.HarmonicCounterexample.Control.pureMonomial_ne line 1061
63. lemma OAI.HarmonicCounterexample.Control.branchMonomial_start line 1067
64. lemma OAI.HarmonicCounterexample.Control.evenBranch_common line 1072
65. lemma OAI.HarmonicCounterexample.Control.angularLie_even_endpoint line 1077
66. def OAI.HarmonicCounterexample.Control.oddEndpoint line 1088

    Source documentation

    Common vertex of the two odd branches, using the fourth coordinate plane.

    def oddEndpoint (h : ℕ) (hh : 0 < h) : MonomialIndex (Fin 8 ⊕ Fin 8) (2*h+1) :=
    …

    Mentions: OAI.HarmonicCounterexample.Control.MonomialIndex

67. lemma OAI.HarmonicCounterexample.Control.oddEndpoint_extreme line 1093
68. lemma OAI.HarmonicCounterexample.Control.oddEndpoint_ne_pure line 1098
69. lemma OAI.HarmonicCounterexample.Control.oddEndpoint_merge line 1105
70. lemma OAI.HarmonicCounterexample.Control.oddEndpoint_split line 1119
71. lemma OAI.HarmonicCounterexample.Control.angularLie_odd_last_edges line 1133
72. lemma OAI.HarmonicCounterexample.Control.angularLie_odd_branch_endpoints line 1148
73. lemma OAI.HarmonicCounterexample.Control.angularLie_odd_endpoint line 1162
74. theorem OAI.HarmonicCounterexample.Control.angularLie_endpoint line 1172

    Source documentation

    A genuine rank-one endpoint unit on every degree needed in the n=16 construction. This is produced, not hypothesized.

    theorem angularLie_endpoint (l : ℕ) (hl : 2 ≤ l) :
        single (pureMonomial true l) (pureMonomial false l) (1:ℂ) ∈ angularLie l := by
    …

    Mentions: OAI.HarmonicCounterexample.Control.pureMonomial, OAI.HarmonicCounterexample.Control.angularLie

75. def OAI.HarmonicCounterexample.Control.linearChange line 1202

    Source documentation

    Actual substitution of a linear coordinate motion in a polynomial.

    def linearChange (M : Matrix ι ι 𝕜) : MvPolynomial ι 𝕜 →ₐ[𝕜] MvPolynomial ι 𝕜 :=
    …

76. lemma OAI.HarmonicCounterexample.Control.linearChange_X line 1206
77. lemma OAI.HarmonicCounterexample.Control.linearChange_one line 1209
78. lemma OAI.HarmonicCounterexample.Control.linearChange_comp line 1215
79. lemma OAI.HarmonicCounterexample.Control.linearChange_linearField_X line 1224
80. lemma OAI.HarmonicCounterexample.Control.linearChange_linearField line 1237
81. lemma OAI.HarmonicCounterexample.Control.linearChange_homogeneous line 1246
82. def OAI.HarmonicCounterexample.Control.homogeneousChange line 1255
83. lemma OAI.HarmonicCounterexample.Control.homogeneousChange_apply_val line 1262
84. lemma OAI.HarmonicCounterexample.Control.homogeneousChange_one line 1266
85. lemma OAI.HarmonicCounterexample.Control.homogeneousChange_mul line 1274
86. lemma OAI.HarmonicCounterexample.Control.homogeneousChange_field line 1280
87. def OAI.HarmonicCounterexample.Control.homogeneousChangeMatrix line 1286
88. lemma OAI.HarmonicCounterexample.Control.homogeneousChangeMatrix_one line 1290
89. lemma OAI.HarmonicCounterexample.Control.homogeneousChangeMatrix_mul line 1294
90. lemma OAI.HarmonicCounterexample.Control.homogeneousChangeMatrix_field line 1299
91. def OAI.HarmonicCounterexample.Berger.ComplexStructure.orthogonalConjugate line 1326

    Source documentation

    Orthogonal coordinate conjugation, including both orientation components.

    def orthogonalConjugate (J : ComplexStructure ι) (R : Matrix ι ι ℝ)
        (hR : Rᵀ*R = 1) : ComplexStructure ι where
    …

    Mentions: OAI.HarmonicCounterexample.Berger.ComplexStructure

92. lemma OAI.HarmonicCounterexample.Berger.ComplexStructure.splitFieldMatrix_one line 1341
93. lemma OAI.HarmonicCounterexample.Control.matrix_conjugate_traceFree line 1367
94. lemma OAI.HarmonicCounterexample.Control.matrix_conjugate_lie line 1374
95. lemma OAI.HarmonicCounterexample.Control.conjugation_lieSpan line 1380

    Source documentation

    Conjugation closure follows from closure of the actual generators.

    lemma conjugation_lieSpan (T : Set (Matrix ι ι 𝕜)) (G H : Matrix ι ι 𝕜) (hHG : H*G = 1)
        (hT : ∀ A ∈ T,G*A*H ∈ LieSubalgebra.lieSpan 𝕜 _ T) :
        ∀ A ∈ LieSubalgebra.lieSpan 𝕜 _ T,G*A*H ∈ LieSubalgebra.lieSpan 𝕜 _ T := by
    …

96. def OAI.HarmonicCounterexample.Control.angularChange line 1397
97. lemma OAI.HarmonicCounterexample.Control.angularChange_orthogonal line 1400
98. lemma OAI.HarmonicCounterexample.Control.angularChange_field line 1405
99. lemma OAI.HarmonicCounterexample.Control.angularLie_orthogonal_conjugate line 1422
100. lemma OAI.HarmonicCounterexample.Berger.ComplexStructure.splitFieldMatrix_apply line 1458
101. lemma OAI.HarmonicCounterexample.Berger.ComplexStructure.splitFieldMatrix_skew line 1471
102. lemma OAI.HarmonicCounterexample.Control.orthogonalMatrix_two_rows line 1504

     Source documentation

     Extension of an actual ordered real orthonormal two-frame to an orthogonal coordinate matrix. Both orientation classes are intentionally allowed.

     lemma orthogonalMatrix_two_rows (i j : ι) (hij : i ≠ j)
         (u v : EuclideanSpace ℝ ι)
         (hu : inner ℝ u u = 1) (hv : inner ℝ v v = 1) (huv : inner ℝ u v = 0) :
         ∃ R : Matrix ι ι ℝ,Rᵀ*R = 1 ∧ (∀ a,R i a = u a) ∧ (∀ a,R j a = v a) := by
     …

     Mentions: OAI.HarmonicCounterexample.a

103. lemma OAI.HarmonicCounterexample.Control.complex_null_parts line 1556
104. lemma OAI.HarmonicCounterexample.Control.nullVector_orthogonal_frame line 1574

     Source documentation

     Every nonzero complex-null vector really is a scalar multiple of an orthogonal real two-frame; this is not an orbit-transitivity assumption.

     lemma nullVector_orthogonal_frame (i j : ι) (hij : i ≠ j)
         (z : ι → ℂ) (hz : ∑ a : ι,z a*z a = 0) (hn : z ≠ 0) :
         ∃ (r : ℝ) (R : Matrix ι ι ℝ),0 < r ∧ Rᵀ*R = 1 ∧
           ∀ a,z a = (r:ℂ)*((R i a:ℂ)+Complex.I*(R j a:ℂ)) := by
     …

     Mentions: OAI.HarmonicCounterexample.a

105. lemma OAI.HarmonicCounterexample.Berger.ComplexStructure.splitFieldMatrix_transpose line 1637
106. lemma OAI.HarmonicCounterexample.Control.split_null_row_orbit line 1668

     Source documentation

     The null cone in complex split coordinates is the actual real orthogonal orbit of the first isotropic coordinate, up to a nonzero real scale.

     lemma split_null_row_orbit (i : Fin s) (a : (Fin s ⊕ Fin s) → ℂ)
         (ha : ∑ j : Fin s,a (.inl j)*a (.inr j) = 0) (hn : a ≠ 0) :
         ∃ (r : ℝ) (R : Matrix (Fin s ⊕ Fin s) (Fin s ⊕ Fin s) ℝ),
           0 < r ∧ Rᵀ*R = 1 ∧ ∀ b,a b = (r:ℂ)*splitFieldMatrix R (.inl i) b := by
     …

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