Optimize GapCVP build dependencies and row-count elaboration

LeanPool/GapCVP.lean

@@ -4,9 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: OpenAI, Dean Cureton
 -/
 
-module
+module -- shake: keep-all
 
+-- Preserve the historical public API while proof modules use narrower dependencies.
 public import LeanPool.GapCVP.Part18
+public import LeanPool.GapCVP.Part16 -- shake: keep
+public import LeanPool.GapCVP.Part17 -- shake: keep
 
 /-!
 # Polynomial-factor hardness of the closest vector problem
@@ -37,7 +40,9 @@ statements stable when updating the proof modules. Their public `PromiseProblem`
 remain behind that interface.
 
 For Mathlib updates, repair the shared trace/composition helpers before individual machine
-proofs, then run `lake build LeanPool.GapCVP` and the project linters. The source modules follow
-dependency order, so a focused rebuild checks the affected suffix without rebuilding other
-pooled projects. The large Turing-machine layer remains a maintenance cost of this import.
+proofs, then run `lake build LeanPool.GapCVP` and the project linters. Proof modules import their
+dependencies directly and keep proof-only imports private. The numbered entry modules retain
+their historical public exports, so focused rebuilds follow the proof dependencies without
+rebuilding other pooled projects. The large Turing-machine layer remains a maintenance cost
+of this import.
 -/

LeanPool/GapCVP/Part01.lean

@@ -4,8 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: OpenAI, Dean Cureton
 -/
 
-module
+module -- shake: keep-all
 
 public import LeanPool.GapCVP.Part01B
+public import Mathlib.Algebra.Module.ZLattice.Basic -- shake: keep
 
 /-! # GapCVP proof, part 01 -/

LeanPool/GapCVP/Part01A.lean

@@ -4,14 +4,16 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: OpenAI, Dean Cureton
 -/
 
-module
+module -- shake: keep-all
 
 public import Mathlib.Algebra.Group.Translate
-public import Mathlib.Algebra.Module.ZLattice.Basic
+import Mathlib.Algebra.Module.ZLattice.Basic
 public import Mathlib.Algebra.Order.Ring.Star
 public import Mathlib.Algebra.Order.Star.Real
 public import Mathlib.Computability.Language
 public import Mathlib.Computability.TuringMachine.Computable
+public import Mathlib.Analysis.InnerProductSpace.PiL2
+public import Mathlib.Logic.Equiv.Finset
 
 /-! # GapCVP proof, part 01 -/
 

LeanPool/GapCVP/Part02.lean

@@ -6,7 +6,7 @@ Authors: OpenAI, Dean Cureton
 
 module
 
-public import LeanPool.GapCVP.Part01
+public import LeanPool.GapCVP.Part01B
 
 /-! # GapCVP proof, part 02 -/
 

LeanPool/GapCVP/Part03.lean

@@ -4,8 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: OpenAI, Dean Cureton
 -/
 
-module
+module -- shake: keep-all
 
 public import LeanPool.GapCVP.Part03G
+public import LeanPool.GapCVP.Part01 -- shake: keep
 
 /-! # GapCVP proof, part 03 -/

LeanPool/GapCVP/Part04.lean

@@ -4,8 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: OpenAI, Dean Cureton
 -/
 
-module
+module -- shake: keep-all
 
 public import LeanPool.GapCVP.Part04G
+public import LeanPool.GapCVP.Part03 -- shake: keep
 
 /-! # GapCVP proof, part 04 -/

LeanPool/GapCVP/Part04A.lean

@@ -6,7 +6,7 @@ Authors: OpenAI, Dean Cureton
 
 module
 
-public import LeanPool.GapCVP.Part03
+public import LeanPool.GapCVP.Part03E
 
 /-! # GapCVP proof, part 04 -/
 

LeanPool/GapCVP/Part04B.lean

@@ -7,6 +7,7 @@ Authors: OpenAI, Dean Cureton
 module
 
 public import LeanPool.GapCVP.Part04A
+public import LeanPool.GapCVP.Part03G
 
 /-! # GapCVP proof, part 04, continuation 02 -/
 

LeanPool/GapCVP/Part05.lean

@@ -4,8 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: OpenAI, Dean Cureton
 -/
 
