From 95066dd308c05fad718a834c384714655cd06e8a Mon Sep 17 00:00:00 2001 From: Per Alexandersson Date: Fri, 4 Sep 2026 18:55:01 +0000 Subject: [PATCH] refactor: golf cubic root-count endpoint --- ARCHITECTURE.md | 4 ++-- RealRooted/Tactic/RootCount/LowDegree.lean | 5 ++--- 2 files changed, 4 insertions(+), 5 deletions(-) diff --git a/ARCHITECTURE.md b/ARCHITECTURE.md index 83e73019..5cdc0a60 100644 --- a/ARCHITECTURE.md +++ b/ARCHITECTURE.md @@ -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 diff --git a/RealRooted/Tactic/RootCount/LowDegree.lean b/RealRooted/Tactic/RootCount/LowDegree.lean index 7d99a91d..261e1860 100644 --- a/RealRooted/Tactic/RootCount/LowDegree.lean +++ b/RealRooted/Tactic/RootCount/LowDegree.lean @@ -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