The gap graph of an input

Everything the reduction does, in one function: read the formula, write its constraint graph padded to a size the input's length decides, and amplify it as many times as a logarithmic ruler is long.

Main definitions

• Complexity.gapAllG — the graph itself
• Complexity.gapAll — that graph, as a string

Main results

• Complexity.gapAll_eq — the string is the graph's encoding
• Complexity.satisfiable_gapAllG — completeness
• Complexity.gap_le_unsatVal_gapAllG — soundness

noncomputable def Complexity.gapRuler (padU : List Bool → List Bool) (x : List Bool) : List Bool

How many rounds an input gets: enough that the padded edge count is below 2 ^ rounds.

Equations

• Complexity.gapRuler padU x = Complexity.logRuler (padU x)

theorem Complexity.gapRuler_mem_FP (padU : List Bool → List Bool) (hpad : padU ∈ FP) : gapRuler padU ∈ FP

@[simp]

theorem Complexity.length_gapRuler (padU : List Bool → List Bool) (x : List Bool) : (gapRuler padU x).length = rulerLen (padU x).length

noncomputable def Complexity.gapAllG (F : FinBase) (hd : 1 < F.deg) (padU : List Bool → List Bool) {Φ : List Bool → SAT.CNF} (x : List Bool) : ConstraintGraph DinurAlpha

The gap graph of an input.

Equations

• Complexity.gapAllG F hd padU x = (Complexity.Dinur.step (F.toFamily hd) (Complexity.qOf F hd) ⋯)^[Complexity.rulerLen (padU x).length] ((Complexity.baseCSP (Φ x)).padGraph ⋯ (padU x).length)

noncomputable def Complexity.gapAll (F : FinBase) (hd : 1 < F.deg) (E padU : List Bool → List Bool) : List Bool → List Bool

The gap graph of an input, as a string.

Equations

• Complexity.gapAll F hd E padU = Complexity.gapFn F hd (Complexity.basePadFn E padU Complexity.baseCodeFn) (Complexity.gapRuler padU)

theorem Complexity.gapAll_eq (F : FinBase) (hd : 1 < F.deg) (E padU : List Bool → List Bool) {Φ : List Bool → SAT.CNF} (hE : ∀ (x : List Bool), E x = (Φ x).encode) (h3 : ∀ (x : List Bool), (Φ x).Is3CNF) (hmark : ∀ (x : List Bool), padU x = List.replicate (padU x).length true) (hle : ∀ (x : List Bool), 3 * List.length (Φ x) ≤ (padU x).length) (x : List Bool) : gapAll F hd E padU x = encGraph (gapAllG F hd padU x)

The gap

theorem Complexity.numEdges_padded_le (padU : List Bool → List Bool) {Φ : List Bool → SAT.CNF} (x : List Bool) (hle : 3 * List.length (Φ x) ≤ (padU x).length) : ((baseCSP (Φ x)).padGraph ⋯ (padU x).length).numEdges ≤ 2 ^ rulerLen (padU x).length

theorem Complexity.satisfiable_gapAllG (F : FinBase) (hd : 1 < F.deg) (padU : List Bool → List Bool) {Φ : List Bool → SAT.CNF} (h3 : ∀ (x : List Bool), (Φ x).Is3CNF) (hle : ∀ (x : List Bool), 3 * List.length (Φ x) ≤ (padU x).length) (x : List Bool) (h : (Φ x).Satisfiable) : (gapAllG F hd padU x).Satisfiable

Completeness.

theorem Complexity.gap_le_unsatVal_gapAllG (F : FinBase) (hd : 1 < F.deg) (padU : List Bool → List Bool) {Φ : List Bool → SAT.CNF} (h3 : ∀ (x : List Bool), (Φ x).Is3CNF) (hle : ∀ (x : List Bool), 3 * List.length (Φ x) ≤ (padU x).length) (x : List Bool) (h : ¬(Φ x).Satisfiable) : (Dinur.amplifier (F.toFamily hd)).gap ≤ (gapAllG F hd padU x).unsatVal

Soundness.

Writing it is polynomial-time

noncomputable def Complexity.growthExp (F : FinBase) (hd : 1 < F.deg) : ℕ

The exponent by which the whole iteration can grow the graph.

Equations

• Complexity.growthExp F hd = Complexity.rulerLen (Complexity.Dinur.edgeFactor (F.toFamily hd) (Complexity.qOf F hd))

theorem Complexity.pow_edgeFactor_le (F : FinBase) (hd : 1 < F.deg) (m : ℕ) : Dinur.edgeFactor (F.toFamily hd) (qOf F hd) ^ rulerLen m ≤ (2 * m + 1) ^ growthExp F hd

noncomputable def Complexity.widthPoly (F : FinBase) (hd : 1 < F.deg) (p₀ q : Polynomial ℕ) : Polynomial ℕ

How wide the iteration ever gets.

def Complexity.widthFn (p₀ q : Polynomial ℕ) (v cw d n : ℕ) : ℕ

How wide the iteration ever gets, as a function of the input's length. The round's constants are parameters, so that no tactic here ever meets them.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.widthFn_hasRuler (p₀ q : Polynomial ℕ) (v cw d : ℕ) : HasRuler (widthFn p₀ q v cw d)

theorem Complexity.gapAll_mem_FP (F : FinBase) (hd : 1 < F.deg) (E padU : List Bool → List Bool) {Φ : List Bool → SAT.CNF} (hEfp : E ∈ FP) (hpad : padU ∈ FP) (hE : ∀ (x : List Bool), E x = (Φ x).encode) (h3 : ∀ (x : List Bool), (Φ x).Is3CNF) (hmark : ∀ (x : List Bool), padU x = List.replicate (padU x).length true) (hle : ∀ (x : List Bool), 3 * List.length (Φ x) ≤ (padU x).length) (p₀ q : Polynomial ℕ) (hp₀ : ∀ (x : List Bool), (E x).length ≤ Polynomial.eval x.length p₀) (hq : ∀ (x : List Bool), (padU x).length = Polynomial.eval x.length q) : gapAll F hd E padU ∈ FP

Writing the gap graph is polynomial-time.