structure UniqueGames.UniqueGame (V : Type u_1) (W : Type u_2) [DecidableEq V] [DecidableEq W] (k : ℕ) : Type (max u_1 u_2)

• edges : Finset (V × W)
• constraint : V → W → Equiv.Perm (Fin k)
• left_degree : ℕ
• right_degree : ℕ
• left_regular (v : V) : {e ∈ self.edges | e.1 = v}.card = self.left_degree
• right_regular (w : W) : {e ∈ self.edges | e.2 = w}.card = self.right_degree

structure UniqueGames.Labeling (V : Type u_1) (W : Type u_2) (k : ℕ) : Type (max u_1 u_2)

• labelV : V → Fin k
• labelW : W → Fin k

def UniqueGames.edgeSatisfied {V : Type u_1} {W : Type u_2} [DecidableEq V] [DecidableEq W] {k : ℕ} (game : UniqueGame V W k) (labeling : Labeling V W k) (v : V) (w : W) : Prop

@[implicit_reducible]

instance UniqueGames.instDecidableEdgeSatisfied {V : Type u_1} {W : Type u_2} [DecidableEq V] [DecidableEq W] {k : ℕ} (game : UniqueGame V W k) (labeling : Labeling V W k) (v : V) (w : W) : Decidable (edgeSatisfied game labeling v w)

def UniqueGames.numSatisfiedEdges {V : Type u_1} {W : Type u_2} {k : ℕ} [DecidableEq V] [DecidableEq W] (game : UniqueGame V W k) (labeling : Labeling V W k) : ℕ

def UniqueGames.numEdges {V : Type u_1} {W : Type u_2} [DecidableEq V] [DecidableEq W] {k : ℕ} (game : UniqueGame V W k) : ℕ

noncomputable def UniqueGames.fractionSatisfied {V : Type u_1} {W : Type u_2} {k : ℕ} [DecidableEq V] [DecidableEq W] (game : UniqueGame V W k) (labeling : Labeling V W k) : ℝ

noncomputable def UniqueGames.value {V : Type u_1} {W : Type u_2} {k : ℕ} [DecidableEq V] [DecidableEq W] (game : UniqueGame V W k) : ℝ

opaque UniqueGames.IsPolyTimeUniqueGameReduction {numV numW : ℕ → ℕ} {k : ℕ} : ((m : ℕ) → PCP.BinaryString m → UniqueGame (Fin (numV m)) (Fin (numW m)) k) → Prop

def UniqueGames.IsNPHardGapUniqueGame (k : ℕ) (c s : ℝ) : Prop

structure UniqueGames.NonBipartiteUniqueGame (X : Type u_1) [DecidableEq X] (k : ℕ) : Type u_1

• edges : Finset (X × X)
• constraint : X → X → Equiv.Perm (Fin k)
• degree : ℕ
• regular (x : X) : {e ∈ self.edges | e.1 = x}.card = self.degree