-module
+module -- shake: keep-all
 
 public import LeanPool.GapCVP.Part05F
+public import LeanPool.GapCVP.Part04 -- shake: keep
+public import LeanPool.GapCVP.Part05B -- shake: keep
 
 /-! # GapCVP proof, part 05 -/

LeanPool/GapCVP/Part05A.lean

@@ -6,7 +6,7 @@ Authors: OpenAI, Dean Cureton
 
 module
 
-public import LeanPool.GapCVP.Part04
+public import LeanPool.GapCVP.Part04G
 
 /-! # GapCVP proof, part 05 -/
 

LeanPool/GapCVP/Part05C.lean

@@ -6,7 +6,8 @@ Authors: OpenAI, Dean Cureton
 
 module
 
-public import LeanPool.GapCVP.Part05B
+public import LeanPool.GapCVP.Part04D
+import LeanPool.GapCVP.Part05B
 
 /-! # GapCVP proof, part 05, continuation 03 -/
 

LeanPool/GapCVP/Part05D.lean

@@ -7,6 +7,7 @@ Authors: OpenAI, Dean Cureton
 module
 
 public import LeanPool.GapCVP.Part05C
+import LeanPool.GapCVP.Part04F
 
 /-! # GapCVP proof, part 05, continuation 04 -/
 

LeanPool/GapCVP/Part05E.lean

@@ -7,6 +7,7 @@ Authors: OpenAI, Dean Cureton
 module
 
 public import LeanPool.GapCVP.Part05D
+public import LeanPool.GapCVP.Part04F
 
 /-! # GapCVP proof, part 05, continuation 05 -/
 

LeanPool/GapCVP/Part05F.lean

@@ -7,6 +7,8 @@ Authors: OpenAI, Dean Cureton
 module
 
 public import LeanPool.GapCVP.Part05E
+public import LeanPool.GapCVP.Part05A
+import LeanPool.GapCVP.Part05B
 
 /-! # GapCVP proof, part 05, continuation 06 -/
 

LeanPool/GapCVP/Part06.lean

@@ -4,8 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: OpenAI, Dean Cureton
 -/
 
-module
+module -- shake: keep-all
 
 public import LeanPool.GapCVP.Part06D
+public import LeanPool.GapCVP.Part05 -- shake: keep
+public import LeanPool.GapCVP.Part06C -- shake: keep
 
 /-! # GapCVP proof, part 06 -/

LeanPool/GapCVP/Part06A.lean

@@ -6,7 +6,7 @@ Authors: OpenAI, Dean Cureton
 
 module
 
-public import LeanPool.GapCVP.Part05
+public import LeanPool.GapCVP.Part05F
 
 /-! # GapCVP proof, part 06 -/
 

LeanPool/GapCVP/Part06D.lean

@@ -6,7 +6,8 @@ Authors: OpenAI, Dean Cureton
 
 module
 
-public import LeanPool.GapCVP.Part06C
+public import LeanPool.GapCVP.Part06B
+import LeanPool.GapCVP.Part06C
 
 /-! # GapCVP proof, part 06, continuation 04 -/
 

LeanPool/GapCVP/Part07.lean

@@ -4,8 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: OpenAI, Dean Cureton
 -/
 
-module
+module -- shake: keep-all
 
 public import LeanPool.GapCVP.Part07G
+public import LeanPool.GapCVP.Part06 -- shake: keep
 
 /-! # GapCVP proof, part 07 -/

LeanPool/GapCVP/Part07A.lean

@@ -6,7 +6,7 @@ Authors: OpenAI, Dean Cureton
 
 module
 
-public import LeanPool.GapCVP.Part06
+public import LeanPool.GapCVP.Part06D
 
 /-! # GapCVP proof, part 07 -/
 

LeanPool/GapCVP/Part07B.lean

@@ -6,7 +6,8 @@ Authors: OpenAI, Dean Cureton
 
 module
 
-public import LeanPool.GapCVP.Part07A
+public import LeanPool.GapCVP.Part06D
+import LeanPool.GapCVP.Part07A
 
 /-! # GapCVP proof, part 07, continuation 02 -/
 

LeanPool/GapCVP/Part07C.lean

