Merge pull request #517 from PerAlexandersson/refactor/common-interleaver-layers

refactor: split common-interleaver tactic layers

Author: PerAlexandersson

ARCHITECTURE.md

@@ -352,6 +352,26 @@ the historical facade before the split. The low-degree theorem endpoint has a
 136-module / 59,976-line closure and remains independent of tactic syntax and
 rules.
 
+The common-interleaver tactic now has the same stable frontend shape:
+
+- `Tactic.CommonInterleaver.Core` owns the pointwise sequence transports;
+- `BasicSyntax` and `BasicRules` own compatibility transports, finite-family
+  upgrades, and their sequence forms;
+- `AnalyticSyntax` and `AnalyticRules` own root-count certificates and
+  two-polynomial common-interleaver endpoints;
+- `FamilySyntax` and `FamilyRules` own the Chudnovsky--Seymour four-way and
+  pairwise-to-family certificate families, including their private routing
+  helpers; and
+- `LowDegreeSyntax` and `LowDegreeRules` own the degree-at-most-three endpoint
+  certificates, while `Tactic.CommonInterleaver` remains the compatibility
+  facade.
+
+The nine implementation units have 195, 338, 340, 298, 346, 546, 724, 196,
+and 227 local lines, replacing one 3,089-line mixed source. The OEIS tactic
+umbrella imports only `BasicRules`, exactly matching the sequence tactics it
+advertises and preserving its 425-module budget; the full tactic umbrella
+continues to re-export the complete compatibility facade.
+
 `Tactic.OEIS` is undergoing the same certificate-family migration. Its
 `OEIS.Basic` child owns the scalar-denominator certificate aliases, and
 `OEIS.DerivativeLag` owns the degree-two derivative-lag parser, dispatch, and

RealRooted.lean

@@ -646,6 +646,15 @@ import RealRooted.Tactic.Attr
 import RealRooted.Tactic.Bezoutian
 import RealRooted.Tactic.CoefficientShape
 import RealRooted.Tactic.CommonInterleaver
+import RealRooted.Tactic.CommonInterleaver.AnalyticRules
+import RealRooted.Tactic.CommonInterleaver.AnalyticSyntax
+import RealRooted.Tactic.CommonInterleaver.BasicRules
+import RealRooted.Tactic.CommonInterleaver.BasicSyntax
+import RealRooted.Tactic.CommonInterleaver.Core
+import RealRooted.Tactic.CommonInterleaver.FamilyRules
+import RealRooted.Tactic.CommonInterleaver.FamilySyntax
+import RealRooted.Tactic.CommonInterleaver.LowDegreeRules
+import RealRooted.Tactic.CommonInterleaver.LowDegreeSyntax
 import RealRooted.Tactic.CubicDiscriminant
 import RealRooted.Tactic.Derivative
 import RealRooted.Tactic.EndpointDerivative