Documentation

MIPRE.TM.CookLevin.Link6

The link clauses of the windowed describer #

The windowed describer of MIPRE.SAT.WindowDescriber (slice P4g of the Aldous–Lyons track) ties three input blocks to the first 4T variables of three witness blocks, which carry the tableau of thm:succinct-sat: the first and third blocks to the consecutive windows [0, 2^ℓa) and [2^ℓa, 2^ℓa + 2^ℓc) of the tape encoding of the first answer, the second to the window [2T, 2T + 2^ℓb) of that of the second, and it makes the three witness blocks agree. There are five rows, the analogue of rows 2, 3, 8 and 9 of Link.lean; nothing pins the tape outside the windows, which the decider's own checks of its input lengths do.

Link6 is the disjunction of the five conditions on a decoded clause and link6Fml the formula that decides it on the ℓa + ℓb + ℓc + 3r + 6 input bits, with eval_link6Fml their equivalence. Every comparison is made at width r, the window indices zero-padded.

The input layout #

def MIPRE.TM.CookLevin.Desc.wOff (ℓa ℓb ℓc : ℕ) :

The offset of the three witness indices.

Equations

MIPRE.TM.CookLevin.Desc.wOff ℓa ℓb ℓc = ℓa + ℓb + ℓc

Instances For

def MIPRE.TM.CookLevin.Desc.sgOff6 (ℓa ℓb ℓc r : ℕ) :

The offset of the six signs.

Equations

MIPRE.TM.CookLevin.Desc.sgOff6 ℓa ℓb ℓc r = MIPRE.TM.CookLevin.Desc.wOff ℓa ℓb ℓc + 3 * r

Instances For

def MIPRE.TM.CookLevin.Desc.k₁F (ℓa r : ℕ) :

The three window indices, zero-padded to r bits, and the three witness indices.

Equations

MIPRE.TM.CookLevin.Desc.k₁F ℓa r = MIPRE.SAT.Fml.padTo r (MIPRE.SAT.Fml.field 0 ℓa)

Instances For

def MIPRE.TM.CookLevin.Desc.k₂F (ℓa ℓb r : ℕ) :

Equations

MIPRE.TM.CookLevin.Desc.k₂F ℓa ℓb r = MIPRE.SAT.Fml.padTo r (MIPRE.SAT.Fml.field ℓa ℓb)

Instances For

def MIPRE.TM.CookLevin.Desc.k₃F (ℓa ℓb ℓc r : ℕ) :

Equations

MIPRE.TM.CookLevin.Desc.k₃F ℓa ℓb ℓc r = MIPRE.SAT.Fml.padTo r (MIPRE.SAT.Fml.field (ℓa + ℓb) ℓc)

Instances For

def MIPRE.TM.CookLevin.Desc.k₄F (ℓa ℓb ℓc r : ℕ) :

Equations

MIPRE.TM.CookLevin.Desc.k₄F ℓa ℓb ℓc r = MIPRE.SAT.Fml.field (MIPRE.TM.CookLevin.Desc.wOff ℓa ℓb ℓc) r

Instances For

def MIPRE.TM.CookLevin.Desc.k₅F (ℓa ℓb ℓc r : ℕ) :

Equations

MIPRE.TM.CookLevin.Desc.k₅F ℓa ℓb ℓc r = MIPRE.SAT.Fml.field (MIPRE.TM.CookLevin.Desc.wOff ℓa ℓb ℓc + r) r

Instances For

def MIPRE.TM.CookLevin.Desc.k₆F (ℓa ℓb ℓc r : ℕ) :

Equations

MIPRE.TM.CookLevin.Desc.k₆F ℓa ℓb ℓc r = MIPRE.SAT.Fml.field (MIPRE.TM.CookLevin.Desc.wOff ℓa ℓb ℓc + 2 * r) r

Instances For

def MIPRE.TM.CookLevin.Desc.t₀F (ℓa ℓb ℓc r k : ℕ) :

The k-th of the six signs.

Equations

MIPRE.TM.CookLevin.Desc.t₀F ℓa ℓb ℓc r k = MIPRE.SAT.Fml.inp (MIPRE.TM.CookLevin.Desc.sgOff6 ℓa ℓb ℓc r + k)

