The starting graph, written out

BaseAlg reads the starting graph's numbers straight off a formula, which is all a verifier needs. Amplification needs more: the graph itself, as a string the round function can consume. This module writes it, reusing that module's readers.

An edge's constraint depends on the formula only through the three signs of its clause and which of the three positions the edge checks — twelve bits in all. That is what baseCodeKey extracts and relOfSigns turns back into a constraint, so the constraint's code is written by a table lookup.

Main definitions

• Complexity.relOfSigns — an edge's constraint, as a function of the signs
• Complexity.baseCodeKey — the bounded data an edge's constraint depends on
• Complexity.baseGraphFn — the starting graph, as a string

Main results

• Complexity.rel_baseCSP — the constraint depends only on the signs
• Complexity.baseGraphFn_mem_FP — writing the graph is polynomial-time
• Complexity.baseGraphFn_eq — it writes the right graph

The constraint, from the signs alone

noncomputable def Complexity.relOfSigns (s : Fin 3 → Bool) (p : Fin 3) : GapAlpha → GapAlpha → Bool

The constraint of an edge that checks position p of a clause whose three literals have signs s: both endpoints name triples in the image of the alphabet embedding, the first satisfies the clause, and the two agree on the checked position.

Equations

• Complexity.relOfSigns s p u v = decide (∃ (a₁ : Fin 3 → Bool) (a₂ : Fin 3 → Bool), Complexity.alphaEmb a₁ = u ∧ Complexity.alphaEmb a₂ = v ∧ (∃ (q : Fin 3), a₁ q = s q) ∧ a₁ p = a₂ 0)

theorem Complexity.rel_baseCSP (φ : SAT.CNF) (e : ℕ) (he : e < (baseCSP φ).numEdges) : (baseCSP φ).rel ⟨e, he⟩ = relOfSigns (fun (q : Fin 3) => (ThreeSATCSP.litOf φ (e / 3) q).sign) ⟨e % 3, ⋯⟩

The constraint depends only on the signs.

The key

noncomputable def Complexity.baseCodeKey (E : List Bool → List Bool) (w : List Bool) : List Bool

The data an edge's constraint depends on: the clause's three signs and which of them the edge reads.

Equations

• Complexity.baseCodeKey E w = Complexity.pair (Complexity.baseSigns E (Complexity.pair w [])) (Complexity.modFn [false, false, false] (Complexity.pairSnd w))

theorem Complexity.baseCodeKey_mem_FP (E : List Bool → List Bool) (hE : E ∈ FP) : baseCodeKey E ∈ FP

theorem Complexity.baseCodeKey_length_le (E : List Bool → List Bool) (w : List Bool) : (baseCodeKey E w).length ≤ 12

theorem Complexity.baseCodeKey_pair (E : List Bool → List Bool) {Φ : List Bool → SAT.CNF} (hE : ∀ (x : List Bool), E x = (Φ x).encode) (h3 : ∀ (x : List Bool), (Φ x).Is3CNF) (x : List Bool) {e : ℕ} (he : e < 3 * List.length (Φ x)) : baseCodeKey E (pair x (List.replicate e true)) = pair [(ThreeSATCSP.litOf (Φ x) (e / 3) 0).sign, (ThreeSATCSP.litOf (Φ x) (e / 3) 1).sign, (ThreeSATCSP.litOf (Φ x) (e / 3) 2).sign] (List.replicate (e % 3) true)

The constraint's code, from the key

noncomputable def Complexity.baseRelOfKey (k : List Bool) : GapAlpha → GapAlpha → Bool

The constraint an edge's key stands for.

Equations

• Complexity.baseRelOfKey k = Complexity.relOfSigns (fun (q : Fin 3) => (Complexity.pairFst k).getD (↑q) false) ⟨(Complexity.pairSnd k).length % 3, ⋯⟩

noncomputable def Complexity.baseCodeFn (k : List Bool) : List Bool

The constraint's code, in unary, from the key.

Equations

• Complexity.baseCodeFn k = List.replicate (Complexity.codeOfRel (Complexity.baseRelOfKey k)) true

theorem Complexity.relOfSigns_congr {s t : Fin 3 → Bool} {m n : ℕ} (hm : m < 3) (hn : n < 3) (hs : s = t) (h : m = n) : relOfSigns s ⟨m, hm⟩ = relOfSigns t ⟨n, hn⟩

theorem Complexity.baseCodeFn_codeKey (E : List Bool → List Bool) {Φ : List Bool → SAT.CNF} (hE : ∀ (x : List Bool), E x = (Φ x).encode) (h3 : ∀ (x : List Bool), (Φ x).Is3CNF) (x : List Bool) (e : ℕ) (he : e < (baseCSP (Φ x)).numEdges) : baseCodeFn (baseCodeKey E (pair x (List.replicate e true))) = List.replicate (codeOfRel ((baseCSP (Φ x)).rel ⟨e, he⟩)) true

