Succinct decoupled 6SAT descriptions of deciders with three input windows: the statement

Paper II's prop:explicit-padded-succinct-deciders (II:8675, a proof sketch), in the form the Aldous–Lyons track's answer reduction needs (planning/aldous-lyons-track.md, slice P4g). Its output indicator L* reads three strings — the two readable answers and the encoding O of the decoupled linear system — and the PCP must hold each of them in its own block of variables: the isolated player B, compared with the second, cannot hold a block containing O, which depends on both readable answers. lem:decoupled-5sat (MIPRE.SAT.DecoupledDescriber) has two answer blocks; this statement has three windows.

A decider reads (n, x, y, a, b); the tableau of thm:succinct-sat has the tape encoding of a on its variables [0, 2T) and that of b on [2T, 4T). The describer outputs a circuit with three index inputs of lengths ℓa, ℓb, ℓc, three of length r and six signs, describing a decoupled 6SAT formula (Circuit.formula6) on blocks of 2^ℓa, 2^ℓb, 2^ℓc and three times 2^r variables, such that three tables A, B, C extend to a satisfying 6-tuple exactly when there are strings a, b of length at most T that the decider accepts within cost T, with A and C the consecutive windows of lengths 2^ℓa and 2^ℓc at the start of the tape encoding of a, and B the first 2^ℓb bits of that of b (Circuit.DescribesWindows). The third window starts at 2^ℓa, a power of two, so that the describer computes its offset without binary addition. L* reads a = a^R ++ O and b = b^R. A decider that accepts only strings filling their windows exactly is then described completely by the windows: that is how L*, which checks the lengths of its inputs, is used.

The window lengths are inputs, in unary, since a polynomial-time program must be polynomial in its input on every input; the answer reduction computes them from its parameters.

Decoupled 6SAT

structure MIPRE.SAT.Clause6 (V₁ : Type u_1) (V₂ : Type u_2) (V₃ : Type u_3) (V₄ : Type u_4) (V₅ : Type u_5) (V₆ : Type u_6) : Type (max (max (max (max (max u_1 u_2) u_3) u_4) u_5) u_6)

A decoupled 6SAT clause: one literal from each of six blocks.

• l₁ : Lit V₁
• l₂ : Lit V₂
• l₃ : Lit V₃
• l₄ : Lit V₄
• l₅ : Lit V₅
• l₆ : Lit V₆

def MIPRE.SAT.Clause6.eval {V₁ : Type u_1} {V₂ : Type u_2} {V₃ : Type u_3} {V₄ : Type u_4} {V₅ : Type u_5} {V₆ : Type u_6} (w₁ : V₁ → Bool) (w₂ : V₂ → Bool) (w₃ : V₃ → Bool) (w₄ : V₄ → Bool) (w₅ : V₅ → Bool) (w₆ : V₆ → Bool) (c : Clause6 V₁ V₂ V₃ V₄ V₅ V₆) : Bool

The value of a decoupled clause on six assignments.

Equations

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

@[reducible, inline]

abbrev MIPRE.SAT.Cnf6 (V₁ : Type u_1) (V₂ : Type u_2) (V₃ : Type u_3) (V₄ : Type u_4) (V₅ : Type u_5) (V₆ : Type u_6) : Type (max (max (max (max (max u_6 u_5) u_4) u_3) u_2) u_1)

A decoupled 6SAT formula.

Equations

• MIPRE.SAT.Cnf6 V₁ V₂ V₃ V₄ V₅ V₆ = Set (MIPRE.SAT.Clause6 V₁ V₂ V₃ V₄ V₅ V₆)

def MIPRE.SAT.Cnf6.Sat {V₁ : Type u_1} {V₂ : Type u_2} {V₃ : Type u_3} {V₄ : Type u_4} {V₅ : Type u_5} {V₆ : Type u_6} (φ : Cnf6 V₁ V₂ V₃ V₄ V₅ V₆) (w₁ : V₁ → Bool) (w₂ : V₂ → Bool) (w₃ : V₃ → Bool) (w₄ : V₄ → Bool) (w₅ : V₅ → Bool) (w₆ : V₆ → Bool) : Prop

The six assignments satisfy every clause of φ.

Equations

• φ.Sat w₁ w₂ w₃ w₄ w₅ w₆ = ∀ c ∈ φ, MIPRE.SAT.Clause6.eval w₁ w₂ w₃ w₄ w₅ w₆ c = true

@[reducible, inline]

abbrev MIPRE.SAT.Clause6W (ℓa ℓb ℓc r : ℕ) : Type

The blocks of a decoupled clause of the describer: three windows, three witness blocks.

Equations

• MIPRE.SAT.Clause6W ℓa ℓb ℓc r = MIPRE.SAT.Clause6 (Fin (2 ^ ℓa)) (Fin (2 ^ ℓb)) (Fin (2 ^ ℓc)) (Fin (2 ^ r)) (Fin (2 ^ r)) (Fin (2 ^ r))

