bibkey: mathlib2026gelfandandivt authors: The mathlib community year: 2026 title: Gelfand formula and the intermediate value theorem in mathlib doi: null url: https://github.com/leanprover-community/mathlib4/tree/db584cd6d46c92f209a44c0f1c829460d327499d claim: The norm-power limit equals the complex spectral radius, and a continuous real function on a closed interval attains every value between its endpoint values. strata_touched: [] license: Apache-2.0, citation-only triage: anchor

Classical spectral and continuity tools

The Gelfand formula is used through spectrum.pow_norm_pow_one_div_tendsto_nhds_spectralRadius in Mathlib/Analysis/Normed/Algebra/GelfandFormula.lean. The intermediate value theorem is used through intermediate_value_Icc in Mathlib/Topology/Order/IntermediateValue.lean. These classical tools supply the analytic limits and scalar root existence step. The reset-codebook common-realization chain and its original 6/20 pruned graph are derived from the source-completion dynamics model; they are not attributed to those classical theorems.

Verified locator

https://github.com/leanprover-community/mathlib4/tree/db584cd6d46c92f209a44c0f1c829460d327499d