Complete Polylean source port

LeanPool.lean

@@ -860,15 +860,23 @@ import LeanPool.PolyaEnumerationTheorem.PermutationAuxiliary
 import LeanPool.PolyaEnumerationTheorem.ReductionToFin
 import LeanPool.PolyaEnumerationTheorem.StirlingFirstKindSum
 import LeanPool.Polylean
+import LeanPool.Polylean.Complexes
+import LeanPool.Polylean.Complexes.Constructions.UniversalCover
 import LeanPool.Polylean.Complexes.GraphPaths
 import LeanPool.Polylean.Complexes.Structures.Category
+import LeanPool.Polylean.Complexes.Structures.FreeGroupoid
 import LeanPool.Polylean.Complexes.Structures.Groupoid
+import LeanPool.Polylean.Complexes.Structures.Invertegory
 import LeanPool.Polylean.Complexes.Structures.Quiver
+import LeanPool.Polylean.Complexes.Structures.TwoComplex
+import LeanPool.Polylean.ConjInvLength
 import LeanPool.Polylean.ConjInvLength.Length
 import LeanPool.Polylean.ConjInvLength.LengthBound
+import LeanPool.Polylean.ConjInvLength.LengthNode
 import LeanPool.Polylean.ConjInvLength.MemoLength
 import LeanPool.Polylean.ConjInvLength.ProvedBound
 import LeanPool.Polylean.ConjInvLength.WordTree
+import LeanPool.Polylean.Polymath
 import LeanPool.Polylean.UnitConjecture
 import LeanPool.Polylean.UnitConjecture.AddFreeGroup
 import LeanPool.Polylean.UnitConjecture.Cocycle
@@ -880,6 +888,7 @@ import LeanPool.Polylean.UnitConjecture.GroupRing
 import LeanPool.Polylean.UnitConjecture.MetabelianGroup
 import LeanPool.Polylean.UnitConjecture.Tactics
 import LeanPool.Polylean.UnitConjecture.Tactics.AesopRuleSets
+import LeanPool.Polylean.UnitConjecture.Tactics.ReduceGoal
 import LeanPool.Polylean.UnitConjecture.TorsionFree
 import LeanPool.QuasiBorelSpaces
 import LeanPool.QuasiBorelSpaces.Basic

LeanPool/Polylean.lean

@@ -5,15 +5,23 @@ Authors: Siddhartha Gadgil, Anand Rao
 -/
 
 import LeanPool.Polylean.UnitConjecture
+import LeanPool.Polylean.Complexes
+import LeanPool.Polylean.Complexes.Constructions.UniversalCover
 import LeanPool.Polylean.Complexes.GraphPaths
 import LeanPool.Polylean.Complexes.Structures.Category
+import LeanPool.Polylean.Complexes.Structures.FreeGroupoid
 import LeanPool.Polylean.Complexes.Structures.Groupoid
+import LeanPool.Polylean.Complexes.Structures.Invertegory
 import LeanPool.Polylean.Complexes.Structures.Quiver
+import LeanPool.Polylean.Complexes.Structures.TwoComplex
+import LeanPool.Polylean.ConjInvLength
 import LeanPool.Polylean.ConjInvLength.Length
 import LeanPool.Polylean.ConjInvLength.LengthBound
+import LeanPool.Polylean.ConjInvLength.LengthNode
 import LeanPool.Polylean.ConjInvLength.MemoLength
 import LeanPool.Polylean.ConjInvLength.ProvedBound
 import LeanPool.Polylean.ConjInvLength.WordTree
+import LeanPool.Polylean.Polymath
 
 /-!
 # Polylean Unit Conjecture Counterexample

LeanPool/Polylean/Complexes.lean

