chore: agent-driven modulize

CLAUDE.md

@@ -44,7 +44,9 @@ Complexitylib/Models/TuringMachine.lean          — Γ, Dir3, TM, NTM, Cfg, ste
 Complexitylib/Models/TuringMachine/Internal.lean — proof internals (e.g. toNTM_accepts_iff)
 ```
 
-Aggregation files (`Complexitylib.lean`, `Models.lean`) contain only `import` statements — no definitions.
+Aggregation files (`Complexitylib.lean`, `Models.lean`) contain only `import`
+statements — no definitions (a leading `module` header and `public import`s, but
+nothing else).
 
 ### Three-Layer Architecture
 
@@ -78,7 +80,53 @@ definitions in their theorem signatures rather than raw expressions.
 For simple modules where Internal proofs don't need to reference surface
 definitions, the two-layer pattern (surface + Internal) is fine — introduce
 `Defs.lean` when the need arises. For trivial proofs, `private` lemmas in the
-same file are acceptable.
+same file are acceptable — but only if no `@[expose] public` declaration
+references them (see the Module System section); otherwise they must be public.
+
+### Module System
+
+Every `.lean` file uses Lean's module system. The layout is:
+
+```lean
+/- copyright header -/
+module
+
+public import Mathlib.…
+public import Complexitylib.…
+
+/-! module docstring -/
+
+@[expose] public section
+
+namespace Complexity
+…
+end Complexity
+```
+
+Conventions (matching Mathlib):
+
+- **`module` header + `public import`**: every file (including aggregation
+  files) begins with `module`, and all imports are `public import` so the
+  public interface is re-exported transitively. A `module` file can only
+  import other `module` files.
+- **`@[expose] public section`**: wraps the whole body so definitions stay
+  exposed (reducible/unfoldable) downstream, preserving pre-module defeq
+  behavior. This is the default the `Modulize` migration script emits.
+- **No `private` under an exposed section**: an `@[expose] public` definition
+  cannot reference a `private` declaration — the exposed body must be
+  reconstructible by importers. Make such helpers public (drop `private`)
+  rather than private. `private` is only safe for helpers used exclusively by
+  other non-exposed / `private` declarations.
+- **Meta imports for tactics**: tactic and macro (meta) code is *not*
+  re-exported transitively through a plain `public import` chain. A file that
+  uses a tactic (e.g. `ring`) reached only transitively must import the tactic
+  module directly (`public import Mathlib.Tactic.Ring`). The same applies to
+  `to_additive`-generated lemmas whose defining module isn't in the direct
+  import closure.
+- To migrate a new un-modulized file, run the Lean `Modulize` script:
+  `lake env lean --run script/Modulize.lean path/to/File.lean` (from the
+  `leanprover/lean4` repo), then resolve any private-exposure and meta-import
+  fallout as above.
 
 ### Key Design Decisions
 
@@ -109,7 +157,7 @@ Follow Mathlib style:
 
 ### Common Pitfalls
 
-- **No `module` keyword** in aggregation files — they import files with definitions, and `module` files can only import other `module` files.
+- **Module system**: every file (including aggregation files) starts with a `module` header and uses `public import`; see the Module System section above for the `private`/`@[expose]` and meta-import rules.
 - **`List.get?` removed**: Use `l[i]?` (GetElem? syntax) instead of `l.get? i` in Lean 4 v4.28.0+.
 - **Lambda expressions in conjunction chains** need explicit parens: `c'.work = (fun i => ...) ∧ ...`
 - **`open` scoping**: Prefer `open Foo in` or `section`/`end` blocks over module-level `open` to avoid namespace pollution.

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
@@ -65,3 +67,5 @@ hardwiring and its advice corollary live in
 logarithmic-depth Boolean formula families with polynomial-length width-`5`
 permutation branching-program families.
 -/
+
+@[expose] public section

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,8 @@ 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,8 @@ 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
@@ -20,3 +22,5 @@ an orthonormal basis, Fourier coefficients and weights, Parseval/Plancherel, and
 the mean/variance/covariance and convolution API. All definitions and theorems
 live under the `Complexity.BooleanAnalysis` namespace.
 -/
+
+@[expose] public section

Complexitylib/BooleanAnalysis/FourierExpansion.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.Internal
-import Mathlib.Probability.ProbabilityMassFunction.Constructions
+module
+
+public import Complexitylib.BooleanAnalysis.FourierExpansion.Internal
+public import Mathlib.Probability.ProbabilityMassFunction.Constructions
+import Std.Tactic.BVDecide.Normalize.Prop
 
 /-!
 # Chapter 1: Boolean functions and the Fourier expansion
@@ -17,6 +20,8 @@ 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.InnerProductSpace.Basic
+public import Mathlib.Data.ZMod.Basic
 
 /-!
 # Chapter 1: Boolean functions and the Fourier expansion — Definitions
@@ -42,6 +43,8 @@ the book's conventions:
 * `Pr₂[P]` — joint uniform probability over pairs
 -/
 
+@[expose] public section
+
 namespace Complexity
 
 namespace BooleanAnalysis
@@ -117,26 +120,26 @@ noncomputable instance instInner : Inner ℝ (BooleanFunction n) where
 theorem inner_def (f g : BooleanFunction n) :
     @inner ℝ _ instInner f g = (1 / (2 : ℝ) ^ n) * ∑ x : Cube n, f x * g x := rfl
 
-private theorem inner_comm (f g : BooleanFunction n) :
+theorem inner_comm (f g : BooleanFunction n) :
     @inner ℝ _ instInner f g = @inner ℝ _ instInner g f := by
   simp only [inner_def]; congr 1; apply Finset.sum_congr rfl; intro x _; ring
 
-private theorem inner_add_left (f g h : BooleanFunction n) :
+theorem inner_add_left (f g h : BooleanFunction n) :
     @inner ℝ _ instInner (f + g) h = @inner ℝ _ instInner f h + @inner ℝ _ instInner g h := by
   simp only [inner_def, add_apply, add_mul, Finset.sum_add_distrib, mul_add]
 
-private theorem inner_smul_left (r : ℝ) (f g : BooleanFunction n) :
+theorem inner_smul_left (r : ℝ) (f g : BooleanFunction n) :
     @inner ℝ _ instInner (r • f) g = r * @inner ℝ _ instInner f g := by
   simp only [inner_def, smul_apply, Finset.mul_sum]; ring_nf
 
-private theorem inner_self_nonneg' (f : BooleanFunction n) :
+theorem inner_self_nonneg' (f : BooleanFunction n) :
     0 ≤ @inner ℝ _ instInner f f := by
   simp only [inner_def]
   apply mul_nonneg
   · positivity
   · apply Finset.sum_nonneg; intro x _; exact mul_self_nonneg (f x)
 
-private theorem inner_self_eq_zero {f : BooleanFunction n}
+theorem inner_self_eq_zero {f : BooleanFunction n}
     (h : @inner ℝ _ instInner f f = 0) : f = 0 := by
   simp only [inner_def] at h
   have h2n : (0 : ℝ) < 1 / 2 ^ n := by positivity

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
+import Std.Tactic.BVDecide.Normalize.Prop
 
 /-!
 # Chapter 1: Boolean functions and the Fourier expansion — Internal lemmas
@@ -14,6 +17,8 @@ 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
 
@@ -236,3 +238,5 @@ Theorem modules (re-export definitions + main results):
 Internal modules contain proof machinery (CircDesc, DNF construction,
 restriction/elimination arguments) and are not intended for direct use.
 -/
+
+@[expose] public section