diff --git a/CslibFrontier.lean b/CslibFrontier.lean index 12df481cf0..58b60e3ac3 100644 --- a/CslibFrontier.lean +++ b/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 diff --git a/CslibFrontier/Computability/Circuit/Boolean/ACC0.lean b/CslibFrontier/Computability/Circuit/Boolean/ACC0.lean index 4691f3bf51..d44f365ebc 100644 --- a/CslibFrontier/Computability/Circuit/Boolean/ACC0.lean +++ b/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 /-! diff --git a/CslibFrontier/Computability/Circuit/Boolean/ACC0/Basic.lean b/CslibFrontier/Computability/Circuit/Boolean/ACC0/Basic.lean index 5e3604e7eb..509f9c5fa2 100644 --- a/CslibFrontier/Computability/Circuit/Boolean/ACC0/Basic.lean +++ b/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⟩ diff --git a/CslibFrontier/Computability/Circuit/Boolean/Razborov/MiddleSlice.lean b/CslibFrontier/Computability/Circuit/Boolean/Razborov/MiddleSlice.lean index d33d032c54..033be0da93 100644 --- a/CslibFrontier/Computability/Circuit/Boolean/Razborov/MiddleSlice.lean +++ b/CslibFrontier/Computability/Circuit/Boolean/Razborov/MiddleSlice.lean @@ -8,19 +8,11 @@ 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)` @@ -28,13 +20,16 @@ The **middle slice** (`middleSlice`) accepts the `n`-bit strings with exactly `a (`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 diff --git a/CslibFrontier/Computability/Circuit/Boolean/Razborov/MiddleSlice/P.lean b/CslibFrontier/Computability/Circuit/Boolean/Razborov/MiddleSlice/P.lean new file mode 100644 index 0000000000..5687c00e9a --- /dev/null +++ b/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 diff --git a/CslibFrontierResults/Entries.lean b/CslibFrontierResults/Entries.lean index 444746268d..b60e449bd7 100644 --- a/CslibFrontierResults/Entries.lean +++ b/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,7 +487,7 @@ 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 \ @@ -495,7 +495,8 @@ register_result "middle-slice-mod-two" where 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]" diff --git a/manual/circuits-logic-and-other-models/circuits-and-formulas.md b/manual/circuits-logic-and-other-models/circuits-and-formulas.md index 80e69208c6..fc480c6679 100644 --- a/manual/circuits-logic-and-other-models/circuits-and-formulas.md +++ b/manual/circuits-logic-and-other-models/circuits-and-formulas.md @@ -92,7 +92,7 @@ Chen, Hirahara, Oliveira, Pich, Rajgopal and Santhanam measure the oracle gates [PolylogDepth](https://github.com/cslib-community/cslib-frontier/blob/13e6a31951bf1c89a1a6258c44f9444aecbbefd8/Complexity/Computability/Circuit/Boolean/DepthClasses.lean#L51) defines polynomial-size families with depth bounded by `c(floor(log2 n)+1)^i`. The De Morgan, unbounded, majority and modular bases give NC, AC, TC and ACMod hierarchies. Exponent zero gives constant-depth classes. The families are nonuniform: one circuit may be chosen independently at every length. `ACC0` is the union over fixed moduli at least two, and the library proves its Boolean closure and inclusion in TC0. See [ACC0](https://github.com/cslib-community/cslib-frontier/blob/13e6a31951bf1c89a1a6258c44f9444aecbbefd8/Complexity/Computability/Circuit/Boolean/ACC0/Basic.lean) and [TC0](https://github.com/cslib-community/cslib-frontier/blob/13e6a31951bf1c89a1a6258c44f9444aecbbefd8/Complexity/Computability/Circuit/Boolean/TC0.lean). -For the modulus two, where parity is a single gate, [Razborov/MiddleSlice.lean](../../CslibFrontier/Computability/Circuit/Boolean/Razborov/MiddleSlice.lean) separates `P` from `AC0Mod 2` with a middle slice: `middleSlice n` accepts the `n`-bit strings with exactly `⌈n/2⌉ - ⌊√(n+1)⌋/10` zeros (`sliceLevel_eq`). `middleSlice_notMem_AC0Mod_two` places it outside `AC0Mod 2`, `middleSlice_mem_P` decides it by counting in unary, and `exists_mem_P_notMem_AC0Mod_two` packages the separation. [ACC0.lean](../../CslibFrontier/Computability/Circuit/Boolean/ACC0.lean) combines it with parity for odd primes, so `exists_mem_P_notMem_AC0Mod` gives `P ⊄ AC0Mod p` for every prime `p`. Through `exactlyCircuitOfMajority`, the slice also keeps majority out of `AC0Mod 2`, so `Smolensky.majority_notMem_AC0Mod`, `Smolensky.TC0_not_subset_AC0Mod` and `Smolensky.AC0Mod_ssubset_TC0` hold for every prime ([Smolensky/Majority.lean](../../CslibFrontier/Computability/Circuit/Boolean/Smolensky/Majority.lean)). `AC0Mod_ssubset_ACC0` still needs an odd prime: at `p = 2` it would need `MOD_3 ∉ AC0Mod 2`, which is not in the library. The lower bound goes through Razborov's GF(2) rank method in [Razborov/RankProperty.lean](../../CslibFrontier/Computability/Circuit/Boolean/Razborov/RankProperty.lean). The zero-sum matrix of a function at level `a` is indexed by the `a`-subsets of the inputs, with entry at `(I, J)` the sum of the function over the points vanishing on `I ∪ J`. Functions of degree `D` over `ZMod 2` with `D + 2a < n` have zero matrix, and a function supported on `E` has rank at most `#E`. Smolensky's approximation (`Smolensky.exists_lowDegree_approx`) then bounds the rank of a depth-`d` circuit's matrix by `size · 2^n / 2^ℓ` when `ℓ^d + 2a < n` (`rank_mul_two_pow_le_size`). The rank test (`rankTest n a`, rank at least `C(n, a)/2`) accepts at least half of all functions (`two_pow_two_pow_le_two_mul_ncard_rankTest`) and the indicator `exactWeight (n - a)` of the points with exactly `a` zeros, whose matrix is the identity (`exactWeight_mem_rankTest`). Near the middle level, `two_mul_two_pow_le_size_of_mem_rankTest` gives size at least `2 · 2^ℓ / (5(n+1))` whenever `ℓ^d + 2 ≤ 2s`, where `a = ⌈n/2⌉ - s` and `100s² ≤ n+1`. The test is a variant (one square matrix, threshold `C(n, a)/2`) of the property sketched by Carmosino, Impagliazzo, Kabanets and Kolokolova. [Razborov/Natural.lean](../../CslibFrontier/Computability/Circuit/Boolean/Razborov/Natural.lean) decides it from truth tables with De Morgan circuits of `173 · 8^n` gates (`synthesis_truthTableTest_rankTest`), through the Gauss–Jordan rank circuits of [GF2Rank.lean](../../CslibFrontier/Computability/Circuit/Boolean/GF2Rank.lean), so along any level function `a` the rank property `rankProperty a` is `P/poly`-natural (`isNatural_PPoly_rankProperty`). Along `sliceLevel` it is also useful against `AC0Mod 2` (`isUseful_AC0Mod_two_rankProperty` in [Razborov/Useful.lean](../../CslibFrontier/Computability/Circuit/Boolean/Razborov/Useful.lean)), at an explicit input length polylogarithmic in the circuit size (truth tables quasi-polynomial in it); [the metacomplexity chapter](metacomplexity-and-methods.md#natural-proofs-and-cryptographic-assumptions) states it. Depth and size count every gate, including NOT and constants. +For the modulus two, where parity is a single gate, [Razborov/MiddleSlice.lean](../../CslibFrontier/Computability/Circuit/Boolean/Razborov/MiddleSlice.lean) separates `P` from `AC0Mod 2` with a middle slice: `middleSlice n` accepts the `n`-bit strings with exactly `⌈n/2⌉ - ⌊√(n+1)⌋/10` zeros (`sliceLevel_eq`). `middleSlice_notMem_AC0Mod_two` places it outside `AC0Mod 2`; [Razborov/MiddleSlice/P.lean](../../CslibFrontier/Computability/Circuit/Boolean/Razborov/MiddleSlice/P.lean), kept apart so that the lower bound does not import the Turing machine library, decides it by counting in unary (`middleSlice_mem_P`) and packages the separation (`exists_mem_P_notMem_AC0Mod_two`). [ACC0.lean](../../CslibFrontier/Computability/Circuit/Boolean/ACC0.lean) combines it with parity for odd primes, so `exists_mem_P_notMem_AC0Mod` gives `P ⊄ AC0Mod p` for every prime `p`. Through `exactlyCircuitOfMajority`, the slice also keeps majority out of `AC0Mod 2`, so `Smolensky.majority_notMem_AC0Mod`, `Smolensky.TC0_not_subset_AC0Mod` and `Smolensky.AC0Mod_ssubset_TC0` hold for every prime ([Smolensky/Majority.lean](../../CslibFrontier/Computability/Circuit/Boolean/Smolensky/Majority.lean)). `AC0Mod_ssubset_ACC0` still needs an odd prime: at `p = 2` it would need some language of `ACC0` outside `AC0Mod 2`, such as `MOD_3`, and no such lower bound is in the library. The lower bound goes through Razborov's GF(2) rank method in [Razborov/RankProperty.lean](../../CslibFrontier/Computability/Circuit/Boolean/Razborov/RankProperty.lean). The zero-sum matrix of a function at level `a` is indexed by the `a`-subsets of the inputs, with entry at `(I, J)` the sum of the function over the points vanishing on `I ∪ J`. Functions of degree `D` over `ZMod 2` with `D + 2a < n` have zero matrix, and a function supported on `E` has rank at most `#E`. Smolensky's approximation (`Smolensky.exists_lowDegree_approx`) then bounds the rank of a depth-`d` circuit's matrix by `size · 2^n / 2^ℓ` when `ℓ^d + 2a < n` (`rank_mul_two_pow_le_size`). The rank test (`rankTest n a`, rank at least `C(n, a)/2`) accepts at least half of all functions (`two_pow_two_pow_le_two_mul_ncard_rankTest`) and the indicator `exactWeight (n - a)` of the points with exactly `a` zeros, whose matrix is the identity (`exactWeight_mem_rankTest`). Near the middle level, `two_mul_two_pow_le_size_of_mem_rankTest` gives size at least `2 · 2^ℓ / (5(n+1))` whenever `ℓ^d + 2 ≤ 2s`, where `a = ⌈n/2⌉ - s` and `100s² ≤ n+1`. The test is a variant (one square matrix, threshold `C(n, a)/2`) of the property sketched by Carmosino, Impagliazzo, Kabanets and Kolokolova. [Razborov/Natural.lean](../../CslibFrontier/Computability/Circuit/Boolean/Razborov/Natural.lean) decides it from truth tables with De Morgan circuits of `173 · 8^n` gates (`synthesis_truthTableTest_rankTest`), through the Gauss–Jordan rank circuits of [GF2Rank.lean](../../CslibFrontier/Computability/Circuit/Boolean/GF2Rank.lean), so along any level function `a` the rank property `rankProperty a` is `P/poly`-natural (`isNatural_PPoly_rankProperty`). Along `sliceLevel` it is also useful against `AC0Mod 2` (`isUseful_AC0Mod_two_rankProperty` in [Razborov/Useful.lean](../../CslibFrontier/Computability/Circuit/Boolean/Razborov/Useful.lean)), at an explicit input length polylogarithmic in the circuit size (truth tables quasi-polynomial in it); [the metacomplexity chapter](metacomplexity-and-methods.md#natural-proofs-and-cryptographic-assumptions) states it. Depth and size count every gate, including NOT and constants. [SymAnd](../../CslibFrontier/Computability/Circuit/Boolean/SymAnd.lean) is a separate depth-two model, not a `Circuit` basis: a multiset of AND gates over positive literals, counted with multiplicity, below an arbitrary symmetric gate `ℕ → Bool`. Size counts AND gates, and fan-in is the largest AND fan-in. A `ModPolyLayer` on a finite slot set updates every slot to whether an integer polynomial of the previous slots is nonzero modulo the layer's modulus. [SymAnd/Collapse](../../CslibFrontier/Computability/Circuit/Boolean/SymAnd/Collapse.lean) proves Beigel–Tarui's collapse (Lemma 2.8) for prime moduli. Suppose the primes, the slot-polynomial degrees and `log₂(|T|+1)` are at most `B`. Then a `SYM ∘ AND` circuit of fan-in `≤ B` and size `≤ 2^B` above `L` layers becomes one of fan-in `≤ (2B)^(5^L)` and size `≤ 2^((2B)^(5^L))`. The proof uses the amplifier `1 - p_k(q^(p-1))` modulo `p^k` from [ModulusAmplifier](../../CslibFrontier/Foundations/Data/Polynomial/ModulusAmplifier.lean). The collapse is a definition: [SymAnd/Mobius](../../CslibFrontier/Computability/Circuit/Boolean/SymAnd/Mobius.lean) defines the canonical circuit `SymAnd.ofLowDegree D M c out` of an integer function `c` of degree `≤ D`. Its AND gates are the sets of at most `D` positions, each repeated as often as the least residue modulo `M` of `c`'s subset Möbius coefficient, and its symmetric gate is `z ↦ out (z mod M)`. It computes `out (c x mod M)` with fan-in `≤ D` and size `≤ M(|T|+1)^D`. `SymAnd.collapseStep` is the canonical circuit of the amplified count, and `SymAnd.collapseRun` iterates it over a tower; the existence theorems are their corollaries. [SymAnd tests](../../CslibFrontierTests/Computability/Circuit/Boolean/SymAnd.lean) apply the tower theorem to a two-layer `MOD_2`/`MOD_3` tower and check that the resulting circuit takes both values. [Mobius tests](../../CslibFrontierTests/Computability/Circuit/Boolean/SymAnd/Mobius.lean) compute the canonical gates of two-bit functions, including a negative coefficient stored as its residue, and a truncation below the degree that changes the function.