The counts

noncomputable def Complexity.baseVertsU (E : List Bool → List Bool) (z : List Bool) : List Bool

The number of vertices, in unary: one per variable, one per clause.

Equations

• Complexity.baseVertsU E z = Complexity.marks (Complexity.baseMaxU E z) ++ [true] ++ Complexity.divC 3 (Complexity.baseEdgesU E z)

theorem Complexity.baseVertsU_mem_FP (E : List Bool → List Bool) (hE : E ∈ FP) : baseVertsU E ∈ FP

theorem Complexity.baseVertsU_eq (E : List Bool → List Bool) {Φ : List Bool → SAT.CNF} (hE : ∀ (x : List Bool), E x = (Φ x).encode) (h3 : ∀ (x : List Bool), (Φ x).Is3CNF) (x : List Bool) : baseVertsU E x = List.replicate (baseCSP (Φ x)).numVerts true

theorem Complexity.baseEdgesU_count (E : List Bool → List Bool) {Φ : List Bool → SAT.CNF} (hE : ∀ (x : List Bool), E x = (Φ x).encode) (x : List Bool) : baseEdgesU E x = List.replicate (baseCSP (Φ x)).numEdges true

The endpoints

theorem Complexity.baseTailU_val (E : List Bool → List Bool) {Φ : List Bool → SAT.CNF} (hE : ∀ (x : List Bool), E x = (Φ x).encode) (h3 : ∀ (x : List Bool), (Φ x).Is3CNF) (x : List Bool) (e : ℕ) (he : e < (baseCSP (Φ x)).numEdges) : (baseTailU E (pair x (List.replicate e true))).length = ↑((baseCSP (Φ x)).tail ⟨e, he⟩)

theorem Complexity.baseHeadU_val (E : List Bool → List Bool) {Φ : List Bool → SAT.CNF} (hE : ∀ (x : List Bool), E x = (Φ x).encode) (h3 : ∀ (x : List Bool), (Φ x).Is3CNF) (x : List Bool) (e : ℕ) (he : e < (baseCSP (Φ x)).numEdges) : (baseHeadU E (pair x (List.replicate e true))).length = ↑((baseCSP (Φ x)).head ⟨e, he⟩)

The graph

noncomputable def Complexity.baseGraphFn (E g : List Bool → List Bool) : List Bool → List Bool

The starting graph, as a string.

Equations

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

theorem Complexity.baseGraphFn_mem_FP (E : List Bool → List Bool) (hE : E ∈ FP) (g : List Bool → List Bool) : baseGraphFn E g ∈ FP

theorem Complexity.baseGraphFn_eq (E : List Bool → List Bool) {Φ : List Bool → SAT.CNF} (hE : ∀ (x : List Bool), E x = (Φ x).encode) (h3 : ∀ (x : List Bool), (Φ x).Is3CNF) (x : List Bool) : baseGraphFn E baseCodeFn x = encGraph (baseCSP (Φ x))

The rule writes the starting graph.

Padded to a fixed size

theorem Complexity.numVerts_baseCSP_pos (φ : SAT.CNF) : 0 < (baseCSP φ).numVerts

The base graph always has a vertex.

noncomputable def Complexity.trivCode : List Bool

The code of the constraint that is always true, in unary.

Equations

• Complexity.trivCode = List.replicate (Complexity.codeOfRel fun (x x_1 : Complexity.GapAlpha) => true) true

noncomputable def Complexity.basePadFn (E padU g : List Bool → List Bool) : List Bool → List Bool

The starting graph, padded: the edge count is whatever padU says, so it can be made to depend on the input's length alone.

Equations

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

theorem Complexity.basePadFn_mem_FP (E : List Bool → List Bool) {padU : List Bool → List Bool} (hE : E ∈ FP) (hP : padU ∈ FP) (g : List Bool → List Bool) : basePadFn E padU g ∈ FP

theorem Complexity.basePadFn_eq (E : List Bool → List Bool) {Φ : List Bool → SAT.CNF} {padU : List Bool → List Bool} (hE : ∀ (x : List Bool), E x = (Φ x).encode) (h3 : ∀ (x : List Bool), (Φ x).Is3CNF) (x : List Bool) (hPmark : padU x = List.replicate (padU x).length true) (hPle : 3 * List.length (Φ x) ≤ (padU x).length) : basePadFn E padU baseCodeFn x = encGraph ((baseCSP (Φ x)).padGraph ⋯ (padU x).length)

The rule writes the padded starting graph.