@@ -6,7 +6,8 @@ Authors: OpenAI, Dean Cureton
 
 module
 
-public import LeanPool.GapCVP.Part07B
+public import LeanPool.GapCVP.Part06D -- shake: keep
+import LeanPool.GapCVP.Part05B
 
 /-! # GapCVP proof, part 07, continuation 03 -/
 

LeanPool/GapCVP/Part07D.lean

@@ -7,6 +7,8 @@ Authors: OpenAI, Dean Cureton
 module
 
 public import LeanPool.GapCVP.Part07C
+public import LeanPool.GapCVP.Part07B
+public import LeanPool.GapCVP.Part07A
 
 /-! # GapCVP proof, part 07, continuation 04 -/
 

LeanPool/GapCVP/Part07F.lean

@@ -6,7 +6,7 @@ Authors: OpenAI, Dean Cureton
 
 module
 
-public import LeanPool.GapCVP.Part07E
+public import LeanPool.GapCVP.Part06D -- shake: keep
 
 /-! # GapCVP proof, part 07, continuation 06 -/
 
@@ -24,20 +24,6 @@ open GapCVP.TraceGolf (oneStep rebound)
 
 namespace CNFFiveFamilyForbiddenWholeClauseExactSourceTM
 
-open Computability Turing GapCVP.BinaryEncoding GapCVP.SourceUniformTuringTM
-
-open GapCVP.CLStructuralPrefixWriter GapCVP.CNFFlatSourceGridDescriptorTM
-
-open GapCVP.CNFFlatPhysicalBinaryAppendTM
-
-open GapCVP.SourceFourFamilyInterpolationMembershipPredicateTM
-
-open GapCVP.CNFFiveFamilyFlatCandidateGenerationTM
-
-open GapCVP.CNFFiveFamilyForbiddenWholeClauseWorkerTM
-
-open GapCVP.CNFFiveFamilyForbiddenWholeClauseSourceCert
-
 end CNFFiveFamilyForbiddenWholeClauseExactSourceTM
 
 namespace CNFFiveFamilyIndependentAnchoredFamilyStreamTM
@@ -311,9 +297,7 @@ open GapCVP.CNFFlatPhysicalBinaryAppendTM GapCVP.CNFFiveFamilyFlatCandidateGener
 open GapCVP.CNFFiveFamilyFlatIndexedCatalogueTM GapCVP.CNFFiveFamilyFlatIndexedRankArithmeticTM
 open GapCVP.CNFFiveFamilyFlatRowMajorCatalogueTM
 open GapCVP.CNFFiveFamilyFlatRowMajorAtLeastClauseWorkerTM
-open GapCVP.CNFFiveFamilyFlatRowMajorAtMostClauseWorkerTM
 open GapCVP.CNFFiveFamilyFlatAcceptanceClauseFoldTM
-open GapCVP.CNFFiveFamilyPackedInitialCellDecoderTM
 open GapCVP.CNFFiveFamilyForbiddenWholeClauseExactSourceTM
 open GapCVP.CNFFiveFamilyIndependentAnchoredFamilyStreamTM
 

LeanPool/GapCVP/Part07G.lean

@@ -7,6 +7,7 @@ Authors: OpenAI, Dean Cureton
 module
 
 public import LeanPool.GapCVP.Part07F
+public import LeanPool.GapCVP.Part07E
 
 /-! # GapCVP proof, part 07, continuation 07 -/
 

LeanPool/GapCVP/Part08.lean

@@ -4,8 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: OpenAI, Dean Cureton
 -/
 
-module
+module -- shake: keep-all
 
 public import LeanPool.GapCVP.Part08D
+public import LeanPool.GapCVP.Part07 -- shake: keep
+public import LeanPool.GapCVP.Part08B -- shake: keep
+public import Mathlib.Data.Nat.Bitwise -- shake: keep
+public import Mathlib.FieldTheory.PrimitiveElement -- shake: keep
+public import Mathlib.LinearAlgebra.Lagrange -- shake: keep
 
 /-! # GapCVP proof, part 08 -/

LeanPool/GapCVP/Part08A.lean

@@ -6,11 +6,9 @@ Authors: OpenAI, Dean Cureton
 
 module
 
