Succinct decoupled 5SAT descriptions of deciders: the statement

MIPRE.SAT.DecoupledDescriber is blueprint lem:decoupled-5sat — the paper's prop:explicit-succinct-deciders (answer_reduction.tex, sec:succinct-deciders) — the first consumer of SuccinctCookLevin and the form in which answer reduction's PCP reads the decider: a circuit with two inputs of length ℓ₀ (indexing the answer blocks a, b), three of length r₀ (indexing three separate assignments) and five signs, describing a decoupled 5SAT formula (Circuit.formula5) such that a, b extend to a satisfying five-tuple iff they encode strings of length at most T the decider accepts within cost T (Circuit.DescribesDecider), with ℓ₀ = ⌈log 2T⌉, r₀ = O(log T + log σ), at most s₀ = poly(log T, log n, Q, σ) gates, in polynomial time, the parameters computable in polynomial time from the parameters' bit lengths. Stated here, before anything is proved, so that the statement of thm:succinct-sat is validated by its consumer (planning/succinct-cook-levin.md, S0).

def MIPRE.SAT.clauseInput5 (ℓ r : ℕ) (c : Clause5 (Fin (2 ^ ℓ)) (Fin (2 ^ ℓ)) (Fin (2 ^ r)) (Fin (2 ^ r)) (Fin (2 ^ r))) : List Bool

The input bits presenting a decoupled clause to a describer with two ℓ-bit and three r-bit index inputs, then the five signs.

Equations

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

@[simp]

theorem MIPRE.SAT.length_clauseInput5 (ℓ r : ℕ) (c : Clause5 (Fin (2 ^ ℓ)) (Fin (2 ^ ℓ)) (Fin (2 ^ r)) (Fin (2 ^ r)) (Fin (2 ^ r))) : (clauseInput5 ℓ r c).length = 2 * ℓ + 3 * r + 5

def MIPRE.SAT.Circuit.formula5 (C : Circuit) (ℓ r : ℕ) : Cnf5 (Fin (2 ^ ℓ)) (Fin (2 ^ ℓ)) (Fin (2 ^ r)) (Fin (2 ^ r)) (Fin (2 ^ r))

The decoupled 5SAT formula, on two blocks of 2^ℓ and three of 2^r variables, that C succinctly describes.

Equations

• C.formula5 ℓ r = {c : MIPRE.SAT.Clause5 (Fin (2 ^ ℓ)) (Fin (2 ^ ℓ)) (Fin (2 ^ r)) (Fin (2 ^ r)) (Fin (2 ^ r)) | C.evalBits (MIPRE.SAT.clauseInput5 ℓ r c) = true}

def MIPRE.SAT.Circuit.DescribesDecider (C : Circuit) (ℓ r : ℕ) (D : Decider) (n : ℕ) (x y : Cost.BitStr) (T : ℕ) : Prop

C succinctly describes the decider 𝒟 on n, x, y and time T: for all answer blocks a, b ∈ {0,1}^{2^ℓ}, some three assignments complete them to a satisfying tuple of the described formula iff a, b are the tape encodings of strings of length at most T on which 𝒟 accepts within cost T.

Equations

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

structure MIPRE.SAT.DecoupledDescriber : Type

Explicit succinct decoupled descriptions of deciders (blueprint lem:decoupled-5sat; prop:explicit-succinct-deciders). An instance of this structure is the lemma.

• ℓ₀ : ℕ → ℕ

  ℓ₀(T), the index length of the answer blocks.

• r₀ : ℕ → ℕ → ℕ

  r₀(T, σ), the index length of the three auxiliary blocks.

• s₀ : ℕ → ℕ → ℕ → ℕ → ℕ

  s₀(n, T, Q, σ), the gate bound.

• describe : Cost.PolyTimeFun DescInput Circuit

  The algorithm, in polynomial time.

• params : Cost.PolyTimeFun (ℕ × ℕ × ℕ × ℕ) (ℕ × ℕ × ℕ)

  The parameters, in polynomial time from (n, T, Q, σ).

• params_eq (n T Q σ : ℕ) : self.params.toFun (n, T, Q, σ) = (self.ℓ₀ T, self.r₀ T σ, self.s₀ n T Q σ)
• ℓ₀_spec (T : ℕ) : 1 ≤ T → 2 * T ≤ 2 ^ self.ℓ₀ T ∧ 2 ^ self.ℓ₀ T < 4 * T

  ℓ₀ = ⌈log 2T⌉: 2T ≤ 2^{ℓ₀} < 4T for T ≥ 1.

• r₀_le : ∃ (c : ℕ), ∀ (T σ : ℕ), self.r₀ T σ ≤ c * (T.size + σ.size + 1)

  r₀ = O(log T + log σ).

• s₀_le : ∃ (P : Polynomial ℕ), ∀ (n T Q σ : ℕ), self.s₀ n T Q σ ≤ Polynomial.eval (n.size + T.size + Q + σ) P

  s₀ = poly(log n, log T, Q, σ).

• inputs_eq (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) : (self.describe.toFun ((D, n, T, Q, σ), x, y)).inputs = 2 * self.ℓ₀ T + 3 * self.r₀ T σ + 5

  The describer has 2ℓ₀ + 3r₀ + 5 inputs.

• wellFormed (inp : DescInput) : (self.describe.toFun inp).WellFormed

  The describer is a well-formed circuit.

• size_le (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) : Valid D n T Q σ x y → (self.describe.toFun ((D, n, T, Q, σ), x, y)).size ≤ self.s₀ n T Q σ

  At most s₀ gates on valid inputs.

• describes (D : Decider) (n T Q σ : ℕ) (x y : Cost.BitStr) : Valid D.prog n T Q σ x y → (self.describe.toFun ((D.prog, n, T, Q, σ), x, y)).DescribesDecider (self.ℓ₀ T) (self.r₀ T σ) D n x y T

  The describer describes the decider.