The decoupled describer, and the clauses it describes

The describer of lem:decoupled-5sat: the 3SAT describer of thm:succinct-sat, its inputs renamed into the five-block layout, in disjunction with the link formula of Link.lean, all flattened once to a circuit. mem_formula5_iff is the bridge — 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 eight link conditions (planning/decoupled-5sat.md, A1c).

Where the 3SAT describer's inputs go

def MIPRE.TM.CookLevin.Desc.rho (ℓ r k : ℕ) : ℕ

The renaming: the 3r index bits of the 3SAT describer sit after the two answer indices, and its three signs after the two answer signs.

Equations

• MIPRE.TM.CookLevin.Desc.rho ℓ r k = if k < 3 * r then k + 2 * ℓ else k + 2 * ℓ + 2

def MIPRE.TM.CookLevin.Desc.lastThree {ℓ r : ℕ} (c : SAT.Clause5 (Fin (2 ^ ℓ)) (Fin (2 ^ ℓ)) (Fin (2 ^ r)) (Fin (2 ^ r)) (Fin (2 ^ r))) : SAT.Clause3 (Fin (2 ^ r))

The 3-clause of the last three literals of a decoupled clause.

Equations

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

The renaming reads the right bits

theorem MIPRE.TM.CookLevin.Desc.getD_append_right {α : Type u_1} (pre u : List α) (d : α) (t : ℕ) : (pre ++ u).getD (pre.length + t) d = u.getD t d

theorem MIPRE.TM.CookLevin.Desc.drop_two' {ℓ r : ℕ} (c : SAT.Clause5 (Fin (2 ^ ℓ)) (Fin (2 ^ ℓ)) (Fin (2 ^ r)) (Fin (2 ^ r)) (Fin (2 ^ r))) : List.drop (2 * ℓ) (SAT.clauseInput5 ℓ r c) = SAT.bitsOfNat r ↑c.l₃.var ++ SAT.bitsOfNat r ↑c.l₄.var ++ SAT.bitsOfNat r ↑c.l₅.var ++ sgList c

theorem MIPRE.TM.CookLevin.Desc.getD_rho {ℓ r : ℕ} (c : SAT.Clause5 (Fin (2 ^ ℓ)) (Fin (2 ^ ℓ)) (Fin (2 ^ r)) (Fin (2 ^ r)) (Fin (2 ^ r))) {k : ℕ} (hk : k < 3 * r + 3) : (SAT.clauseInput5 ℓ r c).getD (rho ℓ r k) false = (SAT.clauseInput r (lastThree c)).getD k false

The renaming reads the 3SAT describer's clause off the five-block input.

The shifted candidate

The 3SAT describer's inputs cannot be renamed into the five-block layout by a program: the renaming is k ↦ k + 2ℓ below 3r and k ↦ k + 2ℓ + 2 above, and deciding which needs a comparison of two binary numbers, which the ambient model does not have. So the describer is rebuilt on the shifted layout instead — the candidate reads its three field records at the bases 2ℓ, 2ℓ + r, 2ℓ + 2r and its three signs at 2ℓ + 3r + 2, 3, 4. That is cheaper in both directions: every offset is unary, so the program is the one S3 already has, and the correctness goes straight through eval_tableauPlusF instead of through the renaming.

theorem MIPRE.TM.CookLevin.Desc.ibOf_shift {ℓ m b : ℕ} (c : SAT.Clause5 (Fin (2 ^ ℓ)) (Fin (2 ^ ℓ)) (Fin (2 ^ m)) (Fin (2 ^ m)) (Fin (2 ^ m))) (h : b + m ≤ 3 * m) : (ibOf (2 * ℓ + b) m fun (i : ℕ) => (SAT.clauseInput5 ℓ m c).getD i false) = ibOf b m fun (i : ℕ) => (SAT.clauseInput m (lastThree c)).getD i false

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

noncomputable def MIPRE.TM.CookLevin.Desc.candOf5 (ℓ e T : ℕ) : CandF

The candidate of the decoupled describer: the three field records at the shifted bases and the three auxiliary signs.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.candOf5_lengths (ℓ e T : ℕ) : CandF.Lengths e Gc (candOf5 ℓ e T)

