SamuelSchlesinger · BoltonBailey · Aug 2, 2026 · Aug 2, 2026 · Aug 2, 2026
diff --git a/.gitignore b/.gitignore
@@ -1,5 +1,8 @@
 /.lake
 docbuild/.lake
 .codex/
+.shake-minimize.json
+.expose-minimize.json
+scripts/__pycache__/
 arora-barak-draft.pdf
 .claude/
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
@@ -181,6 +181,57 @@ The last three are the quality gates:
 API documentation builds with doc-gen4 from the `docbuild/` subproject
 (`cd docbuild && lake build Complexitylib:docs`); CI publishes it weekly.
 
+## Minimizing module interfaces
+
+A module's interface is what every downstream module must rebuild against.
+Two things inflate it: `public import X` re-exports X to everything
+downstream, and `@[expose]` puts a definition's *body* in the interface rather
+than just its signature. They also constrain each other — a `public`
+declaration's signature may only mention names from `public` imports, and an
+*exposed* definition's body must too — so de-exposing is what makes some
+import demotions legal in the first place.
+
+`lake shake` reports the import half:
+
+```bash
+lake build --wfail        # shake reads the .oleans, so build first
+lake shake                # report only
+lake shake --explain      # also show which constants require each import
+```
+
+`scripts/shake_minimize.py` turns both halves into a verified minimization
+pass. It applies only *removals* — `@[expose] public section` → `public
+section`, `public import X` → `import X`, or dropping an unused import — and
+runs the full five-target gate build after each change, reverting anything
+that breaks. Run the expose pass first:
+
+```bash
+python3 scripts/shake_minimize.py --state .expose-minimize.json scan-expose
+python3 scripts/shake_minimize.py --state .expose-minimize.json apply
+
+lake build --wfail
+python3 scripts/shake_minimize.py scan --retry-reverted
+python3 scripts/shake_minimize.py apply
+python3 scripts/shake_minimize.py report -v
+```
+
+Shake's suggested *additions* are deliberately ignored, so the script can only
+shrink an interface; a demotion that would have needed a compensating import
+downstream simply fails its build and is rolled back. Nothing is ever made to
+build by adjusting a proof.
+
+State lives in the file named by `--state` (gitignored) and is rewritten after
+every verified step, so `apply` can be interrupted with Ctrl-C or `kill` and
+resumed. Because each candidate costs a real build, a full pass takes hours;
+use `--time-budget MINUTES` to run it in slices. Expose candidates are ordered
+by transitive dependent count ascending, which puts the cheap, near-certain
+wins first. Re-running a scan after a pass finds candidates newly exposed by
+it, and `--retry-reverted` re-queues ones an earlier pass rejected.
+
+Two shake annotations are honoured: `import X -- shake: keep` pins a single
+import and `module -- shake: keep-all` pins a whole file. `meta import` lines
+are never touched.
+
 ## Choosing a Contribution
 
 See [ROADMAP.md](ROADMAP.md) for dependency-ordered research programs and

diff --git a/Complexitylib/Asymptotics/PolynomialComposition.lean b/Complexitylib/Asymptotics/PolynomialComposition.lean
@@ -21,7 +21,7 @@ deterministic function computations are connected sequentially.
 -/
 
 
-@[expose] public section
+public section
 
 namespace Complexity
 

diff --git a/Complexitylib/BooleanAnalysis/FourierExpansion.lean b/Complexitylib/BooleanAnalysis/FourierExpansion.lean
@@ -20,7 +20,7 @@ Functions" by Ryan O'Donnell.
 -/
 
 
-@[expose] public section
+public section
 
 namespace Complexity
 

diff --git a/Complexitylib/BooleanAnalysis/FourierExpansion/Internal.lean b/Complexitylib/BooleanAnalysis/FourierExpansion/Internal.lean
@@ -18,7 +18,7 @@ direct use by downstream code.
 -/
 
 
-@[expose] public section
+public section
 
 namespace Complexity
 

diff --git a/Complexitylib/Circuits/AC0/Iteration.lean b/Complexitylib/Circuits/AC0/Iteration.lean
@@ -21,7 +21,7 @@ of restrictions. No uniformity or circuit-generator assumption is present.
 -/
 
 
-@[expose] public section
+public section
 
 namespace Complexity
 

diff --git a/Complexitylib/Circuits/AC0/Iteration/Internal.lean b/Complexitylib/Circuits/AC0/Iteration/Internal.lean
@@ -17,7 +17,7 @@ public import Complexitylib.Circuits.AC0.NormalForm.Internal
 -/
 
 
-@[expose] public section
+public section
 
 namespace Complexity
 

diff --git a/Complexitylib/Circuits/AC0/NormalForm.lean b/Complexitylib/Circuits/AC0/NormalForm.lean
@@ -17,7 +17,7 @@ restriction arguments.
 -/
 
 
-@[expose] public section
+public section
 
 namespace Complexity
 namespace AC0Formula

diff --git a/Complexitylib/Circuits/AC0/NormalForm/Internal.lean b/Complexitylib/Circuits/AC0/NormalForm/Internal.lean
@@ -12,7 +12,7 @@ public import Complexitylib.Circuits.AC0.NormalForm.Defs
 -/
 
 
