refactor(Circuit/Boolean): split the P side out of Razborov/MiddleSlice to cut Smolensky/Majority's import closure (Part of #4451)

CslibFrontier.lean

@@ -1260,6 +1260,7 @@ public import CslibFrontier.Computability.Circuit.Boolean.PopulationCount.PolyTi
 public import CslibFrontier.Computability.Circuit.Boolean.PopulationCount.ThresholdPolyTime
 public import CslibFrontier.Computability.Circuit.Boolean.Propagation
 public import CslibFrontier.Computability.Circuit.Boolean.Razborov.MiddleSlice
+public import CslibFrontier.Computability.Circuit.Boolean.Razborov.MiddleSlice.P
 public import CslibFrontier.Computability.Circuit.Boolean.Razborov.Natural
 public import CslibFrontier.Computability.Circuit.Boolean.Razborov.RankProperty
 public import CslibFrontier.Computability.Circuit.Boolean.Razborov.Useful

CslibFrontier/Computability/Circuit/Boolean/ACC0.lean

@@ -12,8 +12,8 @@ public import CslibFrontier.Computability.Circuit.Boolean.ACC0.Basic
 public import CslibFrontier.Computability.Circuit.Boolean.ACC0.Simulation
 public import CslibFrontier.Computability.Complexity.Classes.P
 public import CslibFrontier.Computability.Complexity.Classes.PH.Kannan
-import CslibFrontier.Computability.Circuit.Boolean.Razborov.MiddleSlice
-import CslibFrontier.Computability.Circuit.Boolean.Smolensky.Majority
+import CslibFrontier.Computability.Circuit.Boolean.Razborov.MiddleSlice.P
+import CslibFrontier.Computability.Circuit.Boolean.Smolensky
 import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString
 
 /-!

CslibFrontier/Computability/Circuit/Boolean/ACC0/Basic.lean

@@ -11,7 +11,7 @@ public import CslibFrontier.Init
 public import CslibFrontier.Computability.Circuit.Boolean.ModGates
 public import CslibFrontier.Computability.Circuit.Boolean.ModMajority
 public import Mathlib.Data.Nat.Prime.Defs
-import CslibFrontier.Computability.Circuit.Boolean.Smolensky.Majority
+import CslibFrontier.Computability.Circuit.Boolean.Smolensky
 
 /-!
 # Definition, divisibility monotonicity, and Boolean closure of `ACC⁰`
@@ -31,7 +31,8 @@ and `q₂` therefore embed into the common modulus `q₁ * q₂`, making `ACC0`
 intersection, and union (`ACC0.compl`, `ACC0.inf`, `ACC0.sup`). By Håstad's and
 Razborov–Smolensky's lower bounds for parity, `AC0 ⊂ AC0Mod 2 ⊆ ACC0` (`AC0_ssubset_AC0Mod_two`,
 `AC0_ssubset_ACC0`) and `AC0Mod p ⊂ ACC0` for every odd prime `p` (`AC0Mod_ssubset_ACC0`). The case
-`p = 2` needs `MOD_3 ∉ AC⁰[2]`, which is not in the library.
+`p = 2` needs some language of `ACC0` outside AC⁰[2], such as `MOD_3`; no such lower bound is in
+the library.
 
 ## Main definitions
 
@@ -263,9 +264,9 @@ theorem AC0_ssubset_ACC0 : AC0 ⊂ ACC0 :=
     ⟨_, parity_mem_ACC0, parity_notMem_AC0⟩
 
 /-- **`AC⁰[p]` is strictly contained in `ACC⁰`** for every odd prime `p`, witnessed by parity