Instances For

theorem MIPRE.TM.CookLevin.Desc.length_k₁F (ℓa r : ℕ) (h : ℓa ≤ r) :

(k₁F ℓa r).length = r

theorem MIPRE.TM.CookLevin.Desc.length_k₂F (ℓa ℓb r : ℕ) (h : ℓb ≤ r) :

(k₂F ℓa ℓb r).length = r

theorem MIPRE.TM.CookLevin.Desc.length_k₃F (ℓa ℓb ℓc r : ℕ) (h : ℓc ≤ r) :

(k₃F ℓa ℓb ℓc r).length = r

@[simp]

theorem MIPRE.TM.CookLevin.Desc.length_k₄F (ℓa ℓb ℓc r : ℕ) :

(k₄F ℓa ℓb ℓc r).length = r

@[simp]

theorem MIPRE.TM.CookLevin.Desc.length_k₅F (ℓa ℓb ℓc r : ℕ) :

(k₅F ℓa ℓb ℓc r).length = r

@[simp]

theorem MIPRE.TM.CookLevin.Desc.length_k₆F (ℓa ℓb ℓc r : ℕ) :

(k₆F ℓa ℓb ℓc r).length = r

The five conditions #

def MIPRE.TM.CookLevin.Desc.Link6 (ℓa ℓb ℓc r T : ℕ) (c : SAT.Clause6W ℓa ℓb ℓc r) :

The link conditions on a decoupled clause of the windowed describer.

Equations

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

Instances For

def MIPRE.TM.CookLevin.Desc.link6Fml (ℓa ℓb ℓc r T : ℕ) :

The formula deciding Link6 on the ℓa + ℓb + ℓc + 3r + 6 input bits.

Equations

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

Instances For

theorem MIPRE.TM.CookLevin.Desc.InputsLt.link6Fml (ℓa ℓb ℓc r T : ℕ) :

SAT.Fml.InputsLt (ℓa + ℓb + ℓc + 3 * r + 6) (Desc.link6Fml ℓa ℓb ℓc r T)

The slices of a clause's input #

def MIPRE.TM.CookLevin.Desc.sgList6 {ℓa ℓb ℓc r : ℕ} (c : SAT.Clause6W ℓa ℓb ℓc r) :

The six signs, as a list.

Equations

MIPRE.TM.CookLevin.Desc.sgList6 c = [c.l₁.pos, c.l₂.pos, c.l₃.pos, c.l₄.pos, c.l₅.pos, c.l₆.pos]

Instances For

theorem MIPRE.TM.CookLevin.Desc.clauseInput6_eq {ℓa ℓb ℓc r : ℕ} (c : SAT.Clause6W ℓa ℓb ℓc r) :