theorem MIPRE.TM.CookLevin.Desc.candOf5_inputsLt (ℓ e T : ℕ) : CandF.InputsLt (2 * ℓ + 3 * mOf e Gc + 5) (candOf5 ℓ e T)

theorem MIPRE.TM.CookLevin.Desc.evalCand_candOf5 (ℓ e T : ℕ) (c : SAT.Clause5 (Fin (2 ^ ℓ)) (Fin (2 ^ ℓ)) (Fin (2 ^ mOf e Gc)) (Fin (2 ^ mOf e Gc)) (Fin (2 ^ mOf e Gc))) (hT : T ≤ Sof e) : (evalCand (candOf5 ℓ e T) fun (i : ℕ) => (SAT.clauseInput5 ℓ (mOf e Gc) c).getD i false) = candOfClause e T (lastThree c)

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

The describer

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

The tableau half of the 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.descFml5 (ℓ T e : ℕ) (D : Cost.Prog) (n : ℕ) (x y : Cost.BitStr) : SAT.Fml

The formula of the decoupled describer.

Equations

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

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

The decoupled describer circuit: the flattening of descFml5 on 2ℓ + 3r + 5 inputs.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.descCirc5_inputs (ℓ T e : ℕ) (D : Cost.Prog) (n : ℕ) (x y : Cost.BitStr) : (descCirc5 ℓ T e D n x y).inputs = 2 * ℓ + 3 * mOf e Gc + 5

theorem MIPRE.TM.CookLevin.Desc.descFml5_inputsLt (ℓ T e : ℕ) (D : Cost.Prog) (n : ℕ) (x y : Cost.BitStr) (hℓr : ℓ ≤ mOf e Gc) : SAT.Fml.InputsLt (2 * ℓ + 3 * mOf e Gc + 5) (descFml5 ℓ T e D n x y)

theorem MIPRE.TM.CookLevin.Desc.descCirc5_wellFormed (ℓ T e : ℕ) (D : Cost.Prog) (n : ℕ) (x y : Cost.BitStr) (hℓr : ℓ ≤ mOf e Gc) : (descCirc5 ℓ T e D n x y).WellFormed

theorem MIPRE.TM.CookLevin.Desc.mem_formula5_iff (ℓ T e : ℕ) (D : Cost.Prog) (n : ℕ) (x y : Cost.BitStr) (hℓr : ℓ ≤ mOf e Gc) (hr : 1 ≤ mOf e Gc) (hT2 : 2 * T < 2 ^ mOf e Gc) (hT : T ≤ Sof e) (hlen : FixedLen e D n T x y) (hTm : T + 3 < 2 ^ W e) (c : SAT.Clause5 (Fin (2 ^ ℓ)) (Fin (2 ^ ℓ)) (Fin (2 ^ mOf e Gc)) (Fin (2 ^ mOf e Gc)) (Fin (2 ^ mOf e Gc))) : c ∈ (descCirc5 ℓ T e D n x y).formula5 ℓ (mOf e Gc) ↔ lastThree c ∈ (descCirc e T D n x y).formula3 (mOf e Gc) ∨ Link ℓ (mOf e Gc) T c

What the decoupled 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 eight link conditions.

What a satisfying five-tuple is

Following the paper: for a fixed triple of indices the three signs of the other blocks range over all of {0,1}³, so a decoupled clause is satisfied exactly when the literals of the blocks the condition constrains are. Rows 8 and 9 therefore read as equalities of whole blocks, and rows 2 and 3 as equalities of single bits.

def MIPRE.TM.CookLevin.Desc.zeroIdx (k : ℕ) : Fin (2 ^ k)

The index 0 of a block.

Equations

• MIPRE.TM.CookLevin.Desc.zeroIdx k = ⟨0, ⋯⟩

def MIPRE.TM.CookLevin.Desc.offLit {k : ℕ} (w : Fin (2 ^ k) → Bool) : SAT.Lit (Fin (2 ^ k))

A literal of a block that the given assignment falsifies.

Equations

• MIPRE.TM.CookLevin.Desc.offLit w = { var := MIPRE.TM.CookLevin.Desc.zeroIdx k, pos := !w (MIPRE.TM.CookLevin.Desc.zeroIdx k) }

