import Mathlib.Algebra.Field.Basic
import UnitConjecture.TorsionFree
import UnitConjecture.GroupRing


/-!

## Giles Gardam's result

The proof of the theorem `𝔽₂[P]` has non-trivial units. Together with the main result of `TorsionFree` -- that `P` is torsion-free, 
this completes the formal proof of Gardam's theorem that Kaplansky's Unit Conjecture is false.
-/


section Preliminaries

/-! ### Preliminaries -/

/-- The definition of an element of a free module being trivial, i.e., of the form `k•x` for `x : X` and `k ≠ 0`. -/
def 
trivialElem: {R X : Type} → [inst : Ring R] → [inst_1 : DecidableEq X] → R[X] → Prop
trivialElem {
R: Type ?u.2
R 
X: Type ?u.5
X : 
Type _: Type (?u.2+1)
Type _} [
Ring: Type ?u.8 → Type ?u.8
Ring 
R: Type ?u.2
R] [
DecidableEq: Sort ?u.11 → Sort (max1?u.11)
DecidableEq 
X: Type ?u.5
X] (
a: R[X]
a : 
FreeModule: (R X : Type) → [inst : Ring R] → [inst : DecidableEq X] → Type
FreeModule 
R: Type ?u.2
R 
X: Type ?u.5
X) : 
Prop: Type
Prop :=
  ∃! 
x: X
x : 
X: Type
X, 
FreeModule.coordinates: {R : Type} → [inst : Ring R] → {X : Type} → [inst_1 : DecidableEq X] → X → R[X] → R
FreeModule.coordinates 
x: X
x 
a: R[X]
a ≠ 
0: ?m.177
0

/-- The statement of Kaplansky's Unit Conjecture:
The only units in a group ring, when the group is torsion-free and the ring is a field, are the trivial units. -/
def 
UnitConjecture: Prop
UnitConjecture : 
Prop: Type
Prop :=
  ∀ {
F: Type ?u.426
F : 
Type _: Type (?u.426+1)
Type _} [
Field: Type ?u.429 → Type ?u.429
Field 
F: Type ?u.426
F] [
DecidableEq: Sort ?u.432 → Sort (max1?u.432)
DecidableEq 
F: Type ?u.426
F] 
  {
G: Type ?u.441
G : 
Type _: Type (?u.441+1)
Type _} [
Group: Type ?u.444 → Type ?u.444
Group 
G: Type ?u.441
G] [
DecidableEq: Sort ?u.447 → Sort (max1?u.447)
DecidableEq 
G: Type ?u.441
G] [
TorsionFree: (G : Type ?u.456) → [inst : Group G] → Type
TorsionFree 
G: Type ?u.441
G],
    ∀ 
u: (F[G])ˣ
u : (
F: Type ?u.426
F[
G: Type ?u.441
G])ˣ, 
trivialElem: {R X : Type} → [inst : Ring R] → [inst_1 : DecidableEq X] → R[X] → Prop
trivialElem (
u: (F[G])ˣ
u : 
F: Type ?u.426
F[
G: Type ?u.441
G])

/-- The finite field on two elements. -/
abbrev 
𝔽₂: Type
𝔽₂ := 
Fin: ℕ → Type
Fin 
2: ?m.2180
2

instance: Field 𝔽₂
instance : 
Field: Type ?u.2190 → Type ?u.2190
Field 
𝔽₂: Type
𝔽₂ where
  inv := 
id: {α : Sort ?u.2234} → α → α
id
  exists_pair_ne := ⟨
0: ?m.2272
0, 
1: ?m.2314
1, by 
0 ≠ 1decide
Goals accomplished! 🐙⟩
  mul_inv_cancel := fun
        | 
0: Fin 2
0, 
h: 0 ≠ 0
h => by 
h: 0 ≠ 0

0 * 0⁻¹ = 1contradiction
Goals accomplished! 🐙
        | 
1: Fin 2
1, _ => 
rfl: ∀ {α : Sort ?u.2406} {a : α}, a = a
rfl
  inv_zero := 
rfl: ∀ {α : Sort ?u.3124} {a : α}, a = a
rfl
  div_eq_mul_inv := by 
