refactor(modules): module migration

Complexitylib.lean

@@ -3,15 +3,17 @@ Copyright (c) 2025 Samuel Schlesinger. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Samuel Schlesinger
 -/
-import Complexitylib.Models
-import Complexitylib.Asymptotics
-import Complexitylib.TimeConstructible
-import Complexitylib.Classes
-import Complexitylib.Languages
-import Complexitylib.SAT
-import Complexitylib.Circuits
-import Complexitylib.BooleanAnalysis
-import Complexitylib.DescriptiveComplexity
+
+module
+public import Complexitylib.Models
+public import Complexitylib.Asymptotics
+public import Complexitylib.TimeConstructible
+public import Complexitylib.Classes
+public import Complexitylib.Languages
+public import Complexitylib.SAT
+public import Complexitylib.Circuits
+public import Complexitylib.BooleanAnalysis
+public import Complexitylib.DescriptiveComplexity
 
 /-!
 # Complexitylib

Complexitylib/Asymptotics.lean

@@ -3,15 +3,10 @@ Copyright (c) 2025 Samuel Schlesinger. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Samuel Schlesinger
 -/
-import Mathlib.Analysis.Asymptotics.Defs
-import Mathlib.Analysis.Asymptotics.SpecificAsymptotics
-import Mathlib.Analysis.Asymptotics.Lemmas
-import Mathlib.Algebra.Polynomial.Eval.Defs
-import Mathlib.Algebra.Polynomial.Eval.Degree
-import Mathlib.Data.Finset.Lattice.Fold
-import Mathlib.Data.Nat.Log
-import Mathlib.Data.Nat.Size
-import Mathlib.Algebra.Order.Floor.Semiring
+
+module
+public import Mathlib.Analysis.Asymptotics.SpecificAsymptotics
+public import Mathlib.Data.Nat.Size
 
 /-!
 # Asymptotic notation for natural number functions
@@ -51,6 +46,9 @@ opened and read like standard complexity-theoretic asymptotic notation.
 - `LittleO.const_mul_left` — constant multiple preserves little-o
 -/
 
+
+@[expose] public section
+
 open Asymptotics Filter
 
 namespace Complexity

Complexitylib/Asymptotics/PolynomialComposition.lean

@@ -3,7 +3,9 @@ Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Samuel Schlesinger
 -/
-import Complexitylib.Asymptotics
+
+module
+public import Complexitylib.Asymptotics
 
 /-!
 # Polynomial composition bounds
@@ -18,6 +20,9 @@ deterministic function computations are connected sequentially.
 - `BigO.polynomial_composition_time` — the coarse sequential runtime is polynomially bounded
 -/
 
+
+@[expose] public section
+
 namespace Complexity
 
 /-- Composing evaluations of natural-coefficient polynomials gives a function

Complexitylib/BooleanAnalysis.lean

@@ -3,7 +3,9 @@ Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Samuel Schlesinger
 -/
-import Complexitylib.BooleanAnalysis.FourierExpansion
+
+module
+public import Complexitylib.BooleanAnalysis.FourierExpansion
 
 /-!
 # Analysis of Boolean functions

Complexitylib/BooleanAnalysis/FourierExpansion.lean

@@ -3,8 +3,10 @@ Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Samuel Schlesinger
 -/
-import Complexitylib.BooleanAnalysis.FourierExpansion.Internal
-import Mathlib.Probability.ProbabilityMassFunction.Constructions
+
+module
+public import Complexitylib.BooleanAnalysis.FourierExpansion.Internal
+public import Mathlib.Probability.ProbabilityMassFunction.Constructions
 
 /-!
 # Chapter 1: Boolean functions and the Fourier expansion
@@ -17,6 +19,9 @@ Functions" by Ryan O'Donnell.
 * Ryan O'Donnell, *Analysis of Boolean Functions*, Chapter 1.
 -/
 
+
+@[expose] public section
+
 namespace Complexity
 
 namespace BooleanAnalysis

Complexitylib/BooleanAnalysis/FourierExpansion/Defs.lean

@@ -3,9 +3,10 @@ Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Samuel Schlesinger
 -/