SAT.clauseInput6 ℓa ℓb ℓc r c = SAT.bitsOfNat ℓa ↑c.l₁.var ++ (SAT.bitsOfNat ℓb ↑c.l₂.var ++ (SAT.bitsOfNat ℓc ↑c.l₃.var ++ (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.drop6_one {ℓa ℓb ℓc r : ℕ} (c : SAT.Clause6W ℓa ℓb ℓc r) :

List.drop ℓa (SAT.clauseInput6 ℓa ℓb ℓc r c) = SAT.bitsOfNat ℓb ↑c.l₂.var ++ (SAT.bitsOfNat ℓc ↑c.l₃.var ++ (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.drop6_two {ℓa ℓb ℓc r : ℕ} (c : SAT.Clause6W ℓa ℓb ℓc r) :

List.drop (ℓa + ℓb) (SAT.clauseInput6 ℓa ℓb ℓc r c) = SAT.bitsOfNat ℓc ↑c.l₃.var ++ (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.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.drop6_four {ℓa ℓb ℓc r : ℕ} (c : SAT.Clause6W ℓa ℓb ℓc r) :

List.drop (wOff ℓa ℓb ℓc + r) (SAT.clauseInput6 ℓa ℓb ℓc r c) = SAT.bitsOfNat r ↑c.l₅.var ++ (SAT.bitsOfNat r ↑c.l₆.var ++ sgList6 c)

theorem MIPRE.TM.CookLevin.Desc.drop6_five {ℓa ℓb ℓc r : ℕ} (c : SAT.Clause6W ℓa ℓb ℓc r) :

List.drop (wOff ℓa ℓb ℓc + 2 * r) (SAT.clauseInput6 ℓa ℓb ℓc r c) = SAT.bitsOfNat r ↑c.l₆.var ++ sgList6 c

theorem MIPRE.TM.CookLevin.Desc.drop6_signs {ℓa ℓb ℓc r : ℕ} (c : SAT.Clause6W ℓa ℓb ℓc r) :

List.drop (sgOff6 ℓa ℓb ℓc r) (SAT.clauseInput6 ℓa ℓb ℓc r c) = sgList6 c

theorem MIPRE.TM.CookLevin.Desc.val_k₁F {ℓa ℓb ℓc r : ℕ} (c : SAT.Clause6W ℓa ℓb ℓc r) :

(SAT.Fml.val (k₁F ℓa r) fun (i : ℕ) => (SAT.clauseInput6 ℓa ℓb ℓc r c).getD i false) = ↑c.l₁.var

theorem MIPRE.TM.CookLevin.Desc.val_k₂F {ℓa ℓb ℓc r : ℕ} (c : SAT.Clause6W ℓa ℓb ℓc r) :

(SAT.Fml.val (k₂F ℓa ℓb r) fun (i : ℕ) => (SAT.clauseInput6 ℓa ℓb ℓc r c).getD i false) = ↑c.l₂.var

theorem MIPRE.TM.CookLevin.Desc.val_k₃F {ℓa ℓb ℓc r : ℕ} (c : SAT.Clause6W ℓa ℓb ℓc r) :

(SAT.Fml.val (k₃F ℓa ℓb ℓc r) fun (i : ℕ) => (SAT.clauseInput6 ℓa ℓb ℓc r c).getD i false) = ↑c.l₃.var

theorem MIPRE.TM.CookLevin.Desc.val_k₄F {ℓa ℓb ℓc r : ℕ} (c : SAT.Clause6W ℓa ℓb ℓc r) :

(SAT.Fml.val (k₄F ℓa ℓb ℓc r) fun (i : ℕ) => (SAT.clauseInput6 ℓa ℓb ℓc r c).getD i false) = ↑c.l₄.var

theorem MIPRE.TM.CookLevin.Desc.val_k₅F {ℓa ℓb ℓc r : ℕ} (c : SAT.Clause6W ℓa ℓb ℓc r) :

(SAT.Fml.val (k₅F ℓa ℓb ℓc r) fun (i : ℕ) => (SAT.clauseInput6 ℓa ℓb ℓc r c).getD i false) = ↑c.l₅.var

theorem MIPRE.TM.CookLevin.Desc.val_k₆F {ℓa ℓb ℓc r : ℕ} (c : SAT.Clause6W ℓa ℓb ℓc r) :

(SAT.Fml.val (k₆F ℓa ℓb ℓc r) fun (i : ℕ) => (SAT.clauseInput6 ℓa ℓb ℓc r c).getD i false) = ↑c.l₆.var

theorem MIPRE.TM.CookLevin.Desc.eval_t₀F {ℓa ℓb ℓc r : ℕ} (c : SAT.Clause6W ℓa ℓb ℓc r) (k : ℕ) :

SAT.Fml.eval (fun (i : ℕ) => (SAT.clauseInput6 ℓa ℓb ℓc r c).getD i false) (t₀F ℓa ℓb ℓc r k) = List.getD (sgList6 c) k false

The formula decides the conditions #

theorem MIPRE.TM.CookLevin.Desc.eval_link6Fml {ℓa ℓb ℓc r T : ℕ} (ha : ℓa ≤ r) (hb : ℓb ≤ r) (hc : ℓc ≤ r) (hT : 2 * T < 2 ^ r) (hTa : 2 ^ ℓa < 2 ^ r) (c : SAT.Clause6W ℓa ℓb ℓc r) :

SAT.Fml.eval (fun (i : ℕ) => (SAT.clauseInput6 ℓa ℓb ℓc r c).getD i false) (link6Fml ℓa ℓb ℓc r T) = true ↔ Link6 ℓa ℓb ℓc r T c

The link formula decides the link conditions.