Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Ky Fan gap definitions

Abstract

Ky Fan graph maxima and the asymptotic gap predicate.

Definition 1.1 (Ky Fan singular-value sum).

Lean statement: D5/S3/Combinatorics/Graph/KyFanGap/Defs.kyFan

Formalization. D5/S3/Combinatorics/Graph/KyFanGap/Defs.kyFan (✓ std3).

Citation. Jon Crall, Claude Fable 5, Claude Opus 4.8, GPT-5.6 Thinking, and GPT-5.6 High (2026). Formal rectangular singular-value variational bounds. URL: https://github.com/AIQ-Kitware/aiq-dkps-formalization/tree/64e234954217f3ca907ac980c8cbde2900109a66/ForTauCeti/Analysis/InnerProductSpace.

Commentary.

For a real square matrix, sum the first k singular values, with the natural zero extension.

Definition 1.2 (Finite graph maximum).

Lean statement: D5/S3/Combinatorics/Graph/KyFanGap/Defs.xi

Formalization. D5/S3/Combinatorics/Graph/KyFanGap/Defs.xi (✓ std3).

Citation. Vladimir Nikiforov (2015). Extrema of graph eigenvalues. URL: https://arxiv.org/abs/1502.00359v1.

Commentary.

The value xi k n is the maximum Ky Fan k sum over simple graphs on Fin n.

Definition 1.3 (Asymptotic gap predicate).

Lean statement: D5/S3/Combinatorics/Graph/KyFanGap/Defs.conjecture

Formalization. D5/S3/Combinatorics/Graph/KyFanGap/Defs.conjecture (✓ std3).

Citation. Vladimir Nikiforov (2015). Extrema of graph eigenvalues. URL: https://arxiv.org/abs/1502.00359v1.

Commentary.

Infinitely many indices have a limiting normalized graph maximum below the universal square-root bound.

References