The starting constraint graph, over the amplifier's alphabet

Dinur's round is an endomorphism of constraint graphs over the alphabet the composition step produces, MultiTest.Alpha ReadIdx, while the reduction from 3-SAT lands in Fin 3 → Bool. The latter has eight symbols and the former 2^23, so the small alphabet embeds, and AlphabetLift carries the graph across without disturbing satisfiability.

Main definitions

• Complexity.alphaEmb — an injection of the 3-SAT alphabet into the amplifier's
• Complexity.baseCSP — the 3-SAT constraint graph, read over that alphabet

Main results

• Complexity.satisfiable_baseCSP_iff — it is satisfiable exactly when the formula is

@[reducible, inline]

abbrev Complexity.GapAlpha : Type

The alphabet Dinur's round runs over.

Equations

• Complexity.GapAlpha = Complexity.MultiTest.Alpha Complexity.ReadIdx

theorem Complexity.card_le_gapAlpha : Fintype.card (Fin 3 → Bool) ≤ Fintype.card GapAlpha

noncomputable def Complexity.alphaEmb : (Fin 3 → Bool) ↪ GapAlpha

An injection of the 3-SAT alphabet into the amplifier's.

Equations

• Complexity.alphaEmb = Complexity.alphaEmb._proof_1.some

noncomputable def Complexity.baseCSP (φ : SAT.CNF) : ConstraintGraph GapAlpha

The 3-SAT constraint graph, read over the amplifier's alphabet.

Equations

• Complexity.baseCSP φ = (Complexity.ThreeSATCSP.toGraph φ).lift ⇑Complexity.alphaEmb

@[simp]

theorem Complexity.numEdges_baseCSP (φ : SAT.CNF) : (baseCSP φ).numEdges = 3 * List.length φ

theorem Complexity.satisfiable_baseCSP_iff {φ : SAT.CNF} (h3 : φ.Is3CNF) : (baseCSP φ).Satisfiable ↔ φ.Satisfiable

theorem Complexity.numEdges_baseCSP_le_pow (φ : SAT.CNF) : (baseCSP φ).numEdges ≤ 2 ^ (3 * List.length φ)

The starting graph is small enough for logarithmically many rounds.