RA-07: convexity of the elementary-symmetric error sequence
Recorded by the registry's curators from GitHub; the authors did not submit it here.
George Stepaniants
Proves the complete canonical discrete-convexity assertion for (j+1)e_(j+1)/e_j over every positive real spectrum. Actual subset sums, polynomial derivatives, full root multiplicities and an exact nonnegative pair certificate connect the proof to the original ratios.
Claims
Files and sources
- Paper
- OpenProblemsInNLA @ e375a6f, RA-07/lean/ ↗
- Lean bundle
- submissions/bundles/openproblemsinnla-ra-07-lean.tar.gz
- Toolchain
- leanprover/lean4:v4.33.1
- Posted on GitHub
- 12 September 2026
Verification PASSED
- Attempt
- 1
- Toolchain
- leanprover/lean4:v4.33.1
- Auditor
- v1 · modal
- lake build
- succeeded
- Kernel replay
- succeeded
- Duration
- 0:01:55.392886
Declarations audited
| Declaration | Kind | Axioms | Unused hypotheses | Canonical |
|---|---|---|---|---|
| NLA.RA07.errorSequence_convex | theorem · Prop | propext, Classical.choice, Quot.sound | none | matched |
| RegistryProblems.Problem_OP_00117 | definition | propext, Classical.choice, Quot.sound | none | no canonical statement |
NLA.RA07.errorSequence_convex
NLA.RA07.ConvexityConjecture
RegistryProblems.Problem_OP_00117
Prop
Build log
RegistryProblems: built against the registry's copy at 38ca23a44fc2b159a0c944d5c9af39a80eb601c2 rather than the pinned 545a5d18ad3917d52192c41ce172ec4b41945751. Statements are checked by content, not revision. ✔ [2890/2897] Built NLA.RA07.Definitions (6.8s) ✔ [2891/2897] Built NLA.RA07.Algebra (2.5s) ✔ [2892/2897] Built NLA.RA07.Sums (6.9s) ✔ [2893/2897] Built NLA.RA07.Roots (9.7s) ℹ [2894/2897] Built NLA.RA07.Proof (4.5s) info: NLA/RA07/Proof.lean:106:0: 'NLA.RA07.elementary_values_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA07/Proof.lean:107:0: 'NLA.RA07.generating_derivative_values_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA07/Proof.lean:108:0: 'NLA.RA07.positive_derivative_factorization_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA07/Proof.lean:109:0: 'NLA.RA07.power_sum_certificate_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA07/Proof.lean:110:0: 'NLA.RA07.second_difference_certificate_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA07/Proof.lean:111:0: 'NLA.RA07.errorSequence_convex_proved' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [2895/2897] Built Solution (4.3s) info: Solution.lean:77:0: 'NLA.RA07.elementary_values' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:78:0: 'NLA.RA07.generating_derivative_values' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:79:0: 'NLA.RA07.positive_derivative_factorization' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:80:0: 'NLA.RA07.power_sum_certificate' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:81:0: 'NLA.RA07.second_difference_certificate' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:82:0: 'NLA.RA07.errorSequence_convex' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [2896/2897] Built RegistryRecord (4.2s) Build completed successfully (2897 jobs).