-[Smolensky1987]. For `p = 2` a witness would be `MOD_3`, which is not in `AC⁰[2]` by Smolensky's
-theorem for moduli `q` that are not powers of `p` [Smolensky1987]; that lower bound is not in the
-library. -/
+[Smolensky1987]. For `p = 2` any language of `ACC0` outside `AC⁰[2]` would do, for example `MOD_3`
+by Smolensky's theorem for moduli `q` that are not powers of `p` [Smolensky1987]; no such lower
+bound is in the library. -/
 theorem AC0Mod_ssubset_ACC0 {p : ℕ} [Fact p.Prime] (hp2 : p ≠ 2) : AC0Mod p ⊂ ACC0 :=
   (Set.ssubset_iff_of_subset (AC0Mod_subset_ACC0 p)).2
     ⟨_, parity_mem_ACC0, Smolensky.parity_notMem_AC0Mod hp2⟩

CslibFrontier/Computability/Circuit/Boolean/Razborov/MiddleSlice.lean

@@ -8,33 +8,28 @@ module
 -- upstream: candidate
 
 public import CslibFrontier.Computability.Circuit.Boolean.Razborov.RankProperty
-public import CslibFrontier.Computability.Complexity.Classes.P.Slices
 public import Mathlib.Data.Nat.Sqrt
-import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString
-import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
-import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
-import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Div
-import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Eq
-import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Sqrt
-import CslibFrontier.Foundations.Data.BitString.List
 import CslibFrontier.Foundations.Data.Nat.PolynomialBound.Exponential
 
 /-!
-# A middle slice in P but not in AC⁰[2]
+# A middle slice not in AC⁰[2]
 
 The **middle slice** (`middleSlice`) accepts the `n`-bit strings with exactly `a(n)` zeros, where
 `a(n) = ⌈n / 2⌉ - ⌊√(n + 1)⌋ / 10` (`sliceLevel`). It passes Razborov's rank test at level `a(n)`
 (`middleSlice_mem_rankTest`), so the size–depth tradeoff of the rank test
 (`two_mul_two_pow_le_size_of_mem_rankTest`) bounds every constant-depth circuit for it with `MOD_2`
 gates from below by `2 ^ Ω(n ^ (1 / (2 d)))`. Hence the middle slice is not in AC⁰[2]
 (`middleSlice_notMem_AC0Mod_two`) [Razborov1987]. It is in `P`, by counting the true bits and
-comparing with `a(n)` computed in unary from the length (`middleSlice_mem_P`), which separates
-`P` from AC⁰[2] (`exists_mem_P_notMem_AC0Mod_two`).
+comparing with `a(n)` computed in unary from the length, which separates `P` from AC⁰[2]
+(`Cslib.Circuits.Boolean.Razborov.middleSlice_mem_P` and
+`Cslib.Circuits.Boolean.Razborov.exists_mem_P_notMem_AC0Mod_two`). Those are in
+`CslibFrontier.Computability.Circuit.Boolean.Razborov.MiddleSlice.P`, kept apart so that this lower
+bound does not import the polynomial-time Turing machine library.
 
-For odd primes, parity separates `P` from AC⁰[p]; this module covers `p = 2`, where parity is a
-single gate. `Cslib.Circuits.Boolean.exists_mem_P_notMem_AC0Mod` combines the two for every prime,
-and `Cslib.Circuits.Boolean.Smolensky.majority_notMem_AC0Mod` uses the middle slice to show that
-majority is not in AC⁰[2].
+For odd primes, parity separates `P` from AC⁰[p]; the middle slice covers `p = 2`, where parity
+is a single gate. `Cslib.Circuits.Boolean.exists_mem_P_notMem_AC0Mod` combines the two for every
+prime, and `Cslib.Circuits.Boolean.Smolensky.majority_notMem_AC0Mod` uses the middle slice to show
+that majority is not in AC⁰[2].
 
 The lower bound follows the rank argument as recorded by
 [Razborov and Rudich, §3.2][RazborovRudich1997] and sketched for `p = 2` by
@@ -56,8 +51,6 @@ its choice of hard function.
 * `Cslib.Circuits.Boolean.Razborov.two_mul_two_pow_le_size_of_mem_rankTest_sliceLevel`: the
   size–depth tradeoff for any function passing the rank test at level `sliceLevel m`.
 * `Cslib.Circuits.Boolean.Razborov.middleSlice_notMem_AC0Mod_two`: the slice is not in AC⁰[2].
