MF-22: eventual polynomial conditioning of the cubic C1 Toeplitz family

Claims

Files and sources

Paper

OpenProblemsInNLA @ e375a6f, MF-22/lean/ ↗

Lean bundle

submissions/bundles/openproblemsinnla-mf-22-lean.tar.gz

Toolchain

leanprover/lean4:v4.33.1

Posted on GitHub

16 September 2026

Verification PASSED

Attempt

1

Toolchain

leanprover/lean4:v4.33.1

Auditor

v1 · modal

lake build

succeeded

Kernel replay

succeeded

Duration

0:03:46.869842

Declarations audited

Declaration	Kind	Axioms	Unused hypotheses	Canonical
NLA.MF22.polynomial_conditioning	theorem · Prop	propext, Classical.choice, Quot.sound	none	matched
RegistryProblems.Problem_OP_00097	definition	propext, Classical.choice, Quot.sound	none	no canonical statement

NLA.MF22.polynomial_conditioning

∀ (ρ : Real), Real.instLT.lt 0 ρ → Exists fun K => Exists fun α => And (Real.instLT.lt 0 K) (And (Real.instLE.le 0 α) (Exists fun n0 => And (instLENat.le 1 n0) (∀ (n : Nat), instLENat.le n0 n → And (Ne (Matrix.det (NLA.MF22.toeplitz ρ n)) 0) (ENNReal.instLE.le (NLA.MF22.conditionNumber (NLA.MF22.toeplitz ρ n)) (ENNReal.ofReal (instHMul.hMul K (n.cast.rpow α)))))))

RegistryProblems.Problem_OP_00097

Prop

Build log

c1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: NLA/MF22/TransferCertificates.lean:144:80: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: NLA/MF22/TransferCertificates.lean:157:43: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: NLA/MF22/TransferCertificates.lean:158:77: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: NLA/MF22/TransferCertificates.lean:159:12: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: NLA/MF22/TransferCertificates.lean:159:81: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
info: NLA/MF22/TransferCertificates.lean:171:0: 'NLA.MF22.transfer_polynomial_certificates' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3678/3688] Built NLA.MF22.ProjectorRank (9.3s)
info: NLA/MF22/ProjectorRank.lean:105:0: 'NLA.MF22.transfer_eigenspace_finrank_le_one_of_charpoly' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/MF22/ProjectorRank.lean:107:0: 'NLA.MF22.spectralProjector_entry_minor_zero_of_charpoly' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/MF22/ProjectorRank.lean:109:0: 'NLA.MF22.spectralProjector_boundary_sandwich_of_charpoly' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3679/3688] Built NLA.MF22.GreenCoefficients (8.9s)
warning: NLA/MF22/GreenCoefficients.lean:37:30: Unused tactic linter: `ring` does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: NLA/MF22/GreenCoefficients.lean:37:30: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: NLA/MF22/GreenCoefficients.lean:42:30: Unused tactic linter: `ring` does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: NLA/MF22/GreenCoefficients.lean:42:30: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: NLA/MF22/GreenCoefficients.lean:82:60: Unused tactic linter: `ring` does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: NLA/MF22/GreenCoefficients.lean:82:60: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
info: NLA/MF22/GreenCoefficients.lean:124:0: 'NLA.MF22.green_leading_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3680/3688] Built NLA.MF22.GreenInverse (9.7s)
warning: NLA/MF22/GreenInverse.lean:65:36: Variable name `hρ` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hρ

Note: This linter can be disabled with `set_option linter.unusedVariables false`
info: NLA/MF22/GreenInverse.lean:132:0: 'NLA.MF22.green_source_state' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/MF22/GreenInverse.lean:134:0: 'NLA.MF22.green_inverse' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3681/3688] Built NLA.MF22.SpectralAlgebra (6.0s)
info: NLA/MF22/SpectralAlgebra.lean:33:0: 'NLA.MF22.spectral_projector_algebra' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3682/3688] Built NLA.MF22.Dominant (4.8s)
info: NLA/MF22/Dominant.lean:116:0: 'NLA.MF22.dominant_projector' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3683/3688] Built NLA.MF22.SpectralTailBounds (4.5s)
info: NLA/MF22/SpectralTailBounds.lean:110:0: 'NLA.MF22.spectral_tail_bounds_of_gamma' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/MF22/SpectralTailBounds.lean:112:0: 'NLA.MF22.spectral_tail_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3684/3688] Built NLA.MF22.GreenEntryBounds (5.1s)
warning: NLA/MF22/GreenEntryBounds.lean:120:29: Unused tactic linter: `ring` does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: NLA/MF22/GreenEntryBounds.lean:120:29: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
info: NLA/MF22/GreenEntryBounds.lean:138:0: 'NLA.MF22.uniform_green_entries' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3685/3688] Built NLA.MF22.Conditioning (4.9s)
info: NLA/MF22/Conditioning.lean:80:0: 'NLA.MF22.eventual_inverse_entries' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/MF22/Conditioning.lean:82:0: 'NLA.MF22.eventual_quadratic_conditioning' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/MF22/Conditioning.lean:84:0: 'NLA.MF22.polynomial_conditioning' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3686/3688] Built Solution (4.6s)
info: Solution.lean:21:0: 'NLA.MF22.complex_entry_norm_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:23:0: 'NLA.MF22.source_entry_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:25:0: 'NLA.MF22.leading_block_invertible' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:27:0: 'NLA.MF22.source_boundaries' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:29:0: 'NLA.MF22.source_recurrence' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:31:0: 'NLA.MF22.transfer_polynomial_certificates' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:33:0: 'NLA.MF22.numerator_denominator_coprime' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:35:0: 'NLA.MF22.quartic_factorization' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:37:0: 'NLA.MF22.cayley_identity' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:39:0: 'NLA.MF22.positive_discriminant_factor' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:41:0: 'NLA.MF22.real_cubic_discriminant' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:43:0: 'NLA.MF22.exceptional_parameter' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:45:0: 'NLA.MF22.four_roots' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:47:0: 'NLA.MF22.spectral_projector_algebra' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:49:0: 'NLA.MF22.dominant_projector' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:51:0: 'NLA.MF22.spectral_tail_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:53:0: 'NLA.MF22.green_source_state' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:55:0: 'NLA.MF22.green_inverse' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:57:0: 'NLA.MF22.uniform_green_entries' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:59:0: 'NLA.MF22.eventual_inverse_entries' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:61:0: 'NLA.MF22.eventual_quadratic_conditioning' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:63:0: 'NLA.MF22.polynomial_conditioning' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3687/3688] Built RegistryRecord (4.4s)
Build completed successfully (3688 jobs).