-import Mathlib.Algebra.BigOperators.Expect
-import Mathlib.Analysis.InnerProductSpace.Basic
-import Mathlib.Data.ZMod.Basic
+
+module
+public import Mathlib.Analysis.Complex.Order
+public import Mathlib.Analysis.InnerProductSpace.Defs
 
 /-!
 # Chapter 1: Boolean functions and the Fourier expansion — Definitions
@@ -42,6 +43,9 @@ the book's conventions:
 * `Pr₂[P]` — joint uniform probability over pairs
 -/
 
+
+@[expose] public section
+
 namespace Complexity
 
 namespace BooleanAnalysis
@@ -154,7 +158,7 @@ noncomputable instance instCore : PreInnerProductSpace.Core ℝ (BooleanFunction
   toInner := instInner
   conj_inner_symm f g := by simp [inner_comm f g]
   re_inner_nonneg f := by simp [inner_self_nonneg' f]
-  add_left := inner_add_left
+  add_left := by exact inner_add_left
   smul_left f g r := by rw [inner_smul_left]; simp
 
 -- `instFullCore` adds the definiteness axiom (`‖f‖ = 0 → f = 0`) needed to upgrade
@@ -164,7 +168,7 @@ noncomputable instance instCore : PreInnerProductSpace.Core ℝ (BooleanFunction
 -- from the same inner product, so there is no diamond.
 noncomputable instance instFullCore : InnerProductSpace.Core ℝ (BooleanFunction n) where
   toCore := instCore
-  definite := @inner_self_eq_zero n
+  definite := by exact @inner_self_eq_zero n
 
 noncomputable instance : NormedAddCommGroup (BooleanFunction n) :=
   @InnerProductSpace.Core.toNormedAddCommGroup ℝ _ _ _ _ instFullCore

Complexitylib/BooleanAnalysis/FourierExpansion/Internal.lean

@@ -3,8 +3,11 @@ Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Samuel Schlesinger
 -/
-import Complexitylib.BooleanAnalysis.FourierExpansion.Defs
-import Mathlib.Analysis.InnerProductSpace.PiL2
+
+module
+public import Complexitylib.BooleanAnalysis.FourierExpansion.Defs
+public import Mathlib.Analysis.InnerProductSpace.PiL2
+public import Std.Tactic.BVDecide.Normalize.Prop
 
 /-!
 # Chapter 1: Boolean functions and the Fourier expansion — Internal lemmas
@@ -14,6 +17,9 @@ main results in `BooleanAnalysis.FourierExpansion` but are not intended for
 direct use by downstream code.
 -/
 
+
+@[expose] public section
+
 namespace Complexity
 
 namespace BooleanAnalysis.Internal

Complexitylib/Circuits.lean

@@ -3,59 +3,61 @@ Copyright (c) 2025 Samuel Schlesinger. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Samuel Schlesinger
 -/
-import Complexitylib.Circuits.Basic
-import Complexitylib.Circuits.BitString
-import Complexitylib.Circuits.Composition
-import Complexitylib.Circuits.Dependency
-import Complexitylib.Circuits.DecisionTree
-import Complexitylib.Circuits.DecisionTree.Finite
-import Complexitylib.Circuits.DecisionTree.NormalForm
-import Complexitylib.Circuits.DecisionTree.Path
-import Complexitylib.Circuits.DecisionTree.Restriction
-import Complexitylib.Circuits.Formula
-import Complexitylib.Circuits.Spira
-import Complexitylib.Circuits.FormulaEncoding
-import Complexitylib.Circuits.CircuitFormula
-import Complexitylib.Circuits.Restriction
-import Complexitylib.Circuits.RandomRestriction
-import Complexitylib.Circuits.BranchingProgram
-import Complexitylib.Circuits.Barrington
-import Complexitylib.Circuits.BarringtonS5
-import Complexitylib.Circuits.BarringtonBridge
-import Complexitylib.Circuits.BarringtonRepr
-import Complexitylib.Circuits.BarringtonLength
-import Complexitylib.Circuits.BarringtonCompiler
-import Complexitylib.Circuits.BranchingProgramEncoding
-import Complexitylib.Circuits.BarringtonCodeGenerator
-import Complexitylib.Circuits.BarringtonFamily
-import Complexitylib.Circuits.BarringtonConverse
-import Complexitylib.Circuits.BarringtonTyped
-import Complexitylib.Circuits.CircuitFormula.Family
-import Complexitylib.Circuits.MultilinearExtension
-import Complexitylib.Circuits.NormalForm
-import Complexitylib.Circuits.NormalForm.Operations
-import Complexitylib.Circuits.NormalForm.Restriction
-import Complexitylib.Circuits.AndOrNot
-import Complexitylib.Circuits.BasisHom
-import Complexitylib.Circuits.Threshold
-import Complexitylib.Circuits.Monotone
-import Complexitylib.Circuits.KarchmerWigderson
-import Complexitylib.Circuits.Encoding
-import Complexitylib.Circuits.Family
-import Complexitylib.Circuits.Encoding.Family
-import Complexitylib.Circuits.Encoding.Machine
-import Complexitylib.Circuits.XOR
-import Complexitylib.Circuits.XOR.Restriction
-import Complexitylib.Circuits.EssentialInput
-import Complexitylib.Circuits.Shannon
-import Complexitylib.Circuits.LowerBound
-import Complexitylib.Circuits.Schnorr
-import Complexitylib.Circuits.DepthClasses
-import Complexitylib.Circuits.AC0
-import Complexitylib.Circuits.Nondeterminism
-import Complexitylib.Circuits.Hardwiring
-import Complexitylib.Circuits.Unrolling
-import Complexitylib.Circuits.Valiant
+
+module
+public import Complexitylib.Circuits.Basic
+public import Complexitylib.Circuits.BitString
+public import Complexitylib.Circuits.Composition
+public import Complexitylib.Circuits.Dependency
+public import Complexitylib.Circuits.DecisionTree
+public import Complexitylib.Circuits.DecisionTree.Finite
+public import Complexitylib.Circuits.DecisionTree.NormalForm
+public import Complexitylib.Circuits.DecisionTree.Path
+public import Complexitylib.Circuits.DecisionTree.Restriction
+public import Complexitylib.Circuits.Formula
+public import Complexitylib.Circuits.Spira
+public import Complexitylib.Circuits.FormulaEncoding
+public import Complexitylib.Circuits.CircuitFormula
+public import Complexitylib.Circuits.Restriction
+public import Complexitylib.Circuits.RandomRestriction
+public import Complexitylib.Circuits.BranchingProgram
+public import Complexitylib.Circuits.Barrington
+public import Complexitylib.Circuits.BarringtonS5
+public import Complexitylib.Circuits.BarringtonBridge
+public import Complexitylib.Circuits.BarringtonRepr
+public import Complexitylib.Circuits.BarringtonLength
+public import Complexitylib.Circuits.BarringtonCompiler
+public import Complexitylib.Circuits.BranchingProgramEncoding
+public import Complexitylib.Circuits.BarringtonCodeGenerator
+public import Complexitylib.Circuits.BarringtonFamily
+public import Complexitylib.Circuits.BarringtonConverse
+public import Complexitylib.Circuits.BarringtonTyped
+public import Complexitylib.Circuits.CircuitFormula.Family
+public import Complexitylib.Circuits.MultilinearExtension
+public import Complexitylib.Circuits.NormalForm
+public import Complexitylib.Circuits.NormalForm.Operations
+public import Complexitylib.Circuits.NormalForm.Restriction
+public import Complexitylib.Circuits.AndOrNot
+public import Complexitylib.Circuits.BasisHom
+public import Complexitylib.Circuits.Threshold
+public import Complexitylib.Circuits.Monotone
+public import Complexitylib.Circuits.KarchmerWigderson
+public import Complexitylib.Circuits.Encoding
+public import Complexitylib.Circuits.Family
+public import Complexitylib.Circuits.Encoding.Family
+public import Complexitylib.Circuits.Encoding.Machine
+public import Complexitylib.Circuits.XOR
+public import Complexitylib.Circuits.XOR.Restriction
+public import Complexitylib.Circuits.EssentialInput
+public import Complexitylib.Circuits.Shannon
+public import Complexitylib.Circuits.LowerBound
+public import Complexitylib.Circuits.Schnorr
+public import Complexitylib.Circuits.DepthClasses
+public import Complexitylib.Circuits.AC0
+public import Complexitylib.Circuits.Nondeterminism
+public import Complexitylib.Circuits.Hardwiring
+public import Complexitylib.Circuits.Unrolling
+public import Complexitylib.Circuits.Valiant
 
 /-! # Circuit Complexity Library
 

Complexitylib/Circuits/AC0.lean

@@ -3,16 +3,17 @@ Copyright (c) 2025 Samuel Schlesinger. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Samuel Schlesinger
 -/
-import Complexitylib.Circuits.AC0.Defs
-import Complexitylib.Circuits.AC0.NormalForm
-import Complexitylib.Circuits.AC0.Normalization
-import Complexitylib.Circuits.AC0.Restriction
-import Complexitylib.Circuits.AC0.Switching
-import Complexitylib.Circuits.AC0.Switching.Collection
-import Complexitylib.Circuits.AC0.Switching.Parity
-import Complexitylib.Circuits.AC0.Iteration
-import Complexitylib.Circuits.AC0.Parity
-import Complexitylib.Circuits.DepthClasses
+
+module
+public import Complexitylib.Circuits.AC0.Defs
+public import Complexitylib.Circuits.AC0.NormalForm
+public import Complexitylib.Circuits.AC0.Normalization
+public import Complexitylib.Circuits.AC0.Restriction
+public import Complexitylib.Circuits.AC0.Switching
+public import Complexitylib.Circuits.AC0.Switching.Collection
+public import Complexitylib.Circuits.AC0.Switching.Parity
+public import Complexitylib.Circuits.AC0.Iteration
+public import Complexitylib.Circuits.AC0.Parity
 
 /-!
 # The class AC⁰

Complexitylib/Circuits/AC0/Defs.lean

@@ -3,12 +3,17 @@ Copyright (c) 2025 Samuel Schlesinger. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Samuel Schlesinger
 -/
-import Complexitylib.Circuits.DepthClasses.Defs
+
+module
+public import Mathlib.Data.Finset.Attr
+public import Mathlib.Tactic.Bound.Init
+public import Mathlib.Tactic.Finiteness.Attr
+public import Mathlib.Tactic.SetLike
 
 /-!
 # AC0 -- compatibility import
 
 `Complexity.AC0` now lives with the complete `DEPTH`/`NC`/`AC` hierarchy in
 `Complexitylib.Circuits.DepthClasses.Defs`. This module preserves the original
-import path.
+public import path.
 -/

Complexitylib/Circuits/AC0/Iteration.lean

@@ -3,8 +3,10 @@ Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Samuel Schlesinger
 -/
-import Complexitylib.Circuits.AC0.Iteration.Defs
-import Complexitylib.Circuits.AC0.Iteration.Internal
+
+module
+public import Complexitylib.Circuits.AC0.Iteration.Defs
+public import Complexitylib.Circuits.AC0.Iteration.Internal
 
 /-!
 # Iterated switching for finite AC0 formulas
@@ -18,6 +20,9 @@ Everything here is a statement about one finite formula and a finite product
 of restrictions. No uniformity or circuit-generator assumption is present.
 -/
 
+
+@[expose] public section
+
 namespace Complexity
 
 namespace RandomRestriction

Complexitylib/Circuits/AC0/Iteration/Defs.lean

@@ -3,12 +3,13 @@ Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Samuel Schlesinger
 -/
-import Complexitylib.Circuits.AC0.Restriction
-import Complexitylib.Circuits.AC0.Switching.Defs
-import Complexitylib.Circuits.DecisionTree.NormalForm.Defs
-import Complexitylib.Circuits.RandomRestriction.Defs
-import Mathlib.Data.Fintype.BigOperators
-import Mathlib.Data.Fintype.Card
+
+module
+public import Complexitylib.Circuits.AC0.Switching.Defs
+public import Complexitylib.Circuits.DecisionTree.NormalForm.Defs
+public import Complexitylib.Circuits.RandomRestriction.Defs
+public import Complexitylib.Circuits.AC0.NormalForm.Defs
+public import Mathlib.Algebra.BigOperators.Group.Finset.Defs
 
 /-!
 # Iterated switching for AC0 formulas -- definitions
@@ -21,6 +22,9 @@ This representation is finite and nonuniform. It contains restrictions and
 formula trees only; it does not contain or assume a circuit generator.
 -/
 
+
+@[expose] public section
+
 namespace Complexity
 
 open scoped BigOperators