-* `Cslib.Circuits.Boolean.Razborov.middleSlice_mem_P`: the slice is in `P`.
-* `Cslib.Circuits.Boolean.Razborov.exists_mem_P_notMem_AC0Mod_two`: `P ⊄ AC⁰[2]`.
 
 ## References
 
@@ -72,7 +65,7 @@ public section
 
 namespace Cslib.Circuits.Boolean.Razborov
 
-open BitString Cslib.Complexity Turing.MultiTapeTM
+open BitString
 
 /-- The gap of the middle slice below the middle, `⌊√(n + 1)⌋ / 10`. -/
 def sliceGap (n : ℕ) : ℕ := Nat.sqrt (n + 1) / 10
@@ -145,43 +138,4 @@ theorem middleSlice_notMem_AC0Mod_two : Language.ofSlices middleSlice ∉ AC0Mod
   have hlt' : 5 * (n + 1) * size n < 2 ^ ℓ := hlt
   omega
 
-/-- The list evaluator of the middle slice: count the true bits and compare with
-`n - sliceLevel n`, where `n` is the length. -/
-private theorem middleSlice_ofList (x : List Bool) :
-    middleSlice x.length (ofList x.length x) =
-      decide (x.count true = x.length - ((x.length + 1) / 2 - Nat.sqrt (x.length + 1) / 10)) := by
-  rw [Bool.eq_iff_iff, decide_eq_true_iff, middleSlice_eq_true_iff, ← count_true_ofFn,
-    ofFn_ofList rfl, sliceLevel_eq]
-
-/-- **The middle slice is in `P`**: count the true bits in unary and compare with
-`n - sliceLevel n`, computed in unary from the length `n` (the square root in binary). -/
-theorem middleSlice_mem_P : (Language.ofSlices middleSlice : Set (List Bool)) ∈ P encBits := by
-  refine ofSlices_mem_P ?_
-  simp only [middleSlice_ofList]
-  have hlen : ComputableInPolyTime (fun x : List Bool => x.length) encBits encUnary :=
-    ComputableInPolyTime.length_bits
-  have hsucc : ComputableInPolyTime (fun x : List Bool => x.length + 1) encBits encUnary :=
-    ComputableInPolyTime.unary_add' hlen (.const 1)
-  have hsqrt : ComputableInPolyTime (fun x : List Bool => Nat.sqrt (x.length + 1)) encBits
-      encUnary :=
-    ComputableInPolyTime.binary_to_unary_bounded
-      (ComputableInPolyTime.binary_sqrt' (ComputableInPolyTime.unary_to_binary.comp hsucc)) hsucc
-      fun x => Nat.sqrt_le_self _
-  have hgap : ComputableInPolyTime (fun x : List Bool => Nat.sqrt (x.length + 1) / 10) encBits
-      encUnary :=
-    ComputableInPolyTime.unary_div' hsqrt (.const 10)
-  have hlevel : ComputableInPolyTime
-      (fun x : List Bool => (x.length + 1) / 2 - Nat.sqrt (x.length + 1) / 10) encBits encUnary :=
-    ComputableInPolyTime.unary_sub' (ComputableInPolyTime.unary_div' hsucc (.const 2)) hgap
-  have hcount : ComputableInPolyTime (fun x : List Bool => x.count true) encBits encUnary :=
-    ComputableInPolyTime.bitsCountWithInput ComputableInPolyTime.id' (.const true)
-  exact ComputableInPolyTime.unary_eq' hcount (ComputableInPolyTime.unary_sub' hlen hlevel)
-
-/-- **Unconditional separation `P ⊄ AC⁰[2]`**: the middle slice is in `P` and not in AC⁰[2]
-[Razborov1987]. `Cslib.Circuits.Boolean.exists_mem_P_notMem_AC0Mod` combines it with parity for odd
-primes, giving `P ⊄ AC⁰[p]` for every prime `p`. -/
-theorem exists_mem_P_notMem_AC0Mod_two :
-    ∃ L : Language Bool, (L : Set (List Bool)) ∈ P encBits ∧ L ∉ AC0Mod 2 :=
-  ⟨_, middleSlice_mem_P, middleSlice_notMem_AC0Mod_two⟩
-
 end Cslib.Circuits.Boolean.Razborov

