Finite Perron supplier: List

Abstract

Finite Perron supplier: List

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.

List splitting, duplicate detection and index transport support the shortest-path proof. These auxiliary facts are used in the path decomposition and repeated-vertex elimination; they are applications and proof organization, with no claim of new list mathematics.