-@[expose] public section
+public section
 
 namespace Complexity
 namespace AC0Formula

diff --git a/Complexitylib/Circuits/AC0/Normalization.lean b/Complexitylib/Circuits/AC0/Normalization.lean
@@ -23,7 +23,7 @@ No uniformity assumption is used.
 -/
 
 
-@[expose] public section
+public section
 
 namespace Complexity
 

diff --git a/Complexitylib/Circuits/AC0/Normalization/Internal.lean b/Complexitylib/Circuits/AC0/Normalization/Internal.lean
@@ -30,7 +30,7 @@ public import Mathlib.Tactic.ReduceModChar
 -/
 
 
-@[expose] public section
+public section
 
 namespace Complexity
 

diff --git a/Complexitylib/Circuits/AC0/Parity.lean b/Complexitylib/Circuits/AC0/Parity.lean
@@ -25,7 +25,7 @@ bound and a fixed depth.
 -/
 
 
-@[expose] public section
+public section
 
 namespace Complexity
 namespace AC0Formula

diff --git a/Complexitylib/Circuits/AC0/Parity/Internal.lean b/Complexitylib/Circuits/AC0/Parity/Internal.lean
@@ -13,7 +13,7 @@ public import Complexitylib.Circuits.XOR.Restriction.Internal
 -/
 
 
-@[expose] public section
+public section
 
 namespace Complexity
 namespace AC0Formula

diff --git a/Complexitylib/Circuits/AC0/Restriction.lean b/Complexitylib/Circuits/AC0/Restriction.lean
@@ -18,7 +18,7 @@ filtered to the free variables.
 -/
 
 
-@[expose] public section
+public section
 
 namespace Complexity
 namespace AC0Formula

diff --git a/Complexitylib/Circuits/AC0/Switching.lean b/Complexitylib/Circuits/AC0/Switching.lean
@@ -19,7 +19,7 @@ bounded literal positions, branch bits, and phase markers.
 -/
 
 
-@[expose] public section
+public section
 
 namespace Complexity
 

diff --git a/Complexitylib/Circuits/AC0/Switching/Collection.lean b/Complexitylib/Circuits/AC0/Switching/Collection.lean
@@ -18,7 +18,7 @@ assumption is involved.
 -/
 
 
-@[expose] public section
+public section
 
 namespace Complexity
 

diff --git a/Complexitylib/Circuits/AC0/Switching/Collection/Internal.lean b/Complexitylib/Circuits/AC0/Switching/Collection/Internal.lean
@@ -15,7 +15,7 @@ public import Mathlib.Algebra.Order.BigOperators.Group.Finset
 -/
 
 
-@[expose] public section
+public section
 
 namespace Complexity
 

diff --git a/Complexitylib/Circuits/AC0/Switching/Internal.lean b/Complexitylib/Circuits/AC0/Switching/Internal.lean
@@ -16,7 +16,7 @@ public import Complexitylib.Circuits.DecisionTree.Path.Internal
 -/
 
 
-@[expose] public section
+public section
 
 namespace Complexity
 

diff --git a/Complexitylib/Circuits/AC0/Switching/Parity.lean b/Complexitylib/Circuits/AC0/Switching/Parity.lean
@@ -21,7 +21,7 @@ without changing semantics or increasing width.
 -/
 
 
-@[expose] public section
+public section
 
 namespace Complexity
 

diff --git a/Complexitylib/Circuits/AC0/Switching/Parity/Internal.lean b/Complexitylib/Circuits/AC0/Switching/Parity/Internal.lean
@@ -13,7 +13,7 @@ public import Complexitylib.Circuits.XOR.Restriction.Internal
 -/
 
 
-@[expose] public section
+public section
 
 namespace Complexity
 

diff --git a/Complexitylib/Circuits/AndOrNot.lean b/Complexitylib/Circuits/AndOrNot.lean
@@ -29,7 +29,7 @@ This module provides the AND/OR basis definitions and completeness results.
 -/
 
 
-@[expose] public section
+public section
 
 namespace Complexity
 

diff --git a/Complexitylib/Circuits/BarringtonBridge.lean b/Complexitylib/Circuits/BarringtonBridge.lean
@@ -33,7 +33,7 @@ actually consumes — where the *target* representing cycle is an arbitrary
 -/
 
 
-@[expose] public section
+public section
 
 open scoped commutatorElement
 open Equiv

diff --git a/Complexitylib/Circuits/BarringtonCodeGenerator.lean b/Complexitylib/Circuits/BarringtonCodeGenerator.lean
@@ -30,7 +30,7 @@ evaluation matches the source formula, and its instruction count is at most
 -/
 
 
-@[expose] public section
+public section
 
 namespace Complexity
 

diff --git a/Complexitylib/Circuits/BarringtonCodeGenerator/Internal.lean b/Complexitylib/Circuits/BarringtonCodeGenerator/Internal.lean
@@ -14,7 +14,7 @@ public import Complexitylib.Circuits.FormulaEncoding
 -/
 
 