@@ -0,0 +1,21 @@
+/-
+Copyright (c) 2026 Siddhartha Gadgil, Anand Rao. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Siddhartha Gadgil, Anand Rao
+-/
+
+import LeanPool.Polylean.Complexes.Constructions.UniversalCover
+import LeanPool.Polylean.Complexes.GraphPaths
+import LeanPool.Polylean.Complexes.Structures.Category
+import LeanPool.Polylean.Complexes.Structures.FreeGroupoid
+import LeanPool.Polylean.Complexes.Structures.Groupoid
+import LeanPool.Polylean.Complexes.Structures.Invertegory
+import LeanPool.Polylean.Complexes.Structures.Quiver
+import LeanPool.Polylean.Complexes.Structures.TwoComplex
+
+/-!
+# Complexes
+
+Import index for the Polylean complex and groupoid structures that are
+available without upstream `sorry`s.
+-/

LeanPool/Polylean/Complexes/Constructions/UniversalCover.lean

@@ -0,0 +1,18 @@
+/-
+Copyright (c) 2026 Siddhartha Gadgil, Anand Rao. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Siddhartha Gadgil, Anand Rao
+-/
+
+import LeanPool.Polylean.Complexes.Structures.FreeGroupoid
+
+namespace LeanPool.Polylean
+
+/-!
+# Universal Covers
+
+This upstream file currently contains only commented exploratory code after the
+`FreeGroupoid` import, so the Lean Pool port keeps the importable module stub.
+-/
+
+end LeanPool.Polylean

LeanPool/Polylean/Complexes/Structures/FreeGroupoid.lean

