OAI/NumberTheory/DukePrimeDegree/Dynamics/NoInvariantRootGraph.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Without invariant roots the positive-root graph has no two-step path

  1. lemma OAI.DukePrimeDegree.positive_coefficient_atomless line 14
  2. theorem OAI.DukePrimeDegree.no_two_step_positive_roots_of_no_invariant_root line 27

    Source documentation

    The commutator argument handles distinct endpoints; the isolated opposite-root pair is handled by the already proved low-entropy theorem.

    theorem no_two_step_positive_roots_of_no_invariant_root (d : ℕ) (hd : 2 < d+1)
    (μ : Measure (X (d+1))) [IsProbabilityMeasure μ]
    [ErgodicSMul (Multiplicative (LogCoordinates d)) (X (d+1)) μ]
    (hnone : ∀ (i j : Fin (d+1)) (hij : i ≠ j), ¬ ∀ t : ℝ,
      μ.map (fun x => rightAction x (Matrix.SpecialLinearGroup.transvection hij t))=μ) :
    ∀ a b c : Fin (d+1), 0 < canonicalRootCoefficient d μ a b →
      0 < canonicalRootCoefficient d μ b c → False := by
…

    Mentions: OAI.DukePrimeDegree.canonicalRootCoefficient