∀ (a b : 𝔽₂), a / b = a * b⁻¹decide
Goals accomplished! 🐙

instance 
ringElem: Coe P (𝔽₂[P])
ringElem : 
Coe: Sort ?u.4475 → Sort ?u.4474 → Sort (max(max1?u.4475)?u.4474)
Coe 
P: Type
P (
𝔽₂: Type
𝔽₂[
P: Type
P]) where
    coe 
g: ?m.4575
g := ⟦[(
1: ?m.4593
1, 
g: ?m.4575
g)]⟧

end Preliminaries

section Constants

namespace P

/-!
The main constants of the group `P`.
-/

abbrev 
x: P
x : 
P: Type
P := (
K.x: K
K.x, 
Q.e: Q
Q.e)
abbrev 
y: P
y : 
P: Type
P := (
K.y: K
K.y, 
Q.e: Q
Q.e)
abbrev 
z: P
z : 
P: Type
P := (
K.z: K
K.z, 
Q.e: Q
Q.e)
abbrev 
a: P
a : 
P: Type
P := ((
0: ?m.6021
0, 
0: ?m.6036
0, 
0: ?m.6039
0), 
Q.a: Q
Q.a)
abbrev 
b: P
b : 
P: Type
P := ((
0: ?m.6191
0, 
0: ?m.6206
0, 
0: ?m.6209
0), 
Q.b: Q
Q.b)

end P

namespace Gardam

open P

/-! The components of the non-trivial unit `α`. -/
def 
p: 𝔽₂[P]
p : 
𝔽₂: Type
𝔽₂[
P: Type
P] := (
1: ?m.6481
1 : 
𝔽₂: Type
𝔽₂[
P: Type
P]) +  
x: P
x +  
y: P
y +  
x: P
x*
y: P
y +  
z: P
z⁻¹ + 
x: P
x*
z: P
z⁻¹ + 
y: P
y*
z: P
z⁻¹ + 
x: P
x*
y: P
y*
z: P
z⁻¹
def 
q: 𝔽₂[P]
q : 
𝔽₂: Type
𝔽₂[
P: Type
P] := (
x: P
x⁻¹*
y: P
y⁻¹ : 
𝔽₂: Type
𝔽₂[
P: Type
P]) + 
x: P
x + 
y: P
y⁻¹*
z: P
z + 
z: P
z
def 
r: 𝔽₂[P]
r : 
𝔽₂: Type
𝔽₂[
P: Type
P] := (
1: ?m.18429
1 : 
𝔽₂: Type
𝔽₂[
P: Type
P]) + 
x: P
x + 
y: P
y⁻¹*
z: P
z + 
x: P
x*
y: P
y*
z: P
z
def 
s: 𝔽₂[P]
s : 
𝔽₂: Type
𝔽₂[
P: Type
P] := (
1: ?m.21203
1 : 
𝔽₂: Type
𝔽₂[
P: Type
P]) + 
x: P
x*
z: P
z⁻¹ + 
x: P
x⁻¹*
z: P
z⁻¹ + 
y: P
y*
z: P
z⁻¹ + 
y: P
y⁻¹*
z: P
z⁻¹

/-- The non-trivial unit `α`. -/
def 
α: 𝔽₂[P]
α : 
𝔽₂: Type
𝔽₂[
P: Type
P] := 
p: 𝔽₂[P]
p  +  
q: 𝔽₂[P]
q * 
a: P
a  +  
r: 𝔽₂[P]
r * 
b: P
b  +  
s: 𝔽₂[P]
s * 
a: P
a * 
b: P
b
 
/-! The components of the inverse `α'` of the non-trivial unit `α`. -/
def 
p': 𝔽₂[P]
p' : 
𝔽₂: Type
𝔽₂[
P: Type
P] := 
x: P
x⁻¹ * (
a: P
a⁻¹  * 
p: 𝔽₂[P]
p * 
a: P
a)
def 
q': 𝔽₂[P]
q' : 
𝔽₂: Type
𝔽₂[
P: Type
P] := -(
x: P
x⁻¹ * 
q: 𝔽₂[P]
q)
def 
r': 𝔽₂[P]
r' : 
𝔽₂: Type
𝔽₂[
P: Type
P] := -(
y: P
y⁻¹ * 
r: 𝔽₂[P]
r)
def 
s': 𝔽₂[P]
s' : 
𝔽₂: Type
𝔽₂[
P: Type
P] := 
z: P
z⁻¹ * (
a: P
a⁻¹ * 
s: 𝔽₂[P]
s * 
a: P
a)