@@ -0,0 +1,44 @@
+/-
+Copyright (c) 2026 Siddhartha Gadgil, Anand Rao. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Siddhartha Gadgil, Anand Rao
+-/
+
+import LeanPool.Polylean.Complexes.Structures.Groupoid
+
+namespace LeanPool.Polylean
+
+universe u vq vg
+
+namespace FreeGroupoid
+
+/-- The definition of a free groupoid with basis `Q`. -/
+class Struct {S : Sort u} (Q : Quiver.{u, vq} S) (G : Groupoid.{u, vg} S) where
+  /-- Map each generating quiver edge into the generated groupoid. -/
+  map : {X Y : S} → Q.hom X Y → G.hom X Y
+  /-- Extend a quiver pre-functor out of the basis to a groupoid functor. -/
+  inducedMap : {S' : Sort u} → {G' : Groupoid.{u, vg} S'} →
+      Quiver.PreFunctor Q G'.toQuiver → Groupoid.Functor G G'
+
+/-- The inclusion of a quiver into a groupoid generated freely by it. -/
+def ι {S : Sort u} (Q : Quiver.{u, vq} S) (G : Groupoid.{u, vg} S)
+    [FreeGroupoid.Struct Q G] :
+    Quiver.PreFunctor Q G.toQuiver :=
+  { obj := id, map := FreeGroupoid.Struct.map }
+
+end FreeGroupoid
+
+/-- The universal property characterizing a free groupoid on a quiver. -/
+class FreeGroupoid {S : Sort u} (Q : Quiver.{u, vq} S) (G : Groupoid.{u, vg} S) extends
+    _root_.LeanPool.Polylean.FreeGroupoid.Struct Q G where
+  induced_extends : {S' : Sort u} → {G' : Groupoid.{u, vg} S'} →
+      (φ : Quiver.PreFunctor Q G'.toQuiver) →
+        Quiver.PreFunctor.comp (_root_.LeanPool.Polylean.FreeGroupoid.ι Q G)
+          (inducedMap φ).toPreFunctor = φ
+  induced_unique : {S' : Sort u} → {G' : Groupoid.{u, vg} S'} →
+      (Φ Ψ : Groupoid.Functor G G') →
+        Quiver.PreFunctor.comp (_root_.LeanPool.Polylean.FreeGroupoid.ι Q G) Φ.toPreFunctor =
+        Quiver.PreFunctor.comp (_root_.LeanPool.Polylean.FreeGroupoid.ι Q G) Ψ.toPreFunctor →
+          Φ = Ψ
+
+end LeanPool.Polylean

LeanPool/Polylean/Complexes/Structures/Invertegory.lean

@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2026 Siddhartha Gadgil, Anand Rao. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Siddhartha Gadgil, Anand Rao
+-/
+
+import LeanPool.Polylean.Complexes.Structures.Category
+
+namespace LeanPool.Polylean
+
+/-!
+`Invertegory` is an intermediate structure between a category and a groupoid:
+every morphism has a formal inverse, but the inverse is not required to satisfy
+the groupoid inverse laws.
+-/
+
+/-- A category equipped with formal inverses for all morphisms. -/
+class Invertegory (Obj : Sort _) extends Category Obj where
+  /-- Formal inverse of a morphism. -/
+  inv : {X Y : Obj} → (X ⟶ Y) → (Y ⟶ X)
+  invInv : ∀ e : X ⟶ Y, inv (inv e) = e
+
+namespace Invertegory
+
+/-- A morphism of `Invertegory`s preserving formal inverses. -/
+structure Functor {C D : Sort _} (ℭ : Invertegory C) (𝔇 : Invertegory D)
+    extends Category.Functor ℭ.toCategory 𝔇.toCategory where
+  mapInv : {X Y : C} → {f : X ⟶ Y} → map (Invertegory.inv f) = Invertegory.inv (map f)
+
+attribute [simp] Functor.mapInv
+
+end Invertegory
+
+end LeanPool.Polylean

LeanPool/Polylean/Complexes/Structures/TwoComplex.lean

@@ -0,0 +1,36 @@
+/-
+Copyright (c) 2026 Siddhartha Gadgil, Anand Rao. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Siddhartha Gadgil, Anand Rao
+-/
+
+import LeanPool.Polylean.Complexes.Structures.Groupoid
+
+namespace LeanPool.Polylean
+
+universe u vq vg
+
+/-!
+A two-complex is defined by an underlying quiver, a groupoid whose morphisms
+represent path-homotopy classes of the one-complex, and a pre-functor from the
+quiver to that groupoid.
+
+The lifting principle below says the groupoid has no extra edges beyond those
+generated by the quiver modulo the identifications represented by `map`.
+-/
+
+/-- A two-complex presented by a quiver and its path-homotopy groupoid. -/
+class TwoComplex (V : Sort u) [Q : Quiver.{u, vq} V] [H : Groupoid.{u, vg} V] extends
+    Quiver.PreFunctor Q H.toQuiver where
+  /-- Lift a compatible quiver pre-functor to a groupoid functor. -/
+  lift : {W : Sort u} → [G : Groupoid.{u, vg} W] →
+    (F : Quiver.PreFunctor Q G.toQuiver) →
+    (∀ {X Y : V} {e e' : X ⟶ Y}, map e = map e' → F.map e = F.map e') →
+      Groupoid.Functor H G
+  /-- The lifted functor extends the original quiver pre-functor. -/
+  lift_comp : {W : Sort u} → [G : Groupoid.{u, vg} W] →
+    (F : Quiver.PreFunctor Q G.toQuiver) →
+    (h : ∀ {X Y : V} {e e' : X ⟶ Y}, map e = map e' → F.map e = F.map e') →
+      Quiver.PreFunctor.comp ⟨obj, map⟩ (lift F h).toPreFunctor = F
+
+end LeanPool.Polylean

LeanPool/Polylean/ConjInvLength.lean

@@ -0,0 +1,18 @@
+/-
+Copyright (c) 2026 Siddhartha Gadgil, Anand Rao. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Siddhartha Gadgil, Anand Rao
+-/
+
+import LeanPool.Polylean.ConjInvLength.Length
+import LeanPool.Polylean.ConjInvLength.LengthBound
+import LeanPool.Polylean.ConjInvLength.LengthNode
+import LeanPool.Polylean.ConjInvLength.MemoLength
+import LeanPool.Polylean.ConjInvLength.ProvedBound
+import LeanPool.Polylean.ConjInvLength.WordTree
+
+/-!
+# Conjugacy-Invariant Length
+
+Import index for the Polylean conjugacy-invariant length computations.
+-/