-@[expose] public section
+public section
 
 namespace Complexity
 

diff --git a/Complexitylib/Circuits/BarringtonCompiler.lean b/Complexitylib/Circuits/BarringtonCompiler.lean
@@ -36,7 +36,7 @@ proof, not extraction of program data from an existential theorem.
 -/
 
 
-@[expose] public section
+public section
 
 open scoped commutatorElement
 open Equiv

diff --git a/Complexitylib/Circuits/BarringtonCompiler/Internal.lean b/Complexitylib/Circuits/BarringtonCompiler/Internal.lean
@@ -14,7 +14,7 @@ public import Std.Tactic.BVDecide.Normalize.BitVec
 -/
 
 
-@[expose] public section
+public section
 
 open scoped commutatorElement
 open Equiv

diff --git a/Complexitylib/Circuits/BarringtonConverse.lean b/Complexitylib/Circuits/BarringtonConverse.lean
@@ -29,7 +29,7 @@ equivalence under the library's total-assignment family convention.
 -/
 
 
-@[expose] public section
+public section
 
 namespace Complexity
 

diff --git a/Complexitylib/Circuits/BarringtonConverse/Internal.lean b/Complexitylib/Circuits/BarringtonConverse/Internal.lean
@@ -15,7 +15,7 @@ evaluation, then lifts that construction to polynomial-length families.
 -/
 
 
-@[expose] public section
+public section
 
 open Equiv
 

diff --git a/Complexitylib/Circuits/BarringtonLength.lean b/Complexitylib/Circuits/BarringtonLength.lean
@@ -39,7 +39,7 @@ the classical `4 ^ depth` bound.
 -/
 
 
-@[expose] public section
+public section
 
 open scoped commutatorElement
 open Equiv

diff --git a/Complexitylib/Circuits/BarringtonRepr.lean b/Complexitylib/Circuits/BarringtonRepr.lean
@@ -43,7 +43,7 @@ converse live in `BarringtonFamily.lean` and `BarringtonConverse.lean`.
 -/
 
 
-@[expose] public section
+public section
 
 open scoped commutatorElement
 open Equiv

diff --git a/Complexitylib/Circuits/BarringtonS5.lean b/Complexitylib/Circuits/BarringtonS5.lean
@@ -44,7 +44,7 @@ output cycle.
 -/
 
 
-@[expose] public section
+public section
 
 open scoped commutatorElement
 open Equiv

diff --git a/Complexitylib/Circuits/BarringtonTyped.lean b/Complexitylib/Circuits/BarringtonTyped.lean
@@ -25,7 +25,7 @@ model stores the unique zero-input answer separately.
 -/
 
 
-@[expose] public section
+public section
 
 namespace Complexity
 

diff --git a/Complexitylib/Circuits/BarringtonTyped/Internal.lean b/Complexitylib/Circuits/BarringtonTyped/Internal.lean
@@ -14,7 +14,7 @@ public import Complexitylib.Circuits.BarringtonTyped.Defs
 -/
 
 
-@[expose] public section
+public section
 
 namespace Complexity
 

diff --git a/Complexitylib/Circuits/BasisHom.lean b/Complexitylib/Circuits/BasisHom.lean
@@ -17,7 +17,7 @@ gate count, wiring, and depth exactly.
 -/
 
 
-@[expose] public section
+public section
 
 namespace Complexity
 

diff --git a/Complexitylib/Circuits/BasisHom/Internal.lean b/Complexitylib/Circuits/BasisHom/Internal.lean
@@ -12,7 +12,7 @@ public import Complexitylib.Circuits.BasisHom.Defs
 -/
 
 
-@[expose] public section
+public section
 
 namespace Complexity
 

diff --git a/Complexitylib/Circuits/BranchingProgramEncoding.lean b/Complexitylib/Circuits/BranchingProgramEncoding.lean
@@ -31,7 +31,7 @@ finite permutation proofs on the machine tape.
 -/
 
 
-@[expose] public section
+public section
 
 namespace Complexity
 

diff --git a/Complexitylib/Circuits/BranchingProgramEncoding/Internal.lean b/Complexitylib/Circuits/BranchingProgramEncoding/Internal.lean
@@ -34,7 +34,7 @@ Public statements are re-exported by
 -/
 
 
-@[expose] public section
+public section
 
 set_option maxRecDepth 100000
 

diff --git a/Complexitylib/Circuits/CircuitFormula.lean b/Complexitylib/Circuits/CircuitFormula.lean
@@ -33,7 +33,7 @@ size claim.
 -/
 
 
-@[expose] public section
+public section
 
 namespace Complexity
 

diff --git a/Complexitylib/Circuits/CircuitFormula/Defs.lean b/Complexitylib/Circuits/CircuitFormula/Defs.lean
@@ -17,7 +17,7 @@ formula tree; no formula-size claim is implicit in this bridge.
 -/
 
 
-@[expose] public section
+public section
 
 namespace Complexity
-Original file line number
+Diff line change
@@ Expand Up @@
     -/
-    @[expose] public section
+    public section
     namespace Complexity
@@ Expand Down @@