refactor: golf cubic root-count endpoint

Author: PerAlexandersson

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

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