The windowed describer, and the clauses it describes

The describer of MIPRE.SAT.WindowDescriber (slice P4g of the Aldous–Lyons track): the 3SAT describer of thm:succinct-sat rebuilt on the six-block layout — its three field records read at the bases P, P + r, P + 2r with P = ℓa + ℓb + ℓc, its three signs after the three window signs — in disjunction with the link formula of Link6.lean, all flattened once to a circuit, exactly as descCirc5 is built for two answer blocks (Decoupled.lean). mem_formula6_iff is the bridge, sat_formula6_iff reads what a satisfying 6-tuple is, and describes6 is the description: three tables complete to a satisfying 6-tuple exactly when they are the windows of the tape encodings of strings the decider accepts within T.

The 3SAT describer's clause inside a six-block clause

def MIPRE.TM.CookLevin.Desc.lastThree6 {ℓa ℓb ℓc r : ℕ} (c : SAT.Clause6W ℓa ℓb ℓc r) : SAT.Clause3 (Fin (2 ^ r))

The 3-clause of the last three literals of a six-block clause.

Equations

• MIPRE.TM.CookLevin.Desc.lastThree6 c = { l₁ := c.l₄, l₂ := c.l₅, l₃ := c.l₆ }

theorem MIPRE.TM.CookLevin.Desc.drop6_three' {ℓa ℓb ℓc r : ℕ} (c : SAT.Clause6W ℓa ℓb ℓc r) : List.drop (wOff ℓa ℓb ℓc) (SAT.clauseInput6 ℓa ℓb ℓc r c) = SAT.bitsOfNat r ↑c.l₄.var ++ SAT.bitsOfNat r ↑c.l₅.var ++ SAT.bitsOfNat r ↑c.l₆.var ++ sgList6 c

theorem MIPRE.TM.CookLevin.Desc.getD_shift6 {ℓa ℓb ℓc r : ℕ} (c : SAT.Clause6W ℓa ℓb ℓc r) {k : ℕ} (hk : k < 3 * r) : (SAT.clauseInput6 ℓa ℓb ℓc r c).getD (wOff ℓa ℓb ℓc + k) false = (SAT.clauseInput r (lastThree6 c)).getD k false

The six-block input at the witness offset reads the 3SAT describer's indices.

theorem MIPRE.TM.CookLevin.Desc.ibOf_shift6 {ℓa ℓb ℓc m b : ℕ} (c : SAT.Clause6W ℓa ℓb ℓc m) (h : b + m ≤ 3 * m) : (ibOf (wOff ℓa ℓb ℓc + b) m fun (i : ℕ) => (SAT.clauseInput6 ℓa ℓb ℓc m c).getD i false) = ibOf b m fun (i : ℕ) => (SAT.clauseInput m (lastThree6 c)).getD i false

A slice of the six-block input at a shifted base is the 3SAT describer's own slice.

The shifted candidate

noncomputable def MIPRE.TM.CookLevin.Desc.candOf6 (P e T : ℕ) : CandF

The candidate of the windowed describer: the three field records at the shifted bases and the three witness signs.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.candOf6_lengths (P e T : ℕ) : CandF.Lengths e Gc (candOf6 P e T)

theorem MIPRE.TM.CookLevin.Desc.candOf6_inputsLt (P e T : ℕ) : CandF.InputsLt (P + 3 * mOf e Gc + 6) (candOf6 P e T)

theorem MIPRE.TM.CookLevin.Desc.evalCand_candOf6 (ℓa ℓb ℓc e T : ℕ) (c : SAT.Clause6W ℓa ℓb ℓc (mOf e Gc)) (hT : T ≤ Sof e) : (evalCand (candOf6 (wOff ℓa ℓb ℓc) e T) fun (i : ℕ) => (SAT.clauseInput6 ℓa ℓb ℓc (mOf e Gc) c).getD i false) = candOfClause e T (lastThree6 c)

The shifted candidate reads the 3SAT describer's clause.

The describer

noncomputable def MIPRE.TM.CookLevin.Desc.descBody6 (P T e : ℕ) (D : Cost.Prog) (n : ℕ) (x y : Cost.BitStr) : SAT.Fml

The tableau half of the windowed describer's formula, on the shifted candidate.

Equations

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

noncomputable def MIPRE.TM.CookLevin.Desc.descFml6 (ℓa ℓb ℓc T e : ℕ) (D : Cost.Prog) (n : ℕ) (x y : Cost.BitStr) : SAT.Fml

The formula of the windowed describer.

Equations

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

noncomputable def MIPRE.TM.CookLevin.Desc.descCirc6 (ℓa ℓb ℓc T e : ℕ) (D : Cost.Prog) (n : ℕ) (x y : Cost.BitStr) : SAT.Circuit

The windowed describer circuit: the flattening of descFml6 on ℓa + ℓb + ℓc + 3r + 6 inputs.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.descCirc6_inputs (ℓa ℓb ℓc T e : ℕ) (D : Cost.Prog) (n : ℕ) (x y : Cost.BitStr) : (descCirc6 ℓa ℓb ℓc T e D n x y).inputs = ℓa + ℓb + ℓc + 3 * mOf e Gc + 6