/-- The inverse `α'` of the non-trivial unit `α`. -/
def 
α': 𝔽₂[P]
α' : 
𝔽₂: Type
𝔽₂[
P: Type
P] := 
p': 𝔽₂[P]
p'  +  
q': 𝔽₂[P]
q' * 
a: P
a  +  
r': 𝔽₂[P]
r' * 
b: P
b  +  
s': 𝔽₂[P]
s' * 
a: P
a * 
b: P
b

end Gardam

end Constants


section Verification

/-! 
### Verification

The main verification of Giles Gardam's result. 
-/

namespace Gardam

open P

/-- A proof that the unit is non-trivial. -/
theorem 
α_nonTrivial: ¬trivialElem α
α_nonTrivial : ¬ (
trivialElem: {R X : Type} → [inst : Ring R] → [inst_1 : DecidableEq X] → R[X] → Prop
trivialElem 
α: 𝔽₂[P]
α) := by
    
¬trivialElem αintro ⟨
g: P
g, _, (
eqg: ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g
eqg : ∀ y, α.coordinates y ≠ 0 → y = g)⟩
g: P

left✝: (fun x => FreeModule.coordinates x α ≠ 0) g

eqg: ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g

False
    
¬trivialElem αhave : 
z: P
z⁻¹ = 
g: P
g := 
g: P

left✝: (fun x => FreeModule.coordinates x α ≠ 0) g

eqg: ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g

Falseby
      
g: P

left✝: (fun x => FreeModule.coordinates x α ≠ 0) g

eqg: ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g

z⁻¹ = gapply 
eqg: ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g
eqg
g: P

left✝: (fun x => FreeModule.coordinates x α ≠ 0) g

eqg: ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g

a
FreeModule.coordinates z⁻¹ α ≠ 0;
g: P

left✝: (fun x => FreeModule.coordinates x α ≠ 0) g

eqg: ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g

a
FreeModule.coordinates z⁻¹ α ≠ 0 
g: P

left✝: (fun x => FreeModule.coordinates x α ≠ 0) g

eqg: ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g

z⁻¹ = gnative_decide
Goals accomplished! 🐙
    
¬trivialElem αhave : 
x: P
x * 
y: P
y = 
g: P
g := 
g: P

left✝: (fun x => FreeModule.coordinates x α ≠ 0) g

eqg: ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g

this: z⁻¹ = g

Falseby
      
g: P

left✝: (fun x => FreeModule.coordinates x α ≠ 0) g

eqg: ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g

this: z⁻¹ = g

x * y = gapply 
eqg: ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g
eqg
g: P

left✝: (fun x => FreeModule.coordinates x α ≠ 0) g

eqg: ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g

this: z⁻¹ = g

a
FreeModule.coordinates (x * y) α ≠ 0;
g: P

left✝: (fun x => FreeModule.coordinates x α ≠ 0) g

eqg: ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g

this: z⁻¹ = g

a
FreeModule.coordinates (x * y) α ≠ 0 
g: P

left✝: (fun x => FreeModule.coordinates x α ≠ 0) g

eqg: ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g

this: z⁻¹ = g

x * y = gnative_decide
Goals accomplished! 🐙
    
¬trivialElem αhave : 
z: P
z⁻¹ = 
x: P
x * 
y: P
y := 
g: P

left✝: (fun x => FreeModule.coordinates x α ≠ 0) g

eqg: ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g

this✝: z⁻¹ = g

this: x * y = g

Falseby
      
g: P

left✝: (fun x => FreeModule.coordinates x α ≠ 0) g

eqg: ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g

this✝: z⁻¹ = g

this: x * y = g