CslibFrontier/Computability/Circuit/Boolean/Razborov/MiddleSlice/P.lean

@@ -0,0 +1,89 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import CslibFrontier.Computability.Circuit.Boolean.Razborov.MiddleSlice
+public import CslibFrontier.Computability.Complexity.Classes.P.Slices
+import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString
+import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
+import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
+import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Div
+import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Eq
+import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Sqrt
+import CslibFrontier.Foundations.Data.BitString.List
+
+/-!
+# The middle slice is in P: `P ⊄ AC⁰[2]`
+
+The middle slice `Cslib.Circuits.Boolean.Razborov.middleSlice`, which is not in AC⁰[2]
+(`Cslib.Circuits.Boolean.Razborov.middleSlice_notMem_AC0Mod_two`), is in `P`: a multi-tape Turing
+machine counts the true bits and compares with `n - sliceLevel n`, computed in unary from the
+length `n` (`middleSlice_mem_P`). This separates `P` from AC⁰[2]
+(`exists_mem_P_notMem_AC0Mod_two`) [Razborov1987].
+
+The `P` side is kept apart from the lower bound so that clients of the lower bound alone, such as
+`Cslib.Circuits.Boolean.Smolensky.majority_notMem_AC0Mod`, do not import the polynomial-time Turing
+machine library.
+
+## Main results
+
+* `Cslib.Circuits.Boolean.Razborov.middleSlice_mem_P`: the middle slice is in `P`.
+* `Cslib.Circuits.Boolean.Razborov.exists_mem_P_notMem_AC0Mod_two`: `P ⊄ AC⁰[2]`.
+
+## References
+
+* [A. A. Razborov, *Lower bounds on the size of bounded depth circuits over a complete basis with
+  logical addition*][Razborov1987]
+-/
+
+public section
+
+namespace Cslib.Circuits.Boolean.Razborov
+
+open BitString Cslib.Complexity Turing.MultiTapeTM
+
+/-- The list evaluator of the middle slice: count the true bits and compare with
+`n - sliceLevel n`, where `n` is the length. -/
+private theorem middleSlice_ofList (x : List Bool) :
+    middleSlice x.length (ofList x.length x) =
+      decide (x.count true = x.length - ((x.length + 1) / 2 - Nat.sqrt (x.length + 1) / 10)) := by
+  rw [Bool.eq_iff_iff, decide_eq_true_iff, middleSlice_eq_true_iff, ← count_true_ofFn,
+    ofFn_ofList rfl, sliceLevel_eq]
+
+/-- **The middle slice is in `P`**: count the true bits in unary and compare with
+`n - sliceLevel n`, computed in unary from the length `n` (the square root in binary). -/
+theorem middleSlice_mem_P : (Language.ofSlices middleSlice : Set (List Bool)) ∈ P encBits := by
+  refine ofSlices_mem_P ?_
+  simp only [middleSlice_ofList]
+  have hlen : ComputableInPolyTime (fun x : List Bool => x.length) encBits encUnary :=
+    ComputableInPolyTime.length_bits
+  have hsucc : ComputableInPolyTime (fun x : List Bool => x.length + 1) encBits encUnary :=
+    ComputableInPolyTime.unary_add' hlen (.const 1)
+  have hsqrt : ComputableInPolyTime (fun x : List Bool => Nat.sqrt (x.length + 1)) encBits
+      encUnary :=
+    ComputableInPolyTime.binary_to_unary_bounded
+      (ComputableInPolyTime.binary_sqrt' (ComputableInPolyTime.unary_to_binary.comp hsucc)) hsucc
+      fun x => Nat.sqrt_le_self _
+  have hgap : ComputableInPolyTime (fun x : List Bool => Nat.sqrt (x.length + 1) / 10) encBits
+      encUnary :=
+    ComputableInPolyTime.unary_div' hsqrt (.const 10)
+  have hlevel : ComputableInPolyTime
+      (fun x : List Bool => (x.length + 1) / 2 - Nat.sqrt (x.length + 1) / 10) encBits encUnary :=
+    ComputableInPolyTime.unary_sub' (ComputableInPolyTime.unary_div' hsucc (.const 2)) hgap
+  have hcount : ComputableInPolyTime (fun x : List Bool => x.count true) encBits encUnary :=
+    ComputableInPolyTime.bitsCountWithInput ComputableInPolyTime.id' (.const true)
+  exact ComputableInPolyTime.unary_eq' hcount (ComputableInPolyTime.unary_sub' hlen hlevel)
+
+/-- **Unconditional separation `P ⊄ AC⁰[2]`**: the middle slice is in `P` and not in AC⁰[2]
+[Razborov1987]. `Cslib.Circuits.Boolean.exists_mem_P_notMem_AC0Mod` combines it with parity for odd
+primes, giving `P ⊄ AC⁰[p]` for every prime `p`. -/
+theorem exists_mem_P_notMem_AC0Mod_two :
+    ∃ L : Language Bool, (L : Set (List Bool)) ∈ P encBits ∧ L ∉ AC0Mod 2 :=
+  ⟨_, middleSlice_mem_P, middleSlice_notMem_AC0Mod_two⟩
+
+end Cslib.Circuits.Boolean.Razborov