theorem MIPRE.TM.CookLevin.Desc.descFml6_inputsLt (ℓa ℓb ℓc T e : ℕ) (D : Cost.Prog) (n : ℕ) (x y : Cost.BitStr) : SAT.Fml.InputsLt (ℓa + ℓb + ℓc + 3 * mOf e Gc + 6) (descFml6 ℓa ℓb ℓc T e D n x y)

theorem MIPRE.TM.CookLevin.Desc.descCirc6_wellFormed (ℓa ℓb ℓc T e : ℕ) (D : Cost.Prog) (n : ℕ) (x y : Cost.BitStr) : (descCirc6 ℓa ℓb ℓc T e D n x y).WellFormed

theorem MIPRE.TM.CookLevin.Desc.mem_formula6_iff (ℓa ℓb ℓc T e : ℕ) (D : Cost.Prog) (n : ℕ) (x y : Cost.BitStr) (ha : ℓa ≤ mOf e Gc) (hb : ℓb ≤ mOf e Gc) (hc : ℓc ≤ mOf e Gc) (hT2 : 2 * T < 2 ^ mOf e Gc) (hTa : 2 ^ ℓa < 2 ^ mOf e Gc) (hT : T ≤ Sof e) (hlen : FixedLen e D n T x y) (hTm : T + 3 < 2 ^ W e) (c : SAT.Clause6W ℓa ℓb ℓc (mOf e Gc)) : c ∈ (descCirc6 ℓa ℓb ℓc T e D n x y).formula6 ℓa ℓb ℓc (mOf e Gc) ↔ lastThree6 c ∈ (descCirc e T D n x y).formula3 (mOf e Gc) ∨ Link6 ℓa ℓb ℓc (mOf e Gc) T c

What the windowed describer accepts: a clause is accepted exactly when the 3-clause of its last three literals is accepted by the 3SAT describer, or the clause satisfies one of the five link conditions.

What a satisfying 6-tuple is

structure MIPRE.TM.CookLevin.Desc.LinkSat6 (ℓa ℓb ℓc r T : ℕ) (A : Fin (2 ^ ℓa) → Bool) (B : Fin (2 ^ ℓb) → Bool) (C : Fin (2 ^ ℓc) → Bool) (w₁ w₂ w₃ : Fin (2 ^ r) → Bool) : Prop

The link half: what the five rows force.

• aWin (i : Fin (2 ^ ℓa)) (j : Fin (2 ^ r)) : ↑j = ↑i → A i = w₁ j
• bWin (i : Fin (2 ^ ℓb)) (j : Fin (2 ^ r)) : ↑j = ↑i + 2 * T → B i = w₁ j
• cWin (i : Fin (2 ^ ℓc)) (j : Fin (2 ^ r)) : ↑j = ↑i + 2 ^ ℓa → C i = w₁ j
• w12 (i j : Fin (2 ^ r)) : ↑i = ↑j → w₁ i = w₂ j
• w23 (i j : Fin (2 ^ r)) : ↑i = ↑j → w₂ i = w₃ j

theorem MIPRE.TM.CookLevin.Desc.sat_formula6_iff (ℓa ℓb ℓc T e : ℕ) (D : Cost.Prog) (n : ℕ) (x y : Cost.BitStr) (ha : ℓa ≤ mOf e Gc) (hb : ℓb ≤ mOf e Gc) (hc : ℓc ≤ mOf e Gc) (hT2 : 2 * T < 2 ^ mOf e Gc) (hTa : 2 ^ ℓa < 2 ^ mOf e Gc) (hT : T ≤ Sof e) (hlen : FixedLen e D n T x y) (hTm : T + 3 < 2 ^ W e) (A : Fin (2 ^ ℓa) → Bool) (B : Fin (2 ^ ℓb) → Bool) (C : Fin (2 ^ ℓc) → Bool) (w₁ w₂ w₃ : Fin (2 ^ mOf e Gc) → Bool) : ((descCirc6 ℓa ℓb ℓc T e D n x y).formula6 ℓa ℓb ℓc (mOf e Gc)).Sat A B C w₁ w₂ w₃ ↔ Tri ((descCirc e T D n x y).formula3 (mOf e Gc)) w₁ w₂ w₃ ∧ LinkSat6 ℓa ℓb ℓc (mOf e Gc) T A B C w₁ w₂ w₃

The two halves of satisfaction.

The describer describes the decider through the windows

theorem MIPRE.TM.CookLevin.Desc.describes6 (𝒟 : Decider) (ℓa ℓb ℓc T e n : ℕ) (x y : Cost.BitStr) (hwac : 2 ^ ℓa + 2 ^ ℓc ≤ 2 * T) (hwb : 2 ^ ℓb ≤ 2 * T) (ha : ℓa ≤ mOf e Gc) (hb : ℓb ≤ mOf e Gc) (hc : ℓc ≤ mOf e Gc) (h4T : 4 * T ≤ 2 ^ mOf e Gc) (hTle : T ≤ Sof e) (hlen : FixedLen e 𝒟.prog n T x y) (hTm : T + 3 < 2 ^ W e) (hrb : ∀ (ap bp : Cost.BitStr), List.length ap ≤ T → List.length bp ≤ T → Interp.runBound 𝒟.prog n x y ap bp T ≤ Sof e) : (descCirc6 ℓa ℓb ℓc T e 𝒟.prog n x y).DescribesWindows ℓa ℓb ℓc (mOf e Gc) 𝒟 n x y T

The windowed describer describes the decider (slice P4g, the description clause).