Import Wallace problem formalization

LeanPool.lean

@@ -4113,6 +4113,46 @@ import LeanPool.Vlasov.OT.Coupling
 import LeanPool.Vlasov.OT.Wasserstein
 import LeanPool.Vlasov.OT.WeakToLagrangian
 import LeanPool.Vlasov.OT.WellPosedness
+import LeanPool.Wallace
+import LeanPool.Wallace.BlockFilters
+import LeanPool.Wallace.BlockLimit
+import LeanPool.Wallace.BoundedIndependentMap
+import LeanPool.Wallace.CoefficientTransfiniteExtension
+import LeanPool.Wallace.ConcreteClosure
+import LeanPool.Wallace.ConcreteData
+import LeanPool.Wallace.ConcreteFusionRun
+import LeanPool.Wallace.ConcreteLocalSetup
+import LeanPool.Wallace.CountableClosure
+import LeanPool.Wallace.CountableDisjointization
+import LeanPool.Wallace.FiniteCombinatorics
+import LeanPool.Wallace.FullTopology
+import LeanPool.Wallace.FullTopologyMain
+import LeanPool.Wallace.FusionLimit
+import LeanPool.Wallace.FusionSchedule
+import LeanPool.Wallace.FusionStage
+import LeanPool.Wallace.GeneralMain
+import LeanPool.Wallace.GlobalAssembly
+import LeanPool.Wallace.InitialCharacter
+import LeanPool.Wallace.LocalEnumeration
+import LeanPool.Wallace.LocalFusion
+import LeanPool.Wallace.MathlibFoundations
+import LeanPool.Wallace.NontrivialSequences
+import LeanPool.Wallace.PackageTransport
+import LeanPool.Wallace.RationalAssembly
+import LeanPool.Wallace.RationalClosure
+import LeanPool.Wallace.RationalData
+import LeanPool.Wallace.RationalFusionRun
+import LeanPool.Wallace.RationalLocalSetup
+import LeanPool.Wallace.RationalTransfiniteExtension
+import LeanPool.Wallace.RationalTriangularPreprocess
+import LeanPool.Wallace.RealMain
+import LeanPool.Wallace.Result
+import LeanPool.Wallace.SeparationInterface
+import LeanPool.Wallace.TorsionFreeCoordinate
+import LeanPool.Wallace.TransfiniteExtension
+import LeanPool.Wallace.TriangularPreprocess
+import LeanPool.Wallace.TychonoffWallace
+import LeanPool.Wallace.UniformKronecker
 import LeanPool.WhiteheadTheorem
 import LeanPool.WhiteheadTheorem.Auxiliary
 import LeanPool.WhiteheadTheorem.Basic

LeanPool/Wallace.lean

@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2026 Juliane Trianon Fraga and Vinicius de Oliveira Rodrigues. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Juliane Trianon Fraga, Vinicius de Oliveira Rodrigues
+-/
+
+import LeanPool.Wallace.GeneralMain
+import LeanPool.Wallace.RealMain
+import LeanPool.Wallace.TychonoffWallace
+
+/-!
+# The Wallace problem in ZFC
+
+Source: arxiv:2608.17317, doi:10.48550/arXiv.2608.17317, url:https://github.com/vo-rodrigues/wallace-problem-zfc-paper
+Authors: Juliane Trianon Fraga, Vinicius de Oliveira Rodrigues
+Status: verified
+Main declarations: `Wallace.commutativeTychonoffWallaceCounterexampleExists`
+Tags: wallace-problem, topological-groups, set-theoretic-topology
+MSC: 22A05, 54D30, 20K20
+-/
+
+/-!
+# Countably compact groups and the Wallace counterexample
+
+This library proves the paper's main theorem for every torsion-free Abelian group of cardinality
+continuum.  It also exposes the free, rational, real, and Baer--Specker specializations.  The
+nonnegative cone in the free Abelian group gives a commutative Tychonoff countably compact
+cancellative topological additive monoid which is not a group.  The internal Section 10
+propositions on large closures and suitable sets are included as well.
+
+The public entry point exposes the three principal statements from the paper.
+-/