Perron-Frobenius for irreducible nonnegative matrices

irreducible_nonnegative_matrix_has_positive_eigenvector_at_spectralRadius

Submitter: Kim Morrison.

Notes: A Perron-Frobenius style eigenvector existence statement at the spectral radius.

Source: Classical theorem in linear algebra.

Informal solution: Show that an irreducible nonnegative matrix has a strictly positive eigenvector with eigenvalue equal to its spectral radius.

theorem declaration uses `sorry`irreducible_nonnegative_matrix_has_positive_eigenvector_at_spectralRadius {n : Type*} [Fintype n] [DecidableEq n] [Nonempty n]
    (A : Matrix n n ℝ)
    (hA : A.IsIrreducible) :
    ∃ v : n → ℝ,
      Module.End.HasEigenvector (Matrix.toLin' A) (spectralRadius ℝ A).toReal v ∧
      (∀ i, 0 < v i) := byn:Type u_1inst✝²:Fintype ninst✝¹:DecidableEq ninst✝:Nonempty nA:Matrix n n ℝhA:A.IsIrreducible⊢ ∃ v, Module.End.HasEigenvector (Matrix.toLin' A) (spectralRadius ℝ A).toReal v ∧ ∀ (i : n), 0 < v i
  sorryAll goals completed! 🐙

Solved by

• @LorenzoLuccioli with Aristotle (Harmonic) on May 9, 2026 (proof)

• @antpavzhi with Aleph Prover(logicalintelligence.com) on May 11, 2026

• @daouid with Antigravity (Multi-Model Ensemble: Gemini 3.1 Pro, Gemini 3 Flash, Claude 4.6 Sonnet/Opus) on May 13, 2026 (proof)

• @A-M-Berns with GPT-5.5 on May 16, 2026 (proof)

• @GanjinZero with Seed Prover (ByteDance) on May 20, 2026