z⁻¹ = x * yrefine' 
Eq.trans: ∀ {α : Sort ?u.38198} {a b c : α}, a = b → b = c → a = c
Eq.trans 
_: ?m.38200 = ?m.38201
_ (
Eq.symm: ∀ {α : Sort ?u.38204} {a b : α}, a = b → b = a
Eq.symm 
_: ?m.38206 = ?refine'_2
_)
g: P

left✝: (fun x => FreeModule.coordinates x α ≠ 0) g

eqg: ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g

this✝: z⁻¹ = g

this: x * y = g

refine'_1
z⁻¹ = ?refine'_2
g: P

left✝: (fun x => FreeModule.coordinates x α ≠ 0) g

eqg: ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g

this✝: z⁻¹ = g

this: x * y = g

refine'_2
P
g: P

left✝: (fun x => FreeModule.coordinates x α ≠ 0) g

eqg: ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g

this✝: z⁻¹ = g

this: x * y = g

refine'_3
x * y = ?refine'_2 
g: P

left✝: (fun x => FreeModule.coordinates x α ≠ 0) g

eqg: ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g

this✝: z⁻¹ = g

this: x * y = g

z⁻¹ = x * y<;>
g: P

left✝: (fun x => FreeModule.coordinates x α ≠ 0) g

eqg: ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g

this✝: z⁻¹ = g

this: x * y = g

refine'_1
z⁻¹ = ?refine'_2
g: P

left✝: (fun x => FreeModule.coordinates x α ≠ 0) g

eqg: ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g

this✝: z⁻¹ = g

this: x * y = g

refine'_2
P
g: P

left✝: (fun x => FreeModule.coordinates x α ≠ 0) g

eqg: ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g

this✝: z⁻¹ = g

this: x * y = g

refine'_3
x * y = ?refine'_2 
g: P

left✝: (fun x => FreeModule.coordinates x α ≠ 0) g

eqg: ∀ (y : P), FreeModule.coordinates y α ≠ 0 → y = g

this✝: z⁻¹ = g

this: x * y = g

z⁻¹ = x * yassumption
Goals accomplished! 🐙
    
¬trivialElem αsimp at 
this: z⁻¹ = x * y
this
Goals accomplished! 🐙

/-! The fact that the counter-example `α` is in fact a unit of the group ring `𝔽₂[P]` is verified by 
  computing the product of `α` with its inverse `α'` and checking that the result is `(1 : 𝔽₂[P])`.

  The computational aspects of the group ring implementation and the Metabelian construction are used here. -/

/-- A proof of the existence of a non-trivial unit in `𝔽₂[P]`. -/
def 
Counterexample: { u // ¬trivialElem ↑u }
Counterexample : {
u: (𝔽₂[P])ˣ
u : (
𝔽₂: Type
𝔽₂[
P: Type
P])ˣ // ¬(
trivialElem: {R X : Type} → [inst : Ring R] → [inst_1 : DecidableEq X] → R[X] → Prop
trivialElem 
u: (𝔽₂[P])ˣ
u.
val: {α : Type ?u.39602} → [inst : Monoid α] → αˣ → α
val)} := 
  ⟨⟨
α: 𝔽₂[P]
α, 
α': 𝔽₂[P]
α', by 
α * α' = 1native_decide
Goals accomplished! 🐙, by 
α' * α = 1native_decide
Goals accomplished! 🐙⟩, 
α_nonTrivial: ¬trivialElem α
α_nonTrivial⟩

/-- Giles Gardam's result - Kaplansky's Unit Conjecture is false. -/
theorem 
GardamTheorem: ¬UnitConjecture
GardamTheorem : ¬ 
UnitConjecture: Prop
UnitConjecture :=
   fun 
conjecture: ?m.41987
conjecture => 
Counterexample: { u // ¬trivialElem ↑u }
Counterexample.
prop: ∀ {α : Sort ?u.41989} {p : α → Prop} (x : Subtype p), p ↑x
prop <| 
    
conjecture: ?m.41987
conjecture (F := 
𝔽₂: Type
𝔽₂) (G := 
P: Type
P) 
Counterexample: { u // ¬trivialElem ↑u }
Counterexample.
val: {α : Sort ?u.42005} → {p : α → Prop} → Subtype p → α
val

end Gardam

end Verification