MF-21: the uniform Toeplitz eigenvalue expansion threshold for every m >= 3
Recorded by the registry's curators from GitHub; the authors did not submit it here.
OpenAI Codex AI agents
Complete symbolic Lean proof of the original three-part target, continuous-family obstruction, smooth common coefficients, sharp finite-head and global errors, and exact Fourier-matrix correspondence. All five contracts passed actual non-root Linux Comparator and default-kernel acceptance at the recorded immutable proof revision.
Claims
Files and sources
- Paper
- OpenProblemsInNLA @ e375a6f, MF-21/lean/ ↗
- Lean bundle
- submissions/bundles/openproblemsinnla-mf-21-lean.tar.gz
- Toolchain
- leanprover/lean4:v4.33.1
- Posted on GitHub
- 20 September 2026
Verification PASSED
- Attempt
- 2
- Toolchain
- leanprover/lean4:v4.33.1
- Auditor
- v1 · modal
- lake build
- succeeded
- Kernel replay
- succeeded
- Duration
- 0:12:54.478325
Declarations audited
| Declaration | Kind | Axioms | Unused hypotheses | Canonical |
|---|---|---|---|---|
| NLA.MF21.full_target | theorem · Prop | propext, Classical.choice, Quot.sound | none | matched |
| RegistryProblems.Problem_OP_00096 | definition | propext, Classical.choice, Quot.sound | none | no canonical statement |
NLA.MF21.full_target
MF21Challenge.FullTarget
RegistryProblems.Problem_OP_00096
Prop
Build log
oundary.actual_phase_error_bounds' depends on axioms: [propext, Classical.choice, Quot.sound] info: MF21/ActualPhaseIndexing.lean:156:0: 'MF21ActualBoundary.simple_sine_zero_unique_index' depends on axioms: [propext, Classical.choice, Quot.sound] info: MF21/ActualPhaseIndexing.lean:157:0: 'MF21ActualBoundary.actual_indexed_phase_roots' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [8768/8778] Built MF21.MF21Transcendence.ETranscendental (13s) ✔ [8769/8778] Built MF21.MF21Transcendence.HermiteLindemann (8.1s) ℹ [8770/8778] Built MF21.ActualTailAngles (12s) info: MF21/ActualTailAngles.lean:55:0: 'MF21Expansion.actual_tailAngleApproximation' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [8771/8782] Built MF21.MF21Transcendence.PiLindemann (13s) ✔ [8772/8782] Built MF21.MF21Transcendence.SubsetSumEsymm (27s) ℹ [8773/8787] Built MF21.InverseTraceRecurrence (14s) info: MF21/InverseTraceRecurrence.lean:85:0: 'MF21InverseTrace.inverse_tail' depends on axioms: [propext, Classical.choice, Quot.sound] info: MF21/InverseTraceRecurrence.lean:87:0: 'MF21InverseTrace.inverse_trace_step' depends on axioms: [propext, Classical.choice, Quot.sound] info: MF21/InverseTraceRecurrence.lean:88:0: 'MF21InverseTrace.toeplitz_inverse_trace_step' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [8774/8787] Built MF21.MF21Transcendence.MonicRootSums (27s) ℹ [8775/8787] Built MF21.TraceLimitSummation (12s) info: MF21/TraceLimitSummation.lean:92:0: 'MF21DiscreteLimits.sum_normalized_tendsto' depends on axioms: [propext, Classical.choice, Quot.sound] info: MF21/TraceLimitSummation.lean:94:0: 'MF21DiscreteLimits.sequence_of_increment_tendsto' depends on axioms: [propext, Classical.choice, Quot.sound] info: MF21/TraceLimitSummation.lean:96:0: 'MF21DiscreteLimits.normalized_shift_tendsto' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [8778/8790] Built MF21.CoefficientUniqueness (9.0s) info: MF21/CoefficientUniqueness.lean:161:0: 'MF21Audit.coefficient_unique_of_weighted_bigO' depends on axioms: [propext, Classical.choice, Quot.sound] info: MF21/CoefficientUniqueness.lean:162:0: 'MF21Audit.continuous_coefficient_unique' depends on axioms: [propext, Classical.choice, Quot.sound] info: MF21/CoefficientUniqueness.lean:164:0: 'MF21Audit.expansion_unique_on_mesh' depends on axioms: [propext, Classical.choice, Quot.sound] info: MF21/CoefficientUniqueness.lean:166:0: 'MF21Audit.top_expansion_unique_on_mesh' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [8779/8790] Built MF21.MF21CoefficientUniqueness (10s) info: MF21/MF21CoefficientUniqueness.lean:163:0: 'MF21Uniqueness.bulkExpansion_unique' depends on axioms: [propext, Classical.choice, Quot.sound] info: MF21/MF21CoefficientUniqueness.lean:164:0: 'MF21Uniqueness.mf21_bulk_coefficients_unique' depends on axioms: [propext, Classical.choice, Quot.sound] info: MF21/MF21CoefficientUniqueness.lean:165:0: 'MF21Uniqueness.mf21_uniform_coefficients_eq_bulk' depends on axioms: [propext, Classical.choice, Quot.sound] info: MF21/MF21CoefficientUniqueness.lean:167:0: 'MF21Uniqueness.universalObstruction_of_fullTarget' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [8781/8790] Built MF21.MF21Transcendence.PiTranscendental (19s) ℹ [8782/8790] Built MF21.MF21Transcendence (9.7s) info: MF21/MF21Transcendence.lean:42:0: 'MF21Audit.pi_transcendental' depends on axioms: [propext, Classical.choice, Quot.sound] info: MF21/MF21Transcendence.lean:43:0: 'MF21Audit.pi_pow_irrational' depends on axioms: [propext, Classical.choice, Quot.sound] info: MF21/MF21Transcendence.lean:44:0: 'MF21Audit.pi_trace_value_irrational' depends on axioms: [propext, Classical.choice, Quot.sound] info: MF21/MF21Transcendence.lean:45:0: 'MF21Audit.trace_values_ne_unconditional' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [8783/8790] Built MF21.MF21TraceSeries (12s) info: MF21/MF21TraceSeries.lean:217:0: 'MF21Audit.even_zeta_sum' depends on axioms: [propext, Classical.choice, Quot.sound] info: MF21/MF21TraceSeries.lean:218:0: 'MF21Audit.half_tail_sum' depends on axioms: [propext, Classical.choice, Quot.sound] info: MF21/MF21TraceSeries.lean:219:0: 'MF21Audit.modelTrace_irrational' depends on axioms: [propext, Classical.choice, Quot.sound] info: MF21/MF21TraceSeries.lean:220:0: 'MF21Audit.kernelTraceConstant_ne_modelTrace' depends on axioms: [propext, Classical.choice, Quot.sound] info: MF21/MF21TraceSeries.lean:221:0: 'MF21Audit.modelTrace_series_summable' depends on axioms: [propext, Classical.choice, Quot.sound] ⚠ [8784/8790] Built MF21.TraceIntegralConstant (11s) warning: MF21/TraceIntegralConstant.lean:72:2: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false` info: MF21/TraceIntegralConstant.lean:75:0: 'MF21DiscreteLimits.integral_pow_one_sub_pow' depends on axioms: [propext, Classical.choice, Quot.sound] info: MF21/TraceIntegralConstant.lean:77:0: 'MF21DiscreteLimits.first_column_integral_constant' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [8785/8790] Built MF21.ToeplitzTraceLimit (9.7s) info: MF21/ToeplitzTraceLimit.lean:85:0: 'MF21TraceLimit.inverseTrace_increment_tendsto' depends on axioms: [propext, Classical.choice, Quot.sound] info: MF21/ToeplitzTraceLimit.lean:86:0: 'MF21TraceLimit.inverseTrace_tendsto' depends on axioms: [propext, Classical.choice, Quot.sound] info: MF21/ToeplitzTraceLimit.lean:87:0: 'MF21TraceLimit.eigenvalue_inverse_sum_tendsto' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [8786/8790] Built MF21.ActualTraceObstruction (11s) info: MF21/ActualTraceObstruction.lean:181:0: 'MF21Obstruction.actual_finite_head_separation' depends on axioms: [propext, Classical.choice, Quot.sound] info: MF21/ActualTraceObstruction.lean:183:0: 'MF21Obstruction.model_finite_head_lower_bound' depends on axioms: [propext, Classical.choice, Quot.sound] info: MF21/ActualTraceObstruction.lean:185:0: 'MF21Obstruction.model_not_uniform' depends on axioms: [propext, Classical.choice, Quot.sound] info: MF21/ActualTraceObstruction.lean:186:0: 'MF21Obstruction.model_finite_head_remainder' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [8787/8790] Built MF21.FinalTarget (10s) info: MF21/FinalTarget.lean:112:0: 'MF21Verified.targetAt' depends on axioms: [propext, Classical.choice, Quot.sound] info: MF21/FinalTarget.lean:113:0: 'MF21Verified.fullTarget' depends on axioms: [propext, Classical.choice, Quot.sound] info: MF21/FinalTarget.lean:114:0: 'MF21Verified.universalObstruction' depends on axioms: [propext, Classical.choice, Quot.sound] info: MF21/FinalTarget.lean:115:0: 'MF21Verified.smooth_coefficients' depends on axioms: [propext, Classical.choice, Quot.sound] info: MF21/FinalTarget.lean:116:0: 'MF21Verified.finite_head_sharpness' depends on axioms: [propext, Classical.choice, Quot.sound] info: MF21/FinalTarget.lean:118:0: 'MF21Verified.smooth_common_family' depends on axioms: [propext, Classical.choice, Quot.sound] info: MF21/FinalTarget.lean:119:0: 'MF21Verified.fourier_matrix_entries' depends on axioms: [propext, Classical.choice, Quot.sound] info: MF21/FinalTarget.lean:120:0: 'MF21Verified.model_sharp_upper' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [8788/8790] Built Solution (10s) info: Solution.lean:56:0: 'NLA.MF21.full_target' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:57:0: 'NLA.MF21.universal_obstruction' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:58:0: 'NLA.MF21.smooth_common_family' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:59:0: 'NLA.MF21.fourier_matrix_entries' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:60:0: 'NLA.MF21.coefficients_unique' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [8789/8790] Built RegistryRecord (10s) Build completed successfully (8790 jobs).