NeutralBlockVelocity.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Actual neutral block directions in the measure stabilizer

Full diagonal invariance and invariance under the roots within equal-weight blocks give every trace-zero neutral matrix as the derivative of a curve in the actual stabilizer. Exponential recovery then gives its entire one-parameter group. This is only the neutral-group input: it does not construct a singular parabolic chart or an atomic conditional graph.

lemma OAI.DukePrimeDegree.hasIdentityMatrixDerivative_diagonalOneParameter line 25

theorem OAI.DukePrimeDegree.neutral_matrix_mem_velocitySpace line 43

Source documentation

All neutral infinitesimal directions arise from actual subgroup curves; a Lie algebra is not assigned as an additional hypothesis.

theorem neutral_matrix_mem_velocitySpace {n : ℕ}
    (ell : Fin n → ℝ) (L : Subgroup (G n))
    (hdiag : ∀ (v : Fin n → ℝ) (hv : ∑ i, v i = 0) (t : ℝ),
      diagonalOneParameter v hv t ∈ L)
    (hroot : ∀ (i j : Fin n) (hij : i ≠ j), ell i = ell j →
      ∀ t : ℝ, SpecialLinearGroup.transvection hij t ∈ L)
    (V : Matrix (Fin n) (Fin n) ℝ) (htrace : Matrix.trace V = 0)
    (hneutral : ∀ i j, ell i ≠ ell j → V i j = 0) :
    V ∈ matrixVelocitySpace L := by
…

Mentions: OAI.DukePrimeDegree.matrixVelocitySpace

lemma OAI.DukePrimeDegree.neutral_matrix_conjugation_fixed line 83

Source documentation

The infinitesimal support condition really is neutrality for the chosen singular diagonal flow.

lemma neutral_matrix_conjugation_fixed {n : ℕ}
    (ell : Fin n → ℝ) (hell : ∑ i, ell i = 0)
    (V : Matrix (Fin n) (Fin n) ℝ)
    (hneutral : ∀ i j, ell i ≠ ell j → V i j = 0) (t : ℝ) :
    (diagonalOneParameter ell hell t).val * V *
      (diagonalOneParameter ell hell (-t)).val = V := by
…

theorem OAI.DukePrimeDegree.neutral_matrix_exp_mem_stabilizer line 95