KE-04: strict interval occupancy in block Lanczos compression spectra
Recorded by the registry's curators from GitHub; the authors did not submit it here.
George Stepaniants
Complete formalization of the original block-Lanczos interval-occupancy conjecture, via the stronger full-prefix theorem and exact finite-dimensional real linear algebra.
Claims
Files and sources
- Paper
- OpenProblemsInNLA @ e375a6f, KE-04/lean/ ↗
- Lean bundle
- submissions/bundles/openproblemsinnla-ke-04-lean.tar.gz
- Toolchain
- leanprover/lean4:v4.33.1
- Posted on GitHub
- 13 September 2026
Verification PASSED
- Attempt
- 1
- Toolchain
- leanprover/lean4:v4.33.1
- Auditor
- v1 · modal
- lake build
- succeeded
- Kernel replay
- succeeded
- Duration
- 0:02:04.479311
Declarations audited
| Declaration | Kind | Axioms | Unused hypotheses | Canonical |
|---|---|---|---|---|
| NLA.KE04.blockLanczosConjecture | theorem · Prop | propext, Classical.choice, Quot.sound | none | matched |
| RegistryProblems.Problem_OP_00089 | definition | propext, Classical.choice, Quot.sound | none | no canonical statement |
NLA.KE04.blockLanczosConjecture
NLA.KE04.BlockLanczosConjecture
RegistryProblems.Problem_OP_00089
Prop
Build log
Quot.sound] info: NLA/KE04/Frames.lean:186:0: 'NLA.KE04._proved.inner_act_transpose' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Frames.lean:188:0: 'NLA.KE04._proved.frameProjection_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Frames.lean:190:0: 'NLA.KE04._proved.submodule_frame_exists' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Frames.lean:192:0: 'NLA.KE04._proved.krylovBasis_exists' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Frames.lean:194:0: 'NLA.KE04._proved.compression_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Frames.lean:196:0: 'NLA.KE04._proved.compressedQuadratic_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [2718/2726] Built NLA.KE04.Intersection (8.2s) info: NLA/KE04/Intersection.lean:38:0: 'NLA.KE04._proved.krylov_intersection_nonzero' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [2719/2726] Built NLA.KE04.Transport (10s) info: NLA/KE04/Transport.lean:141:0: 'NLA.KE04._proved.frame_coordinates' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Transport.lean:143:0: 'NLA.KE04._proved.frame_inner' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Transport.lean:145:0: 'NLA.KE04._proved.compression_action_coordinates' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Transport.lean:147:0: 'NLA.KE04._proved.quadratic_action_expansion' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Transport.lean:149:0: 'NLA.KE04._proved.quadratic_form_expansion' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Transport.lean:151:0: 'NLA.KE04._proved.compressed_form_expansion' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Transport.lean:153:0: 'NLA.KE04._proved.compressed_action_identity' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Transport.lean:155:0: 'NLA.KE04._proved.quadratic_forms_agree' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Transport.lean:157:0: 'NLA.KE04._proved.later_quadratic_identity' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Transport.lean:159:0: 'NLA.KE04._proved.interval_index_validity' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Transport.lean:161:0: 'NLA.KE04._proved.fullPrefix_implies_canonical' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [2720/2726] Built NLA.KE04.Nonannihilation (10s) info: NLA/KE04/Nonannihilation.lean:123:0: 'NLA.KE04._proved.blockExtend' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Nonannihilation.lean:125:0: 'NLA.KE04._proved.blockShift' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Nonannihilation.lean:127:0: 'NLA.KE04._proved.krylovCombination_extend' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Nonannihilation.lean:129:0: 'NLA.KE04._proved.krylovCombination_shift' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Nonannihilation.lean:131:0: 'NLA.KE04._proved.blockShift_eq_smul_extend' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Nonannihilation.lean:133:0: 'NLA.KE04._proved.fullRank_krylov_eigenvector_zero' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Nonannihilation.lean:135:0: 'NLA.KE04._proved.act_sub_smul_one' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Nonannihilation.lean:137:0: 'NLA.KE04._proved.fullRank_quadratic_nonannihilation' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [2721/2726] Built NLA.KE04.SpectralWindow (4.4s) info: NLA/KE04/SpectralWindow.lean:136:0: 'NLA.KE04._proved.compression_basis_independent' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/SpectralWindow.lean:137:0: 'NLA.KE04._proved.orthonormal_span_form_nonpos' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/SpectralWindow.lean:138:0: 'NLA.KE04._proved.spectral_window_subspace' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [2722/2726] Built NLA.KE04.Completion (4.1s) info: NLA/KE04/Completion.lean:76:0: 'NLA.KE04._proved.psd_form_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Completion.lean:77:0: 'NLA.KE04._proved.strictIntervalOccupancy' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Completion.lean:78:0: 'NLA.KE04._proved.blockLanczosConjecture' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [2723/2726] Built NLA.KE04.Proof (4.5s) info: NLA/KE04/Proof.lean:169:0: 'NLA.KE04.real_matrix_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Proof.lean:171:0: 'NLA.KE04.krylov_range_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Proof.lean:173:0: 'NLA.KE04.krylov_nesting_and_shift' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Proof.lean:175:0: 'NLA.KE04.fullBlockDimension_iff_independent' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Proof.lean:177:0: 'NLA.KE04.fullBlockDimension_prefix' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Proof.lean:179:0: 'NLA.KE04.lastFullBlockIteration_exists' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Proof.lean:181:0: 'NLA.KE04.krylovBasis_exists' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Proof.lean:183:0: 'NLA.KE04.frameProjection_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Proof.lean:185:0: 'NLA.KE04.compression_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Proof.lean:187:0: 'NLA.KE04.orderedSpectrum_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Proof.lean:189:0: 'NLA.KE04.compression_basis_independent' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Proof.lean:191:0: 'NLA.KE04.interval_index_validity' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Proof.lean:193:0: 'NLA.KE04.quadratic_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Proof.lean:195:0: 'NLA.KE04.spectral_gap_quadratic_psd' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Proof.lean:197:0: 'NLA.KE04.spectral_window_subspace' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Proof.lean:199:0: 'NLA.KE04.krylov_intersection_nonzero' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Proof.lean:201:0: 'NLA.KE04.psd_zero_form_iff_kernel' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Proof.lean:203:0: 'NLA.KE04.compressedQuadratic_semantics' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Proof.lean:205:0: 'NLA.KE04.quadratic_forms_agree' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Proof.lean:207:0: 'NLA.KE04.later_quadratic_identity' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Proof.lean:209:0: 'NLA.KE04.fullRank_quadratic_nonannihilation' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Proof.lean:211:0: 'NLA.KE04.strictIntervalOccupancy' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Proof.lean:213:0: 'NLA.KE04.fullPrefix_implies_canonical' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/KE04/Proof.lean:215:0: 'NLA.KE04.blockLanczosConjecture' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [2724/2726] Built Solution (3.5s) ✔ [2725/2726] Built RegistryRecord (3.6s) Build completed successfully (2726 jobs).