feat(Analysis/Polynomial): certified Sturm chains from a PRS certificate - #42559
feat(Analysis/Polynomial): certified Sturm chains from a PRS certificate#42559AMcRoberts wants to merge 5 commits into
Conversation
We introduce Sturm sequences for real polynomials and prove Sturm's theorem: the number of sign variations of the sequence decreases by exactly the number of distinct roots crossed on a half-open interval. The development follows the structure of Manuel Eberl's AFP entry *A Formalisation of Sturm's Theorem* (2014); see the module's own References section.
github-actions
Bot
added
the
new-contributor
Welcome new contributor!Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests. We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR. Thank you again for joining our community. |
PR summary a229300f32Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
| Current number | Change | Type (weak) |
|---|---|---|
| 5051 | 2 | exposed public sections |
Current commit a229300f32
Reference commit 87adeaebd3
This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
…rd_msgs) Three real CI failures found and fixed: - PR title had a capitalized subject; mathlib's title linter requires a lowercase first word. - references.bib's new eberl2014sturm entry was in the wrong alphabetical position (bibtool's canonical sort wants it before Echenique2005, not after EinsiedlerWard2017) and left a stray blank line; applied the exact diff CI's own bibtool check computed. - MathlibTest/Sturm.lean used bare #check without #guard_msgs, so its info-level output was flagged as an unexpected build failure; wrapped each #check with #guard_msgs and the exact expected output.
CertifiedSturmChain packages the algebraic data a Euclidean or pseudo-remainder-sequence construction naturally produces (a positive-scaled recurrence at each step, a nonzero-constant Bezout identity between p and its derivative, and a nonzero-constant terminal element) and proves it satisfies IsSturmSequence, so a concrete PRS chain can drive Sturm's root-count theorem directly. This development was produced independently from the classical sources cited in the module's own References section, without consulting the formalisation cited by the abstract theorem this depends on (leanprover-community#42558).
…, guard_msgs) Two real CI failures found and fixed, same root causes as the sturm-abstract branch's own fix commit: - references.bib's eisermann2012sturm entry left a stray double blank line before Eisenbud1995; bibtool's canonical form wants one. - MathlibTest/SturmCertificate.lean used bare #check without #guard_msgs, so its info-level output was flagged as an unexpected build failure; wrapped each #check with #guard_msgs and the exact expected output.
9224c89 to
e0cf58a
Compare
…pacing eisermann2012sturm had drifted back before Eisenbud1995 instead of after it, pebayRojasThompson2022's author field lost its bibtool line-wrap, and a stray blank line before perfect1969matroid crept back in from upstream drift. Re-ran bibtool's canonical pass to restore all three.
1 participant
Stacked on #42558 — this branch is
sturm-abstractplus one more commit,so the diff will include both PRs' changes until #42558 merges. Only the
second commit (
SturmCertificate.lean+ its test file) belongs to this PR;please review that commit specifically until #42558 lands, at which point
this diff will shrink to just this PR's content.
CertifiedSturmChainpackages the algebraic data a Euclidean orpseudo-remainder-sequence construction naturally produces (a positive-scaled
recurrence at each step, a nonzero-constant Bézout identity between
pandits derivative, and a nonzero-constant terminal element) and proves it
satisfies
IsSturmSequence(#42558), so a concrete PRS chain can driveSturm's root-count theorem directly without re-deriving the sign semantics
per instance.
This development was produced independently from the classical sources
cited in the module's own
## Referencessection, without consulting theformalisation cited by #42558.