-public import LeanPool.GapCVP.Part07
-public import Mathlib.FieldTheory.Finite.GaloisField
-public import Mathlib.FieldTheory.PrimitiveElement
-public import Mathlib.LinearAlgebra.Lagrange
-public import Mathlib.LinearAlgebra.Vandermonde
+public import LeanPool.GapCVP.Part07G
+import Mathlib.Combinatorics.Matroid.Init
+import Mathlib.Tactic.Positivity.Finset
 
 /-! # GapCVP proof, part 08 -/
 

LeanPool/GapCVP/Part08B.lean

@@ -6,7 +6,9 @@ Authors: OpenAI, Dean Cureton
 
 module
 
-public import LeanPool.GapCVP.Part08A
+public import LeanPool.GapCVP.Part07D -- shake: keep
+import Mathlib.Combinatorics.Matroid.Init
+import Mathlib.Tactic.Positivity.Finset
 
 /-! # GapCVP proof, part 08, continuation 02 -/
 
@@ -40,9 +42,7 @@ open GapCVP.CNFFiveFamilyPackedInitialCellDecoderTM
 
 open GapCVP.CNFFiveFamilyForbiddenWindowCoordinateTM
 
-open GapCVP.CNFFiveFamilyForbiddenWholeClauseValidity
 
-open GapCVP.CNFFiveFamilyIndependentFiveFamilyBundledCatalogueTM
 
 end CNFFiveFamilyIndependentFiveFamilyCatalogueSourceValidity
 

LeanPool/GapCVP/Part08C.lean

@@ -6,7 +6,10 @@ Authors: OpenAI, Dean Cureton
 
 module
 
-public import LeanPool.GapCVP.Part08B
+public import LeanPool.GapCVP.Part08A
+import LeanPool.GapCVP.Part08B
+import Mathlib.Combinatorics.Matroid.Init
+import Mathlib.Tactic.Positivity.Finset
 
 /-! # GapCVP proof, part 08, continuation 03 -/
 

LeanPool/GapCVP/Part08D.lean

@@ -7,7 +7,10 @@ Authors: OpenAI, Dean Cureton
 module
 
 public import LeanPool.GapCVP.Part08C
-public import Mathlib.Data.Nat.Bitwise
+public import Mathlib.FieldTheory.Finite.GaloisField
+public import Mathlib.LinearAlgebra.Vandermonde
+import Mathlib.Data.Nat.Bitwise
+import Mathlib.LinearAlgebra.Lagrange
 
 /-! # GapCVP proof, part 08, continuation 04 -/
 

LeanPool/GapCVP/Part09.lean

@@ -6,18 +6,21 @@ Authors: OpenAI, Dean Cureton
 
 module
 
-public import LeanPool.GapCVP.Part08
-public import Mathlib.Algebra.Order.Floor.Semifield
-public import Mathlib.Algebra.Order.Star.Int
-public import Mathlib.FieldTheory.RatFunc.AsPolynomial
-public import Mathlib.RingTheory.Flat.TorsionFree
-public import Mathlib.RingTheory.Henselian
-public import Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
-public import Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
-public import Mathlib.RingTheory.Polynomial.Resultant.Basic
-public import Mathlib.RingTheory.Polynomial.Vieta
-public import Mathlib.RingTheory.RegularLocalRing.Defs
 public import Mathlib.RingTheory.SimpleRing.Principal
+public import LeanPool.GapCVP.Part08D
+public import Mathlib.FieldTheory.RatFunc.Basic
+public import Mathlib.LinearAlgebra.Lagrange
+public import Mathlib.RingTheory.Valuation.Basic
+import Mathlib.Algebra.Order.Floor.Semifield
+import Mathlib.Algebra.Order.Star.Int
+import Mathlib.FieldTheory.RatFunc.AsPolynomial
+import Mathlib.RingTheory.Flat.TorsionFree
+import Mathlib.RingTheory.Henselian
+import Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
+import Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
+import Mathlib.RingTheory.Polynomial.Resultant.Basic
+import Mathlib.RingTheory.Polynomial.Vieta
+import Mathlib.RingTheory.RegularLocalRing.Defs
 
 /-! # GapCVP proof, part 09 -/