CslibFrontierResults/Entries.lean

@@ -21,7 +21,7 @@ import CslibFrontier.Computability.Circuit.Boolean.Formula.Andreev
 import CslibFrontier.Computability.Circuit.Boolean.Hastad.Sharp
 import CslibFrontier.Computability.Circuit.Boolean.Khrapchenko
 import CslibFrontier.Computability.Circuit.Boolean.NaturalProof.Generator
-import CslibFrontier.Computability.Circuit.Boolean.Razborov.MiddleSlice
+import CslibFrontier.Computability.Circuit.Boolean.Razborov.MiddleSlice.P
 import CslibFrontier.Computability.Circuit.Boolean.Razborov.Useful
 import CslibFrontier.Computability.Circuit.Boolean.Smolensky
 import CslibFrontier.Computability.Communication.Discrepancy
@@ -487,15 +487,16 @@ register_result "middle-slice-mod-two" where
       locator := "p. 10:20" }
   ]
   theorems := [
-    Cslib.Circuits.Boolean.Razborov.middleSlice_notMem_AC0Mod_two,
+    Cslib.Circuits.Boolean.Razborov.middleSlice_mem_P,
     Cslib.Circuits.Boolean.Razborov.exists_mem_P_notMem_AC0Mod_two
   ]
   scope := "The language of bit strings of length n with exactly ⌈n/2⌉ - ⌊√(n + 1)⌋/10 zeros is \
     decided in polynomial time by a multi-tape Turing machine and is not in AC⁰[2]: no family of \
     circuits of NOT, unbounded fan-in AND/OR and MOD_2 gates of constant depth and polynomial \
     size decides it (nonuniform). Proved through a variant of Razborov's GF(2) rank property \
     (one square matrix, threshold C(n, a)/2); the sources give the abstract property and a \
-    sketch, and Razborov's original paper was not checked for its hard function."
+    sketch, and Razborov's original paper was not checked for its hard function. The lower bound \
+    itself is middleSlice_notMem_AC0Mod_two in the imported module Razborov.MiddleSlice."
 
 register_result "rank-property-natural-ac0-2" where
   title := "Razborov's rank property is a P/poly-natural property useful against AC⁰[2]"