@[simp]

theorem MIPRE.TM.CookLevin.Desc.offLit_eval {k : ℕ} (w : Fin (2 ^ k) → Bool) : SAT.Lit.eval w (offLit w) = false

theorem MIPRE.TM.CookLevin.Desc.eq_of_lit_or {V : Type u_1} {W : Type u_2} (u : V → Bool) (v : W → Bool) (i : V) (j : W) (h : ∀ (o : Bool), (SAT.Lit.eval u { var := i, pos := o } || SAT.Lit.eval v { var := j, pos := !o }) = true) : u i = v j

Two literals of opposite sign force the two bits to agree.

theorem MIPRE.TM.CookLevin.Desc.eq_of_lit {V : Type u_1} (u : V → Bool) (i : V) (o : Bool) (h : SAT.Lit.eval u { var := i, pos := o } = true) : u i = o

One literal forced true.

def MIPRE.TM.CookLevin.Desc.Tri {r : ℕ} (φ : SAT.Cnf3 (Fin (2 ^ r))) (w₁ w₂ w₃ : Fin (2 ^ r) → Bool) : Prop

The three-block half: the described 3SAT formula on the three auxiliary blocks.

Equations

• MIPRE.TM.CookLevin.Desc.Tri φ w₁ w₂ w₃ = ∀ c ∈ φ, (MIPRE.SAT.Lit.eval w₁ c.l₁ || MIPRE.SAT.Lit.eval w₂ c.l₂ || MIPRE.SAT.Lit.eval w₃ c.l₃) = true

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

The link half: what rows 2 to 9 force.

• aLow (i : Fin (2 ^ ℓ)) (j : Fin (2 ^ r)) : ↑i < 2 * T → ↑i = ↑j → a i = w₁ j
• bLow (i : Fin (2 ^ ℓ)) (j : Fin (2 ^ r)) : ↑i < 2 * T → ↑j = ↑i + 2 * T → b i = w₁ j
• aPad (i : Fin (2 ^ ℓ)) : ¬↑i < 2 * T → a i = decide (↑i % 2 = 0)
• bPad (i : Fin (2 ^ ℓ)) : ¬↑i < 2 * T → b i = decide (↑i % 2 = 0)
• 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_formula5_iff (ℓ T e : ℕ) (D : Cost.Prog) (n : ℕ) (x y : Cost.BitStr) (hℓr : ℓ ≤ mOf e Gc) (hr : 1 ≤ mOf e Gc) (hT2 : 2 * T < 2 ^ mOf e Gc) (hT : T ≤ Sof e) (hlen : FixedLen e D n T x y) (hTm : T + 3 < 2 ^ W e) (a b : Fin (2 ^ ℓ) → Bool) (w₁ w₂ w₃ : Fin (2 ^ mOf e Gc) → Bool) : ((descCirc5 ℓ T e D n x y).formula5 ℓ (mOf e Gc)).Sat a b w₁ w₂ w₃ ↔ Tri ((descCirc e T D n x y).formula3 (mOf e Gc)) w₁ w₂ w₃ ∧ LinkSat ℓ (mOf e Gc) T a b w₁ w₂ w₃

The two halves of satisfaction.

The padding of an answer block

theorem MIPRE.TM.CookLevin.Desc.tapeBits_of_ge {s : Cost.BitStr} {T p : ℕ} (hs : List.length s ≤ T) (hp : 2 * T ≤ p) : SAT.tapeBits s p = decide (p % 2 = 0)

Past twice the length of the string, a tape block is the blank cell 10: true at even positions and false at odd ones. This is the parity the audit campaign repaired, and it is what rows 4 to 7 assert.

The describer describes the decider

theorem MIPRE.TM.CookLevin.Desc.describes5 (𝒟 : Decider) (ℓ T e n : ℕ) (x y : Cost.BitStr) (hℓ : 2 * T ≤ 2 ^ ℓ) (hℓr : ℓ ≤ mOf e Gc) (hr : 1 ≤ 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) : (descCirc5 ℓ T e 𝒟.prog n x y).DescribesDecider ℓ (mOf e Gc) 𝒟 n x y T

The decoupled describer describes the decider (lem:decoupled-5sat, the description clause).