Finite Perron supplier: Spectrum

Abstract

Finite Perron supplier: Spectrum

Apache-2.0 source by Matteo Cipollina, or4nge19/MCMC at b901242fd04b6eff425a177e5c9bc6c56257bc62. The full Apache-2.0 license is reproduced in D5/S3/Combinatorics/Graph/PerronFrobenius/MCMCSupplier/Auxiliary.lean; the canonical supplier family retains the original copyright notices. Unused declarations are omitted and imports are relocated; the retained mathematical proof is reused without a novelty claim.

The finite-dimensional spectrum-to-eigenvector bridge extracts a nonzero vector from the nontrivial kernel of a nonunit linear map. The matrix-to-linear-map algebra equivalence preserves spectra. These consumed helpers support the complex spectral bound; the simplex nonemptiness helper supports compact maximization.