def UniqueGames.NonBipartiteUniqueGame.edgesWithin {X : Type u_1} [DecidableEq X] {k : ℕ} (game : NonBipartiteUniqueGame X k) (X' : Finset X) : Finset (X × X)

def UniqueGames.NonBipartiteUniqueGame.edgeSatisfiedBy {X : Type u_1} [DecidableEq X] {k : ℕ} (game : NonBipartiteUniqueGame X k) (A : X → Fin k) (e : X × X) : Prop

@[implicit_reducible]

instance UniqueGames.instDecidableEdgeSatisfiedBy {X : Type u_1} [DecidableEq X] {k : ℕ} (game : NonBipartiteUniqueGame X k) (A : X → Fin k) (e : X × X) : Decidable (game.edgeSatisfiedBy A e)

noncomputable def UniqueGames.NonBipartiteUniqueGame.fractionSatisfiedWithin {X : Type u_1} [DecidableEq X] {k : ℕ} (game : NonBipartiteUniqueGame X k) (X' : Finset X) (A : X → Fin k) : ℝ

def UniqueGames.NonBipartiteUniqueGame.edgeTSatisfiedBy {X : Type u_1} [DecidableEq X] {k : ℕ} (game : NonBipartiteUniqueGame X k) (A : X → Finset (Fin k)) (e : X × X) : Prop

@[implicit_reducible]

instance UniqueGames.instDecidableEdgeTSatisfiedBy {X : Type u_1} [DecidableEq X] {k : ℕ} (game : NonBipartiteUniqueGame X k) (A : X → Finset (Fin k)) (e : X × X) : Decidable (game.edgeTSatisfiedBy A e)

def UniqueGames.IsTAssignment {X : Type u_1} {k : ℕ} (A : X → Finset (Fin k)) (X' : Finset X) (t : ℕ) : Prop

noncomputable def UniqueGames.NonBipartiteUniqueGame.fractionTSatisfiedWithin {X : Type u_1} [DecidableEq X] {k : ℕ} (game : NonBipartiteUniqueGame X k) (X' : Finset X) (A : X → Finset (Fin k)) : ℝ

def UniqueGames.StrongUGC_YES {X : Type u_1} [DecidableEq X] [Fintype X] {k : ℕ} (game : NonBipartiteUniqueGame X k) (ε : ℝ) : Prop

def UniqueGames.StrongUGC_NO {X : Type u_1} [DecidableEq X] [Fintype X] {k : ℕ} (game : NonBipartiteUniqueGame X k) (ε : ℝ) (t : ℕ) : Prop

opaque UniqueGames.IsPolyTimeNonBipartiteUGReduction {numX : ℕ → ℕ} {k : ℕ} : ((m : ℕ) → PCP.BinaryString m → NonBipartiteUniqueGame (Fin (numX m)) k) → Prop

def UniqueGames.StrongUGC : Prop

structure UniqueGames.LabelCover (V : Type u_2) (W : Type u_3) (k l : ℕ) : Type (max u_2 u_3)

• edges : Finset (V × W)
• constraint : V → W → Fin l → Fin k

structure UniqueGames.LabelCover.Labeling (V : Type u_2) (W : Type u_3) (k l : ℕ) : Type (max u_2 u_3)

• labelV : V → Fin k
• labelW : W → Fin l

def UniqueGames.LabelCover.edgeSatisfied {V : Type u_2} {W : Type u_3} {k l : ℕ} (game : LabelCover V W k l) (labeling : Labeling V W k l) (v : V) (w : W) : Prop

@[implicit_reducible]

instance UniqueGames.instDecidableEdgeSatisfied_1 {V : Type u_2} {W : Type u_3} {k l : ℕ} (game : LabelCover V W k l) (labeling : LabelCover.Labeling V W k l) (v : V) (w : W) : Decidable (game.edgeSatisfied labeling v w)

def UniqueGames.LabelCover.numSatisfiedEdges {V : Type u_2} {W : Type u_3} {k l : ℕ} [DecidableEq V] [DecidableEq W] (game : LabelCover V W k l) (labeling : Labeling V W k l) : ℕ

noncomputable def UniqueGames.LabelCover.fractionSatisfied {V : Type u_2} {W : Type u_3} {k l : ℕ} [DecidableEq V] [DecidableEq W] (game : LabelCover V W k l) (labeling : Labeling V W k l) : ℝ

noncomputable def UniqueGames.LabelCover.value {V : Type u_2} {W : Type u_3} {k l : ℕ} [DecidableEq V] [DecidableEq W] (game : LabelCover V W k l) : ℝ

def UniqueGames.LabelCover.IsUnique {V : Type u_2} {W : Type u_3} {k l : ℕ} (game : LabelCover V W k l) : Prop

theorem UniqueGames.fractionSatisfied_le_one {V : Type u_2} {W : Type u_3} [DecidableEq V] [DecidableEq W] {k : ℕ} (game : UniqueGame V W k) (labeling : Labeling V W k) : fractionSatisfied game labeling ≤ 1

theorem UniqueGames.bddAbove_fractionSatisfied {V : Type u_2} {W : Type u_3} [DecidableEq V] [DecidableEq W] {k : ℕ} (game : UniqueGame V W k) : BddAbove (Set.range fun (labeling : Labeling V W k) => fractionSatisfied game labeling)

theorem UniqueGames.fractionSatisfied_le_value {V : Type u_2} {W : Type u_3} [DecidableEq V] [DecidableEq W] {k : ℕ} (game : UniqueGame V W k) (labeling : Labeling V W k) : fractionSatisfied game labeling ≤ value game

theorem UniqueGames.fractionSatisfied_le_of_value_le {V : Type u_2} {W : Type u_3} [DecidableEq V] [DecidableEq W] {k : ℕ} (game : UniqueGame V W k) (δ : ℝ) (hval : value game ≤ δ) (labeling : Labeling V W k) : fractionSatisfied game labeling ≤ δ

theorem uniqueGamesConjecture (ε δ : ℝ) : ε > 0 → δ > 0 → ∃ (k : ℕ), UniqueGames.IsNPHardGapUniqueGame k (1 - ε) δ

structure MaxCut.MaxCutInstance (V : Type u_1) [Fintype V] [DecidableEq V] : Type u_1

• edges : Finset (V × V)
• symm (e : V × V) : e ∈ self.edges → (e.2, e.1) ∈ self.edges

def MaxCut.numCutEdges {V : Type u_1} [Fintype V] [DecidableEq V] (G : MaxCutInstance V) (f : V → Bool) : ℕ

noncomputable def MaxCut.cutFraction {V : Type u_1} [Fintype V] [DecidableEq V] (G : MaxCutInstance V) (f : V → Bool) : ℝ

noncomputable def MaxCut.value {V : Type u_1} [Fintype V] [DecidableEq V] (G : MaxCutInstance V) : ℝ

noncomputable def MaxCut.goemansWilliamsonConstant : ℝ

def MaxCut.IsPolyTimeMaxCutInstanceReduction {numVerts : ℕ → ℕ} : ((m : ℕ) → PCP.BinaryString m → MaxCutInstance (Fin (numVerts m))) → Prop

def MaxCut.IsNPHardGapMaxCut (c s : ℝ) : Prop

opaque IsPolyTimeLongCodeReduction {numV numW k numVerts : ℕ} : (UniqueGames.UniqueGame (Fin numV) (Fin numW) k → MaxCut.MaxCutInstance (Fin numVerts)) → Prop

theorem isPolyTimeMaxCutReduction_of_compose {numV numW : ℕ → ℕ} {k : ℕ} {numVerts : ℕ → ℕ} (ugReduce : (m : ℕ) → PCP.BinaryString m → UniqueGames.UniqueGame (Fin (numV m)) (Fin (numW m)) k) (mcReduce : (m : ℕ) → UniqueGames.UniqueGame (Fin (numV m)) (Fin (numW m)) k → MaxCut.MaxCutInstance (Fin (numVerts m))) (hUG : UniqueGames.IsPolyTimeUniqueGameReduction ugReduce) (hMC : ∀ (m : ℕ), IsPolyTimeLongCodeReduction (mcReduce m)) : PCP.IsPolynomial numVerts ∧ MaxCut.IsPolyTimeMaxCutInstanceReduction fun (m : ℕ) (x : PCP.BinaryString m) => mcReduce m (ugReduce m x)

noncomputable def maxBalancedNoiseStab (ρ δ : ℝ) (k : ℕ) : ℝ

noncomputable def longCodeReduce (_ρ : ℝ) (k numV numW : ℕ) : UniqueGames.UniqueGame (Fin numV) (Fin numW) k → MaxCut.MaxCutInstance (Fin (Fintype.card (Fin numV × (Fin k → Bool))))

theorem longCode_completeness (ρ : ℝ) (hρ_pos : 0 < ρ) (hρ_lt : ρ < 1) (k numV numW : ℕ) (δ : ℝ) (hδ_pos : 0 < δ) (hδ_lt : δ < 1) (game : UniqueGames.UniqueGame (Fin numV) (Fin numW) k) (hgame : UniqueGames.value game ≥ 1 - δ) : MaxCut.value (longCodeReduce ρ k numV numW game) ≥ (1 - δ) * (1 + ρ) / 2

theorem high_influence_gives_good_labeling (k numV numW : ℕ) (δ : ℝ) (hδ_pos : 0 < δ) (hδ_lt : δ < 1) (game : UniqueGames.UniqueGame (Fin numV) (Fin numW) k) (f : Fin numV × (Fin k → Bool) → Bool) (v : Fin numV) (i : Fin k) (h_high_inf : 1 / 2 ^ k * ∑ x : Fin k → Bool, ((if f (v, x) = true then 1 else -1) - if f (v, Function.update x i !x i) = true then 1 else -1) ^ 2 / 4 > δ) : ∃ (lab : UniqueGames.Labeling (Fin numV) (Fin numW) k), UniqueGames.fractionSatisfied game lab > δ

theorem longCode_soundness (ρ : ℝ) (hρ_pos : 0 < ρ) (hρ_lt : ρ < 1) (k numV numW : ℕ) (δ : ℝ) (hδ_pos : 0 < δ) (hδ_lt : δ < 1) (game : UniqueGames.UniqueGame (Fin numV) (Fin numW) k) (hgame : UniqueGames.value game ≤ δ) : MaxCut.value (longCodeReduce ρ k numV numW game) ≤ (1 + maxBalancedNoiseStab ρ δ k) / 2

theorem longCodeReduce_isPolyTime (ρ : ℝ) (k numV numW : ℕ) : IsPolyTimeLongCodeReduction (longCodeReduce ρ k numV numW)

theorem longCode_construction_exists (ρ : ℝ) (hρ_pos : 0 < ρ) (hρ_lt : ρ < 1) (k numV numW : ℕ) (δ : ℝ) (hδ_pos : 0 < δ) (hδ_lt : δ < 1) : ∃ (numVerts : ℕ) (reduce : UniqueGames.UniqueGame (Fin numV) (Fin numW) k → MaxCut.MaxCutInstance (Fin numVerts)), IsPolyTimeLongCodeReduction reduce ∧ (∀ (game : UniqueGames.UniqueGame (Fin numV) (Fin numW) k), UniqueGames.value game ≥ 1 - δ → MaxCut.value (reduce game) ≥ (1 - δ) * (1 + ρ) / 2) ∧ ∀ (game : UniqueGames.UniqueGame (Fin numV) (Fin numW) k), UniqueGames.value game ≤ δ → MaxCut.value (reduce game) ≤ (1 + maxBalancedNoiseStab ρ δ k) / 2

theorem longCode_MIS_stabBound (ρ : ℝ) (hρ_pos : 0 < ρ) (hρ_lt : ρ < 1) (ε' : ℝ) (hε' : ε' > 0) : ∃ δ_MIS > 0, ∀ (k : ℕ) (δ : ℝ), 0 < δ → δ ≤ δ_MIS → δ < 1 → maxBalancedNoiseStab ρ δ k ≤ 1 - 2 / Real.pi * Real.arccos ρ + ε'

theorem longCodeTest_bounds (ρ : ℝ) (hρ_pos : 0 < ρ) (hρ_lt : ρ < 1) (ε : ℝ) (hε : ε > 0) : ∃ δ₀ > 0, ∀ (δ : ℝ), 0 < δ → δ ≤ δ₀ → δ < 1 → ∀ (k numV numW : ℕ), ∃ (numVerts : ℕ) (reduce : UniqueGames.UniqueGame (Fin numV) (Fin numW) k → MaxCut.MaxCutInstance (Fin numVerts)), IsPolyTimeLongCodeReduction reduce ∧ (∀ (game : UniqueGames.UniqueGame (Fin numV) (Fin numW) k), UniqueGames.value game ≥ 1 - δ → MaxCut.value (reduce game) ≥ (1 - δ) * (1 + ρ) / 2) ∧ ∀ (game : UniqueGames.UniqueGame (Fin numV) (Fin numW) k), UniqueGames.value game ≤ δ → MaxCut.value (reduce game) ≤ 1 - 1 / Real.pi * Real.arccos ρ + ε

theorem longCodeReduction_maxcut (ρ : ℝ) (hρ_pos : 0 < ρ) (hρ_lt : ρ < 1) (ε : ℝ) (hε : ε > 0) : ∃ δ > 0, ∀ (k numV numW : ℕ), ∃ (numVerts : ℕ) (reduce : UniqueGames.UniqueGame (Fin numV) (Fin numW) k → MaxCut.MaxCutInstance (Fin numVerts)), IsPolyTimeLongCodeReduction reduce ∧ (∀ (game : UniqueGames.UniqueGame (Fin numV) (Fin numW) k), UniqueGames.value game ≥ 1 - δ → MaxCut.value (reduce game) ≥ 1 / 2 + ρ / 2 - ε) ∧ ∀ (game : UniqueGames.UniqueGame (Fin numV) (Fin numW) k), UniqueGames.value game ≤ δ → MaxCut.value (reduce game) ≤ 1 - 1 / Real.pi * Real.arccos ρ + ε

theorem ug_hardness_maxcut : (∀ (ε δ : ℝ), ε > 0 → δ > 0 → ∃ (k : ℕ), UniqueGames.IsNPHardGapUniqueGame k (1 - ε) δ) → ∀ (ρ : ℝ), 0 < ρ → ρ < 1 → ∀ ε > 0, MaxCut.IsNPHardGapMaxCut (1 / 2 + ρ / 2 - ε) (1 - 1 / Real.pi * Real.arccos ρ + ε)

theorem ug_hardness_maxcut_of_ugc (hUGC : ∀ (ε δ : ℝ), ε > 0 → δ > 0 → ∃ (k : ℕ), UniqueGames.IsNPHardGapUniqueGame k (1 - ε) δ) (ε : ℝ) : ε > 0 → MaxCut.IsNPHardGapMaxCut (1 - ε) (MaxCut.goemansWilliamsonConstant + ε)