From f92f8500e421fc0d19fc54e250a7d9ad679a0408 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Wed, 4 Nov 2026 14:33:37 +0000 Subject: [PATCH 1/2] perf(GapCVP): narrow proof dependencies and row-count simplification --- LeanPool/GapCVP.lean | 13 ++++-- LeanPool/GapCVP/Part01.lean | 2 +- LeanPool/GapCVP/Part01A.lean | 2 +- LeanPool/GapCVP/Part02.lean | 2 +- LeanPool/GapCVP/Part03.lean | 3 +- LeanPool/GapCVP/Part04.lean | 3 +- LeanPool/GapCVP/Part04A.lean | 2 +- LeanPool/GapCVP/Part04B.lean | 1 + LeanPool/GapCVP/Part05.lean | 4 +- LeanPool/GapCVP/Part05A.lean | 2 +- LeanPool/GapCVP/Part05C.lean | 3 +- LeanPool/GapCVP/Part05D.lean | 1 + LeanPool/GapCVP/Part05E.lean | 1 + LeanPool/GapCVP/Part05F.lean | 2 + LeanPool/GapCVP/Part06.lean | 4 +- LeanPool/GapCVP/Part06A.lean | 2 +- LeanPool/GapCVP/Part06D.lean | 3 +- LeanPool/GapCVP/Part07.lean | 3 +- LeanPool/GapCVP/Part07A.lean | 2 +- LeanPool/GapCVP/Part07B.lean | 3 +- LeanPool/GapCVP/Part07C.lean | 3 +- LeanPool/GapCVP/Part07D.lean | 2 + LeanPool/GapCVP/Part07F.lean | 2 +- LeanPool/GapCVP/Part08.lean | 7 ++- LeanPool/GapCVP/Part08A.lean | 8 ++-- LeanPool/GapCVP/Part08B.lean | 4 +- LeanPool/GapCVP/Part08C.lean | 5 ++- LeanPool/GapCVP/Part08D.lean | 5 ++- LeanPool/GapCVP/Part09.lean | 25 ++++++----- LeanPool/GapCVP/Part10.lean | 13 +++++- LeanPool/GapCVP/Part10A.lean | 3 ++ LeanPool/GapCVP/Part10B.lean | 3 ++ LeanPool/GapCVP/Part11.lean | 5 ++- LeanPool/GapCVP/Part11A.lean | 6 +-- LeanPool/GapCVP/Part11B.lean | 5 ++- LeanPool/GapCVP/Part11C.lean | 8 +++- LeanPool/GapCVP/Part12.lean | 3 +- LeanPool/GapCVP/Part12A.lean | 4 +- LeanPool/GapCVP/Part12B.lean | 5 ++- LeanPool/GapCVP/Part12C.lean | 5 +++ LeanPool/GapCVP/Part12D.lean | 2 + LeanPool/GapCVP/Part13.lean | 47 ++++++++++++-------- LeanPool/GapCVP/Part14.lean | 3 +- LeanPool/GapCVP/Part14A.lean | 2 + LeanPool/GapCVP/Part14B.lean | 86 ++++++++++++++---------------------- LeanPool/GapCVP/Part15.lean | 5 ++- LeanPool/GapCVP/Part16.lean | 5 ++- LeanPool/GapCVP/Part16A.lean | 4 +- LeanPool/GapCVP/Part16B.lean | 5 ++- LeanPool/GapCVP/Part17.lean | 5 ++- LeanPool/GapCVP/Part18.lean | 5 ++- 51 files changed, 217 insertions(+), 131 deletions(-) diff --git a/LeanPool/GapCVP.lean b/LeanPool/GapCVP.lean index 76631afd1b..b40bd37ee1 100644 --- a/LeanPool/GapCVP.lean +++ b/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. -/ diff --git a/LeanPool/GapCVP/Part01.lean b/LeanPool/GapCVP/Part01.lean index 4834a0e7a7..0112186977 100644 --- a/LeanPool/GapCVP/Part01.lean +++ b/LeanPool/GapCVP/Part01.lean @@ -4,7 +4,7 @@ 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 diff --git a/LeanPool/GapCVP/Part01A.lean b/LeanPool/GapCVP/Part01A.lean index 14d0e7caa9..af2f53afc2 100644 --- a/LeanPool/GapCVP/Part01A.lean +++ b/LeanPool/GapCVP/Part01A.lean @@ -4,7 +4,7 @@ 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 diff --git a/LeanPool/GapCVP/Part02.lean b/LeanPool/GapCVP/Part02.lean index da6b6b69a4..cf488d75b1 100644 --- a/LeanPool/GapCVP/Part02.lean +++ b/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 -/ diff --git a/LeanPool/GapCVP/Part03.lean b/LeanPool/GapCVP/Part03.lean index 2ca71680be..9e9e65115a 100644 --- a/LeanPool/GapCVP/Part03.lean +++ b/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 -/ diff --git a/LeanPool/GapCVP/Part04.lean b/LeanPool/GapCVP/Part04.lean index 99ff7b3ece..3e89811089 100644 --- a/LeanPool/GapCVP/Part04.lean +++ b/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 -/ diff --git a/LeanPool/GapCVP/Part04A.lean b/LeanPool/GapCVP/Part04A.lean index ccf05ec7f7..43feebb1c2 100644 --- a/LeanPool/GapCVP/Part04A.lean +++ b/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 -/ diff --git a/LeanPool/GapCVP/Part04B.lean b/LeanPool/GapCVP/Part04B.lean index 594232b9a0..1e9103f74f 100644 --- a/LeanPool/GapCVP/Part04B.lean +++ b/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 -/ diff --git a/LeanPool/GapCVP/Part05.lean b/LeanPool/GapCVP/Part05.lean index 851bbc8686..a622c5185c 100644 --- a/LeanPool/GapCVP/Part05.lean +++ b/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 -/ diff --git a/LeanPool/GapCVP/Part05A.lean b/LeanPool/GapCVP/Part05A.lean index dd6eb25b46..3b2df62b2a 100644 --- a/LeanPool/GapCVP/Part05A.lean +++ b/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 -/ diff --git a/LeanPool/GapCVP/Part05C.lean b/LeanPool/GapCVP/Part05C.lean index 7a34f8fc55..c98f6f2552 100644 --- a/LeanPool/GapCVP/Part05C.lean +++ b/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 -/ diff --git a/LeanPool/GapCVP/Part05D.lean b/LeanPool/GapCVP/Part05D.lean index b31202c9b7..3d6d9b0954 100644 --- a/LeanPool/GapCVP/Part05D.lean +++ b/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 -/ diff --git a/LeanPool/GapCVP/Part05E.lean b/LeanPool/GapCVP/Part05E.lean index 26e0e12ad8..fac1519fcb 100644 --- a/LeanPool/GapCVP/Part05E.lean +++ b/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 -/ diff --git a/LeanPool/GapCVP/Part05F.lean b/LeanPool/GapCVP/Part05F.lean index 09dfcdbb96..425ad6b23a 100644 --- a/LeanPool/GapCVP/Part05F.lean +++ b/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 -/ diff --git a/LeanPool/GapCVP/Part06.lean b/LeanPool/GapCVP/Part06.lean index 7b2d227260..bee50284a1 100644 --- a/LeanPool/GapCVP/Part06.lean +++ b/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 -/ diff --git a/LeanPool/GapCVP/Part06A.lean b/LeanPool/GapCVP/Part06A.lean index 98a879b70c..544cfd3c0b 100644 --- a/LeanPool/GapCVP/Part06A.lean +++ b/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 -/ diff --git a/LeanPool/GapCVP/Part06D.lean b/LeanPool/GapCVP/Part06D.lean index d54659c339..49720f1e39 100644 --- a/LeanPool/GapCVP/Part06D.lean +++ b/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 -/ diff --git a/LeanPool/GapCVP/Part07.lean b/LeanPool/GapCVP/Part07.lean index d366aa1549..fe535d5448 100644 --- a/LeanPool/GapCVP/Part07.lean +++ b/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 -/ diff --git a/LeanPool/GapCVP/Part07A.lean b/LeanPool/GapCVP/Part07A.lean index 3b934b4a62..109dde6b15 100644 --- a/LeanPool/GapCVP/Part07A.lean +++ b/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 -/ diff --git a/LeanPool/GapCVP/Part07B.lean b/LeanPool/GapCVP/Part07B.lean index 6a0bebf2dd..8272c83898 100644 --- a/LeanPool/GapCVP/Part07B.lean +++ b/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 -/ diff --git a/LeanPool/GapCVP/Part07C.lean b/LeanPool/GapCVP/Part07C.lean index e33f64e04d..efb9c40f06 100644 --- a/LeanPool/GapCVP/Part07C.lean +++ b/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 -/ diff --git a/LeanPool/GapCVP/Part07D.lean b/LeanPool/GapCVP/Part07D.lean index 5a67b21163..80128c77fe 100644 --- a/LeanPool/GapCVP/Part07D.lean +++ b/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 -/ diff --git a/LeanPool/GapCVP/Part07F.lean b/LeanPool/GapCVP/Part07F.lean index b08381b5a7..f9d4c7e8a2 100644 --- a/LeanPool/GapCVP/Part07F.lean +++ b/LeanPool/GapCVP/Part07F.lean @@ -6,7 +6,7 @@ Authors: OpenAI, Dean Cureton module -public import LeanPool.GapCVP.Part07E +public import LeanPool.GapCVP.Part07E -- shake: keep /-! # GapCVP proof, part 07, continuation 06 -/ diff --git a/LeanPool/GapCVP/Part08.lean b/LeanPool/GapCVP/Part08.lean index 6ee9397194..298f638c7b 100644 --- a/LeanPool/GapCVP/Part08.lean +++ b/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 -/ diff --git a/LeanPool/GapCVP/Part08A.lean b/LeanPool/GapCVP/Part08A.lean index bc48a6d728..c290f3bfbf 100644 --- a/LeanPool/GapCVP/Part08A.lean +++ b/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 -/ diff --git a/LeanPool/GapCVP/Part08B.lean b/LeanPool/GapCVP/Part08B.lean index 9da824358b..76e893a800 100644 --- a/LeanPool/GapCVP/Part08B.lean +++ b/LeanPool/GapCVP/Part08B.lean @@ -6,7 +6,9 @@ Authors: OpenAI, Dean Cureton module -public import LeanPool.GapCVP.Part08A +public import LeanPool.GapCVP.Part08A -- shake: keep +import Mathlib.Combinatorics.Matroid.Init +import Mathlib.Tactic.Positivity.Finset /-! # GapCVP proof, part 08, continuation 02 -/ diff --git a/LeanPool/GapCVP/Part08C.lean b/LeanPool/GapCVP/Part08C.lean index c83e2201f2..07d44305dc 100644 --- a/LeanPool/GapCVP/Part08C.lean +++ b/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 -/ diff --git a/LeanPool/GapCVP/Part08D.lean b/LeanPool/GapCVP/Part08D.lean index 1d1e39d994..0d6da721f9 100644 --- a/LeanPool/GapCVP/Part08D.lean +++ b/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 -/ diff --git a/LeanPool/GapCVP/Part09.lean b/LeanPool/GapCVP/Part09.lean index 7e0817f0f9..94abbe062e 100644 --- a/LeanPool/GapCVP/Part09.lean +++ b/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 -/ diff --git a/LeanPool/GapCVP/Part10.lean b/LeanPool/GapCVP/Part10.lean index 08af6ecb86..4645e2fe68 100644 --- a/LeanPool/GapCVP/Part10.lean +++ b/LeanPool/GapCVP/Part10.lean @@ -4,8 +4,19 @@ 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.Part10B +public import LeanPool.GapCVP.Part08 -- shake: keep +public import Mathlib.Algebra.Order.Floor.Semifield -- shake: keep +public import Mathlib.Algebra.Order.Star.Int -- shake: keep +public import Mathlib.FieldTheory.RatFunc.AsPolynomial -- shake: keep +public import Mathlib.RingTheory.Flat.TorsionFree -- shake: keep +public import Mathlib.RingTheory.Henselian -- shake: keep +public import Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem -- shake: keep +public import Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities -- shake: keep +public import Mathlib.RingTheory.Polynomial.Resultant.Basic -- shake: keep +public import Mathlib.RingTheory.Polynomial.Vieta -- shake: keep +public import Mathlib.RingTheory.RegularLocalRing.Defs -- shake: keep /-! # GapCVP proof, part 10 -/ diff --git a/LeanPool/GapCVP/Part10A.lean b/LeanPool/GapCVP/Part10A.lean index 127b251428..00bbf9df72 100644 --- a/LeanPool/GapCVP/Part10A.lean +++ b/LeanPool/GapCVP/Part10A.lean @@ -7,6 +7,9 @@ Authors: OpenAI, Dean Cureton module public import LeanPool.GapCVP.Part09 +import Mathlib.Algebra.Order.Floor.Semifield +import Mathlib.RingTheory.Henselian +import Mathlib.RingTheory.RegularLocalRing.Defs /-! # GapCVP proof, part 10 -/ diff --git a/LeanPool/GapCVP/Part10B.lean b/LeanPool/GapCVP/Part10B.lean index 66a996a5f5..6f531a5b88 100644 --- a/LeanPool/GapCVP/Part10B.lean +++ b/LeanPool/GapCVP/Part10B.lean @@ -7,6 +7,9 @@ Authors: OpenAI, Dean Cureton module public import LeanPool.GapCVP.Part10A +import LeanPool.GapCVP.Part05B +import Mathlib.Algebra.Order.Floor.Semifield +import Mathlib.CategoryTheory.Category.Init /-! # GapCVP proof, part 10, continuation 02 -/ diff --git a/LeanPool/GapCVP/Part11.lean b/LeanPool/GapCVP/Part11.lean index 151521b8f3..a5477fb4ab 100644 --- a/LeanPool/GapCVP/Part11.lean +++ b/LeanPool/GapCVP/Part11.lean @@ -4,8 +4,11 @@ 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.Part11C +public import LeanPool.GapCVP.Part10 -- shake: keep +public import LeanPool.GapCVP.Part11B -- shake: keep +public import Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas -- shake: keep /-! # GapCVP proof, part 11 -/ diff --git a/LeanPool/GapCVP/Part11A.lean b/LeanPool/GapCVP/Part11A.lean index a6b254a348..d50a069e69 100644 --- a/LeanPool/GapCVP/Part11A.lean +++ b/LeanPool/GapCVP/Part11A.lean @@ -6,9 +6,9 @@ Authors: OpenAI, Dean Cureton module -public import LeanPool.GapCVP.Part10 -public import Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas -public import Mathlib.InformationTheory.Hamming +public import LeanPool.GapCVP.Part10B +import Mathlib.Algebra.Order.Floor.Semifield +import Mathlib.CategoryTheory.Category.Init /-! # GapCVP proof, part 11 -/ diff --git a/LeanPool/GapCVP/Part11B.lean b/LeanPool/GapCVP/Part11B.lean index 25115181eb..e1d0bf959b 100644 --- a/LeanPool/GapCVP/Part11B.lean +++ b/LeanPool/GapCVP/Part11B.lean @@ -6,7 +6,10 @@ Authors: OpenAI, Dean Cureton module -public import LeanPool.GapCVP.Part11A +public import LeanPool.GapCVP.Part10B +import Mathlib.Algebra.Order.Floor.Semifield +import Mathlib.Algebra.Order.Star.Int +import Mathlib.CategoryTheory.Category.Init /-! # GapCVP proof, part 11, continuation 02 -/ diff --git a/LeanPool/GapCVP/Part11C.lean b/LeanPool/GapCVP/Part11C.lean index 9ed21d3f68..7e46d33ceb 100644 --- a/LeanPool/GapCVP/Part11C.lean +++ b/LeanPool/GapCVP/Part11C.lean @@ -6,7 +6,13 @@ Authors: OpenAI, Dean Cureton module -public import LeanPool.GapCVP.Part11B +public import LeanPool.GapCVP.Part11A +public import Mathlib.InformationTheory.Hamming +public import Mathlib.Data.Nat.NthRoot.Defs +public import LeanPool.GapCVP.Part11B -- shake: keep +import Mathlib.Algebra.Order.Floor.Semifield +import Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas +import Mathlib.CategoryTheory.Category.Init /-! # GapCVP proof, part 11, continuation 03 -/ diff --git a/LeanPool/GapCVP/Part12.lean b/LeanPool/GapCVP/Part12.lean index 4a20a8ad21..084c8287a4 100644 --- a/LeanPool/GapCVP/Part12.lean +++ b/LeanPool/GapCVP/Part12.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.Part12D +public import LeanPool.GapCVP.Part11 -- shake: keep /-! # GapCVP proof, part 12 -/ diff --git a/LeanPool/GapCVP/Part12A.lean b/LeanPool/GapCVP/Part12A.lean index 3799d20fd5..699e965c20 100644 --- a/LeanPool/GapCVP/Part12A.lean +++ b/LeanPool/GapCVP/Part12A.lean @@ -6,7 +6,9 @@ Authors: OpenAI, Dean Cureton module -public import LeanPool.GapCVP.Part11 +public import LeanPool.GapCVP.Part11C +import Mathlib.Algebra.Order.Floor.Semifield +import Mathlib.CategoryTheory.Category.Init /-! # GapCVP proof, part 12 -/ diff --git a/LeanPool/GapCVP/Part12B.lean b/LeanPool/GapCVP/Part12B.lean index bbeebaa3e8..b9bfab2788 100644 --- a/LeanPool/GapCVP/Part12B.lean +++ b/LeanPool/GapCVP/Part12B.lean @@ -6,7 +6,10 @@ Authors: OpenAI, Dean Cureton module -public import LeanPool.GapCVP.Part12A +public import LeanPool.GapCVP.Part11C +import Mathlib.Algebra.Order.Floor.Semifield +import Mathlib.Algebra.Order.Star.Int +import Mathlib.CategoryTheory.Category.Init /-! # GapCVP proof, part 12, continuation 02 -/ diff --git a/LeanPool/GapCVP/Part12C.lean b/LeanPool/GapCVP/Part12C.lean index 927d9fde4b..12eb753202 100644 --- a/LeanPool/GapCVP/Part12C.lean +++ b/LeanPool/GapCVP/Part12C.lean @@ -7,6 +7,11 @@ Authors: OpenAI, Dean Cureton module public import LeanPool.GapCVP.Part12B +public import LeanPool.GapCVP.Part12A +import LeanPool.GapCVP.Part11B +import Mathlib.Algebra.Order.Floor.Semifield +import Mathlib.Algebra.Order.Star.Int +import Mathlib.CategoryTheory.Category.Init /-! # GapCVP proof, part 12, continuation 03 -/ diff --git a/LeanPool/GapCVP/Part12D.lean b/LeanPool/GapCVP/Part12D.lean index c7b6e2671f..7944260f10 100644 --- a/LeanPool/GapCVP/Part12D.lean +++ b/LeanPool/GapCVP/Part12D.lean @@ -7,6 +7,8 @@ Authors: OpenAI, Dean Cureton module public import LeanPool.GapCVP.Part12C +import Mathlib.Algebra.Order.Floor.Semifield +import Mathlib.CategoryTheory.Category.Init /-! # GapCVP proof, part 12, continuation 04 -/ diff --git a/LeanPool/GapCVP/Part13.lean b/LeanPool/GapCVP/Part13.lean index 6331d0a17a..facd8f3164 100644 --- a/LeanPool/GapCVP/Part13.lean +++ b/LeanPool/GapCVP/Part13.lean @@ -6,7 +6,13 @@ Authors: OpenAI, Dean Cureton module -public import LeanPool.GapCVP.Part12 +public import LeanPool.GapCVP.Part11B +public import LeanPool.GapCVP.Part12C +import LeanPool.GapCVP.Part12D +import Mathlib.Algebra.Order.Floor.Semifield +import Mathlib.Algebra.Order.Star.Int +import Mathlib.CategoryTheory.Category.Init +import Mathlib.Data.Nat.Bitwise /-! # GapCVP proof, part 13 -/ @@ -5603,8 +5609,7 @@ theorem paperVariableArityExplicitBinaryRowWordCount_eq_fourFamily gridCount = physGridCard formula := by change Fintype.card (ExplicitGridPoint length source) = _ - simpa [length, source, - paperVariableAritySourceFormula_variableCount] using + simpa only [Fintype.card_coe, paperVariableAritySourceFormula_variableCount] using sourceFormulaGrid_card_eq_fieldWordCount length source have field_valid : fieldCount = @@ -5612,8 +5617,7 @@ theorem paperVariableArityExplicitBinaryRowWordCount_eq_fourFamily change Fintype.card (GapCVP.Factor400BinaryConstructiveSourcePlaces.sourceFormulaField length source) = _ - simpa [length, source] using - GapCVP.Core.sourceFiniteField_card + exact GapCVP.Core.sourceFiniteField_card (GapCVP.Core.sourceSizeParameter_ge_one_hundred length source) have shifted_valid : Fintype.card @@ -5633,7 +5637,7 @@ theorem paperVariableArityExplicitBinaryRowWordCount_eq_fourFamily Fin (explicitMomentBudget length source + 1)) = paperShiftedFamilyTagCount formula (explicitMomentBudget length source) := by - simpa [source] using + simpa only [Fintype.card_fin] using (Fintype.card_congr (paperShiftedFamilyWordOrder formula (explicitMomentBudget length source))).symm @@ -5675,9 +5679,10 @@ theorem paperVariableArityExplicitBinaryRowWordCount_eq_fourFamily Finset.sum_const, Finset.card_univ, nsmul_eq_mul, Fintype.card_fin] rw [shifted_valid, table_valid] - simp [source, - gridCount, fieldCount, degree, momentCount, - explicitMomentBudget] + simp only [source, Fintype.card_coe, Fintype.card_unique, Nat.cast_id, + List.length_map, List.length_attach, + GapCVP.SourcePreprocessingSemantics.paperSourceNormalizedClauses, + gridCount, fieldCount, degree, momentCount, explicitMomentBudget] ring _ = paperVariableArityPhysicalFormulaRowCount formula := by rw [grid_valid, field_valid] @@ -6541,23 +6546,27 @@ theorem physicalWordBinaryCheckCoefficient encodingLength formula row).2.1 column) (physicalWordDecodedRow encodingLength formula row).2.2 := by - rw [paperVariableArityPhysicalWordBinarySystem_check_apply] - change - binaryFieldParityMatrix + refine (paperVariableArityPhysicalWordBinarySystem_check_apply + encodingLength formula row column).trans ?_ + refine (binaryFieldParityMatrix_apply_basisCoordinate (GapCVP.Factor400BinaryConstructiveSourcePlaces.sourceFormulaFieldBasis encodingLength (srcFormula formula)) (sourceFormulaPhysicalFamilyFieldMatrix encodingLength (srcFormula formula) (physicalWordDecodedRow encodingLength formula row).1) - ((physicalWordDecodedRow - encodingLength formula row).2.1, - (physicalWordDecodedRow - encodingLength formula row).2.2) + (physicalWordDecodedRow encodingLength formula row).2.1 + (physicalWordDecodedRow encodingLength formula row).2.2 (physicalColumnPermutation - encodingLength formula column) = _ - rw [binaryFieldParityMatrix_apply_basisCoordinate] - rw [← paperVariableArityPhysicalWordFamilyFieldCoefficient_eq_matrix] + encodingLength formula column)).trans ?_ + exact congrArg + (fun value => + (GapCVP.Factor400BinaryConstructiveSourcePlaces.sourceFormulaFieldBasis + encodingLength (srcFormula formula)).equivFun value + (physicalWordDecodedRow encodingLength formula row).2.2) + (paperVariableArityPhysicalWordFamilyFieldCoefficient_eq_matrix + encodingLength formula (physicalWordDecodedRow encodingLength formula row).1 + (physicalWordDecodedRow encodingLength formula row).2.1 column).symm private theorem paperVariableArityPhysicalWordBinaryRightHandSideCoefficient (encodingLength : ℕ) (formula : ThreeCNF) diff --git a/LeanPool/GapCVP/Part14.lean b/LeanPool/GapCVP/Part14.lean index 158452816c..ec3def8741 100644 --- a/LeanPool/GapCVP/Part14.lean +++ b/LeanPool/GapCVP/Part14.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.Part14B +public import LeanPool.GapCVP.Part12 -- shake: keep /-! # GapCVP proof, part 14 -/ diff --git a/LeanPool/GapCVP/Part14A.lean b/LeanPool/GapCVP/Part14A.lean index 63ddda78c3..1b1de2110d 100644 --- a/LeanPool/GapCVP/Part14A.lean +++ b/LeanPool/GapCVP/Part14A.lean @@ -7,6 +7,8 @@ Authors: OpenAI, Dean Cureton module public import LeanPool.GapCVP.Part13 +import Mathlib.Algebra.Order.Floor.Semifield +import Mathlib.CategoryTheory.Category.Init /-! # GapCVP proof, part 14 -/ diff --git a/LeanPool/GapCVP/Part14B.lean b/LeanPool/GapCVP/Part14B.lean index 7131f6badf..fa8f17a7f8 100644 --- a/LeanPool/GapCVP/Part14B.lean +++ b/LeanPool/GapCVP/Part14B.lean @@ -7,6 +7,9 @@ Authors: OpenAI, Dean Cureton module public import LeanPool.GapCVP.Part14A +import Mathlib.Algebra.Order.Floor.Semifield +import Mathlib.RingTheory.Henselian +import Mathlib.RingTheory.RegularLocalRing.Defs /-! # GapCVP proof, part 14, continuation 02 -/ @@ -1404,6 +1407,28 @@ private theorem paperVariableArityPhysicalMatrixFamilyGuardCover afterRefinement, ordinary, afterOrdinary, decide_true, Bool.and_self, Bool.or_true] +private theorem physicalMatrixGuardedFourFamilyCheck_bits + (global refinement ordinary shifted : List Bool → List Bool) + (query : List Bool) (row globalBoundary refinementBoundary ordinaryBoundary : ℕ) + (entry : Bool) + (correctGlobal : global query = [decide (row < globalBoundary) && entry]) + (correctRefinement : refinement query = + [decide (globalBoundary ≤ row ∧ row < refinementBoundary) && entry]) + (correctOrdinary : ordinary query = + [decide (refinementBoundary ≤ row ∧ row < ordinaryBoundary) && entry]) + (correctShifted : shifted query = [decide (ordinaryBoundary ≤ row) && entry]) : + physicalMatrixGuardedFourFamilyCheck global refinement ordinary shifted query = [entry] := by + have last := fourFamilyBooleanOrOutput_bits ordinary shifted query _ _ + correctOrdinary correctShifted + have middle := fourFamilyBooleanOrOutput_bits refinement + (sourceFourFamilyBooleanOrOutput ordinary shifted) query _ _ correctRefinement last + have complete := fourFamilyBooleanOrOutput_bits global + (sourceFourFamilyBooleanOrOutput refinement + (sourceFourFamilyBooleanOrOutput ordinary shifted)) query _ _ correctGlobal middle + exact complete.trans (congrArg (fun bit => [bit]) + (paperVariableArityPhysicalMatrixFamilyGuardCover + row globalBoundary refinementBoundary ordinaryBoundary entry)) + theorem paperVariableArityPhysicalMatrixGuardedFourFamilyCheck_valid (global refinement ordinary shifted : List Bool → List Bool) (formula : ThreeCNF) @@ -1462,63 +1487,16 @@ theorem paperVariableArityPhysicalMatrixGuardedFourFamilyCheck_valid ((physicalWordBinarySystem (encodeThreeCNF formula).length formula).check row column = (1 : ZMod 2))] := by - let query := affineCellQuery row.val column.val - (encodeThreeCNF formula) - let entry := decide - ((physicalWordBinarySystem - (encodeThreeCNF formula).length formula).check - row column = (1 : ZMod 2)) - let globalBit := - decide (row.val < physicalFormulaGlobalBoundary formula) - let refinementBit := decide - (physicalFormulaGlobalBoundary formula ≤ row.val ∧ - row.val < physicalFormulaRefinementBoundary formula) - let ordinaryBit := decide - (physicalFormulaRefinementBoundary formula ≤ row.val ∧ - row.val < physicalFormulaOrdinaryBoundary formula) - let shiftedBit := decide - (physicalFormulaOrdinaryBoundary formula ≤ row.val) - have globalValue : global query = [globalBit && entry] := by - simpa only [query, globalBit, entry] using correctGlobal - have refinementValue : refinement query = [refinementBit && entry] := by - simpa only [query, refinementBit, entry] using correctRefinement - have ordinaryValue : ordinary query = [ordinaryBit && entry] := by - simpa only [query, ordinaryBit, entry] using correctOrdinary - have shiftedValue : shifted query = [shiftedBit && entry] := by - simpa only [query, shiftedBit, entry] using correctShifted - have last := fourFamilyBooleanOrOutput_bits - ordinary shifted query - (ordinaryBit && entry) (shiftedBit && entry) - ordinaryValue shiftedValue - have middle := fourFamilyBooleanOrOutput_bits - refinement (sourceFourFamilyBooleanOrOutput ordinary shifted) query - (refinementBit && entry) - ((ordinaryBit && entry) || (shiftedBit && entry)) - refinementValue last - have complete := fourFamilyBooleanOrOutput_bits - global - (sourceFourFamilyBooleanOrOutput refinement - (sourceFourFamilyBooleanOrOutput ordinary shifted)) query - (globalBit && entry) - ((refinementBit && entry) || - ((ordinaryBit && entry) || (shiftedBit && entry))) - globalValue middle - have covered := paperVariableArityPhysicalMatrixFamilyGuardCover - row.val + exact physicalMatrixGuardedFourFamilyCheck_bits global refinement ordinary shifted + (affineCellQuery row.val column.val (encodeThreeCNF formula)) row.val (physicalFormulaGlobalBoundary formula) (physicalFormulaRefinementBoundary formula) (physicalFormulaOrdinaryBoundary formula) - entry - change - physicalMatrixGuardedFourFamilyCheck - global refinement ordinary shifted query = [entry] - change - sourceFourFamilyBooleanOrOutput global - (sourceFourFamilyBooleanOrOutput refinement - (sourceFourFamilyBooleanOrOutput ordinary shifted)) query = - [entry] - rw [← covered] - exact complete + (decide + ((physicalWordBinarySystem + (encodeThreeCNF formula).length formula).check + row column = (1 : ZMod 2))) + correctGlobal correctRefinement correctOrdinary correctShifted private theorem paperVariableArityPhysicalMatrixCheckEntry_transport (source target : GapCVP.Core.BinaryAffineSystem) diff --git a/LeanPool/GapCVP/Part15.lean b/LeanPool/GapCVP/Part15.lean index c8b9eb5021..0e9ef8a9e5 100644 --- a/LeanPool/GapCVP/Part15.lean +++ b/LeanPool/GapCVP/Part15.lean @@ -6,7 +6,10 @@ Authors: OpenAI, Dean Cureton module -public import LeanPool.GapCVP.Part14 +public import LeanPool.GapCVP.Part14B +import Mathlib.Algebra.Order.Floor.Semifield +import Mathlib.RingTheory.Henselian +import Mathlib.RingTheory.RegularLocalRing.Defs /-! # GapCVP proof, part 15 -/ diff --git a/LeanPool/GapCVP/Part16.lean b/LeanPool/GapCVP/Part16.lean index d7ca255a0e..8828ec9d66 100644 --- a/LeanPool/GapCVP/Part16.lean +++ b/LeanPool/GapCVP/Part16.lean @@ -4,8 +4,11 @@ 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.Part16B +public import LeanPool.GapCVP.Part14 -- shake: keep +public import LeanPool.GapCVP.Part16A -- shake: keep +public import Mathlib.Data.List.Intervals -- shake: keep /-! # GapCVP proof, part 16 -/ diff --git a/LeanPool/GapCVP/Part16A.lean b/LeanPool/GapCVP/Part16A.lean index 2b9bc7f15d..751cf3aeb5 100644 --- a/LeanPool/GapCVP/Part16A.lean +++ b/LeanPool/GapCVP/Part16A.lean @@ -7,7 +7,9 @@ Authors: OpenAI, Dean Cureton module public import LeanPool.GapCVP.Part15 -public import Mathlib.Data.List.Intervals +import Mathlib.Algebra.Order.Floor.Semifield +import Mathlib.CategoryTheory.Category.Init +import Mathlib.Data.List.Intervals /-! # GapCVP proof, part 16 -/ diff --git a/LeanPool/GapCVP/Part16B.lean b/LeanPool/GapCVP/Part16B.lean index 8271a3a37c..90db31a1db 100644 --- a/LeanPool/GapCVP/Part16B.lean +++ b/LeanPool/GapCVP/Part16B.lean @@ -6,7 +6,10 @@ Authors: OpenAI, Dean Cureton module -public import LeanPool.GapCVP.Part16A +public import LeanPool.GapCVP.Part13 +import LeanPool.GapCVP.Part16A +import Mathlib.Algebra.Order.Floor.Semifield +import Mathlib.CategoryTheory.Category.Init /-! # GapCVP proof, part 16, continuation 02 -/ diff --git a/LeanPool/GapCVP/Part17.lean b/LeanPool/GapCVP/Part17.lean index 7c0f58d76c..f08f58daa4 100644 --- a/LeanPool/GapCVP/Part17.lean +++ b/LeanPool/GapCVP/Part17.lean @@ -6,7 +6,10 @@ Authors: OpenAI, Dean Cureton module -public import LeanPool.GapCVP.Part16 +public import LeanPool.GapCVP.Part16B +import Mathlib.Algebra.Order.Floor.Semifield +import Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas +import Mathlib.CategoryTheory.Category.Init /-! # GapCVP proof, part 17 -/ diff --git a/LeanPool/GapCVP/Part18.lean b/LeanPool/GapCVP/Part18.lean index cd8aa63ad4..4245a9d724 100644 --- a/LeanPool/GapCVP/Part18.lean +++ b/LeanPool/GapCVP/Part18.lean @@ -6,7 +6,10 @@ Authors: OpenAI, Dean Cureton module -public import LeanPool.GapCVP.Part17 +public import LeanPool.GapCVP.Part01A +import LeanPool.GapCVP.Part17 +import Mathlib.Algebra.Order.Floor.Semifield +import Mathlib.CategoryTheory.Category.Init /-! # GapCVP proof, part 18 -/ From 9f2cbbe9c099f4a16ebe5cc79842ee2e360da0d3 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Wed, 4 Nov 2026 15:07:59 +0000 Subject: [PATCH 2/2] perf(GapCVP): detach unused scopes and private lattice imports --- LeanPool/GapCVP/Part01.lean | 1 + LeanPool/GapCVP/Part01A.lean | 4 +++- LeanPool/GapCVP/Part07F.lean | 18 +----------------- LeanPool/GapCVP/Part07G.lean | 1 + LeanPool/GapCVP/Part08B.lean | 4 +--- LeanPool/GapCVP/Part12C.lean | 1 - LeanPool/GapCVP/Part13.lean | 1 - 7 files changed, 7 insertions(+), 23 deletions(-) diff --git a/LeanPool/GapCVP/Part01.lean b/LeanPool/GapCVP/Part01.lean index 0112186977..34565b64ea 100644 --- a/LeanPool/GapCVP/Part01.lean +++ b/LeanPool/GapCVP/Part01.lean @@ -7,5 +7,6 @@ Authors: OpenAI, Dean Cureton module -- shake: keep-all public import LeanPool.GapCVP.Part01B +public import Mathlib.Algebra.Module.ZLattice.Basic -- shake: keep /-! # GapCVP proof, part 01 -/ diff --git a/LeanPool/GapCVP/Part01A.lean b/LeanPool/GapCVP/Part01A.lean index af2f53afc2..61f6c5d95a 100644 --- a/LeanPool/GapCVP/Part01A.lean +++ b/LeanPool/GapCVP/Part01A.lean @@ -7,11 +7,13 @@ Authors: OpenAI, Dean Cureton 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 -/ diff --git a/LeanPool/GapCVP/Part07F.lean b/LeanPool/GapCVP/Part07F.lean index f9d4c7e8a2..2e5a2cdb3e 100644 --- a/LeanPool/GapCVP/Part07F.lean +++ b/LeanPool/GapCVP/Part07F.lean @@ -6,7 +6,7 @@ Authors: OpenAI, Dean Cureton module -public import LeanPool.GapCVP.Part07E -- shake: keep +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 diff --git a/LeanPool/GapCVP/Part07G.lean b/LeanPool/GapCVP/Part07G.lean index 9c668ad7fc..9ab0e52b65 100644 --- a/LeanPool/GapCVP/Part07G.lean +++ b/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 -/ diff --git a/LeanPool/GapCVP/Part08B.lean b/LeanPool/GapCVP/Part08B.lean index 76e893a800..54b3c2f63a 100644 --- a/LeanPool/GapCVP/Part08B.lean +++ b/LeanPool/GapCVP/Part08B.lean @@ -6,7 +6,7 @@ Authors: OpenAI, Dean Cureton module -public import LeanPool.GapCVP.Part08A -- shake: keep +public import LeanPool.GapCVP.Part07D -- shake: keep import Mathlib.Combinatorics.Matroid.Init import Mathlib.Tactic.Positivity.Finset @@ -42,9 +42,7 @@ open GapCVP.CNFFiveFamilyPackedInitialCellDecoderTM open GapCVP.CNFFiveFamilyForbiddenWindowCoordinateTM -open GapCVP.CNFFiveFamilyForbiddenWholeClauseValidity -open GapCVP.CNFFiveFamilyIndependentFiveFamilyBundledCatalogueTM end CNFFiveFamilyIndependentFiveFamilyCatalogueSourceValidity diff --git a/LeanPool/GapCVP/Part12C.lean b/LeanPool/GapCVP/Part12C.lean index 12eb753202..39eca49d10 100644 --- a/LeanPool/GapCVP/Part12C.lean +++ b/LeanPool/GapCVP/Part12C.lean @@ -8,7 +8,6 @@ module public import LeanPool.GapCVP.Part12B public import LeanPool.GapCVP.Part12A -import LeanPool.GapCVP.Part11B import Mathlib.Algebra.Order.Floor.Semifield import Mathlib.Algebra.Order.Star.Int import Mathlib.CategoryTheory.Category.Init diff --git a/LeanPool/GapCVP/Part13.lean b/LeanPool/GapCVP/Part13.lean index facd8f3164..9cb51951a6 100644 --- a/LeanPool/GapCVP/Part13.lean +++ b/LeanPool/GapCVP/Part13.lean @@ -6,7 +6,6 @@ Authors: OpenAI, Dean Cureton module -public import LeanPool.GapCVP.Part11B public import LeanPool.GapCVP.Part12C import LeanPool.GapCVP.Part12D import Mathlib.Algebra.Order.Floor.Semifield