def MIPRE.SAT.clauseInput6 (ℓa ℓb ℓc r : ℕ) (c : Clause6W ℓa ℓb ℓc r) : List Bool

The input bits presenting a decoupled clause: the three window indices, the three witness indices, then the six signs.

Equations

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

@[simp]

theorem MIPRE.SAT.length_clauseInput6 (ℓa ℓb ℓc r : ℕ) (c : Clause6W ℓa ℓb ℓc r) : (clauseInput6 ℓa ℓb ℓc r c).length = ℓa + ℓb + ℓc + 3 * r + 6

def MIPRE.SAT.Circuit.formula6 (C : Circuit) (ℓa ℓb ℓc r : ℕ) : Cnf6 (Fin (2 ^ ℓa)) (Fin (2 ^ ℓb)) (Fin (2 ^ ℓc)) (Fin (2 ^ r)) (Fin (2 ^ r)) (Fin (2 ^ r))

The decoupled 6SAT formula that C succinctly describes.

Equations

• C.formula6 ℓa ℓb ℓc r = {c : MIPRE.SAT.Clause6 (Fin (2 ^ ℓa)) (Fin (2 ^ ℓb)) (Fin (2 ^ ℓc)) (Fin (2 ^ r)) (Fin (2 ^ r)) (Fin (2 ^ r)) | C.evalBits (MIPRE.SAT.clauseInput6 ℓa ℓb ℓc r c) = true}

The description

def MIPRE.SAT.Circuit.DescribesWindows (Cc : Circuit) (ℓa ℓb ℓc r : ℕ) (D : Decider) (n : ℕ) (x y : Cost.BitStr) (T : ℕ) : Prop

C succinctly describes the decider 𝒟 through three windows, on n, x, y and time T: three tables A, B, C complete to a satisfying 6-tuple of the described formula exactly when the decider accepts, within cost T, strings a, b of length at most T whose tape encodings start with A then C (for a) and with B (for b).

Equations

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

@[reducible, inline]

abbrev MIPRE.SAT.Desc6Input : Type

The input of the windowed describer: the three window lengths in unary, then the input of the 3SAT describer.

Equations

• MIPRE.SAT.Desc6Input = ((MIPRE.Cost.Unary × MIPRE.Cost.Unary × MIPRE.Cost.Unary) × MIPRE.SAT.DescInput)

structure MIPRE.SAT.WindowDescriber : Type

Succinct decoupled descriptions of deciders through three windows (prop:explicit-padded-succinct-deciders, in the form of slice P4g). An instance of this structure is the proposition.

• r₀ : ℕ → ℕ → ℕ

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

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

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

• describe : Cost.PolyTimeFun Desc6Input 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.r₀ T σ, self.s₀ n T Q σ)
• r₀_le : ∃ (c : ℕ), ∀ (T σ : ℕ), self.r₀ T σ ≤ c * (T.size + σ.size + 1)

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

• four_mul_le (T σ : ℕ) : 4 * T ≤ 2 ^ self.r₀ T σ

  4T ≤ 2^{r₀}: the witness blocks hold the tableau's two input regions.

• 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 (ua ub uc : Cost.Unary) (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) : (self.describe.toFun ((ua, ub, uc), (D, n, T, Q, σ), x, y)).inputs = List.length ua + List.length ub + List.length uc + 3 * self.r₀ T σ + 6

  The describer has ℓa + ℓb + ℓc + 3 r₀ + 6 inputs.

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

  The describer is a well-formed circuit.

• size_le (ua ub uc : Cost.Unary) (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) : Valid D n T Q σ x y → List.length ua ≤ self.r₀ T σ → List.length ub ≤ self.r₀ T σ → List.length uc ≤ self.r₀ T σ → (self.describe.toFun ((ua, ub, uc), (D, n, T, Q, σ), x, y)).size ≤ self.s₀ n T Q σ

  At most s₀ gates on valid inputs whose windows fit the witness indices.

• describes (ua ub uc : Cost.Unary) (D : Decider) (n T Q σ : ℕ) (x y : Cost.BitStr) : Valid D.prog n T Q σ x y → 2 ^ List.length ua + 2 ^ List.length uc ≤ 2 * T → 2 ^ List.length ub ≤ 2 * T → List.length ua ≤ self.r₀ T σ → List.length ub ≤ self.r₀ T σ → List.length uc ≤ self.r₀ T σ → (self.describe.toFun ((ua, ub, uc), (D.prog, n, T, Q, σ), x, y)).DescribesWindows (List.length ua) (List.length ub) (List.length uc) (self.r₀ T σ) D n x y T

  The describer describes the decider through the windows, when the windows fit the two input regions of the tableau and the witness indices.