Skip to content

Golf the cubic root-count endpoint #516

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
PerAlexandersson merged 1 commit into from
Sep 4, 2026
Merged

Golf the cubic root-count endpoint #516

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions ARCHITECTURE.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -344,12 +344,12 @@ The root-count tactic follows the same theorem/frontend boundary:
- `CoreRules` and `LowDegreeRules` own the two macro-expansion tables; and
- `Tactic.RootCount` remains the compatibility facade.

The six implementation units have 630, 405, 653, 401, 750, and 460 local
The six implementation units have 630, 404, 653, 401, 750, and 460 local
lines, respectively, replacing one 3,226-line mixed source while preserving
all 191 theorem and syntax declarations. The reusable sequence core has an
83-module / 30,789-line closure, compared with 138 modules / 62,863 lines for
the historical facade before the split. The low-degree theorem endpoint has a
136-module / 59,977-line closure and remains independent of tactic syntax and
136-module / 59,976-line closure and remains independent of tactic syntax and
rules.

`Tactic.OEIS` is undergoing the same certificate-family migration. Its
Expand Down
5 changes: 2 additions & 3 deletions RealRooted/Tactic/RootCount/LowDegree.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -173,9 +173,8 @@ theorem posCombo_sameDegree_rootCount_degree_le_three
rcases Nat.le_or_eq_of_le_succ hfdeg with hle | hfdeg3
· exact rootCount_diff_le_one_of_posCombo_sameDegree_natDegree_le_two
hf_pos hg_pos hfnn hgnn hfg hdeg hno hle x
· have hgdeg3 : g.natDegree = 3 := by rw [hdeg, hfdeg3]
exact sameDegree_cubic_rootCount_le_one_of_secondRootBound
cubicSecondRootBound_from_analytic hfdeg3 hgdeg3
· exact sameDegree_cubic_rootCount_le_one_of_secondRootBound
cubicSecondRootBound_from_analytic hfdeg3 (hdeg.trans hfdeg3)
(hfg.isRealRooted_left_of_sameDegree hf_pos hg_pos hdeg).2
(hfg.isRealRooted_right_of_sameDegree hf_pos hg_pos hdeg).2
hf_pos hg_pos hfg x
Expand Down
Loading