Padding decoupled descriptions

The semantic content of prop:exciting-padding-prop in answer_reduction.tex. The original clauses are embedded in the larger five blocks. Additional clauses force both answer tails to be blank tapes; the three auxiliary tails are free. In particular, the conclusion preserves Circuit.DescribesDecider, which specifies every answer bit, rather than merely preserving the accepted answer prefixes. The circuit construction and its running time are separate obligations.

def MIPRE.SAT.Clause5.map {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} {E : Type u_5} {A' : Type u_6} {B' : Type u_7} {C' : Type u_8} {D' : Type u_9} {E' : Type u_10} (f₁ : A → A') (f₂ : B → B') (f₃ : C → C') (f₄ : D → D') (f₅ : E → E') (c : Clause5 A B C D E) : Clause5 A' B' C' D' E'

Rename the variables in each of the five separate blocks.

Equations

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

@[simp]

theorem MIPRE.SAT.Clause5.eval_map {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} {E : Type u_5} {A' : Type u_6} {B' : Type u_7} {C' : Type u_8} {D' : Type u_9} {E' : Type u_10} (f₁ : A → A') (f₂ : B → B') (f₃ : C → C') (f₄ : D → D') (f₅ : E → E') (c : Clause5 A B C D E) (w₁ : A' → Bool) (w₂ : B' → Bool) (w₃ : C' → Bool) (w₄ : D' → Bool) (w₅ : E' → Bool) : eval w₁ w₂ w₃ w₄ w₅ (map f₁ f₂ f₃ f₄ f₅ c) = eval (w₁ ∘ f₁) (w₂ ∘ f₂) (w₃ ∘ f₃) (w₄ ∘ f₄) (w₅ ∘ f₅) c

def MIPRE.SAT.Cnf5.blockInclusion {n m : ℕ} (h : n ≤ m) : Fin (2 ^ n) → Fin (2 ^ m)

The inclusion of an old block into a larger one.

Equations

• MIPRE.SAT.Cnf5.blockInclusion h = Fin.castLE ⋯

def MIPRE.SAT.Cnf5.extendBlock {n m : ℕ} (w : Fin (2 ^ n) → Bool) : Fin (2 ^ m) → Bool

Extend a block arbitrarily by false; only the three auxiliary blocks use this.

Equations

• MIPRE.SAT.Cnf5.extendBlock w i = if h : ↑i < 2 ^ n then w ⟨↑i, h⟩ else false

@[simp]

theorem MIPRE.SAT.Cnf5.extendBlock_inclusion {n m : ℕ} (h : n ≤ m) (w : Fin (2 ^ n) → Bool) : extendBlock w ∘ blockInclusion h = w

def MIPRE.SAT.Cnf5.pad {ℓ r ℓ' r' : ℕ} (hℓ : ℓ ≤ ℓ') (hr : r ≤ r') (φ : Cnf5 (Fin (2 ^ ℓ)) (Fin (2 ^ ℓ)) (Fin (2 ^ r)) (Fin (2 ^ r)) (Fin (2 ^ r))) : Cnf5 (Fin (2 ^ ℓ')) (Fin (2 ^ ℓ')) (Fin (2 ^ r')) (Fin (2 ^ r')) (Fin (2 ^ r'))

Embed the original clauses and force the two answer tails to contain blanks.

Equations

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

def MIPRE.SAT.Cnf5.falseLit {n : ℕ} (w : Fin (2 ^ n) → Bool) : Lit (Fin (2 ^ n))

Equations

• MIPRE.SAT.Cnf5.falseLit w = { var := 0, pos := !w 0 }

theorem MIPRE.SAT.Cnf5.eval_falseLit {n : ℕ} (w : Fin (2 ^ n) → Bool) : Lit.eval w (falseLit w) = false

theorem MIPRE.SAT.Cnf5.lit_true_iff {A : Type u_1} (w : A → Bool) (i : A) (o : Bool) : Lit.eval w { var := i, pos := o } = true ↔ w i = o

theorem MIPRE.SAT.Cnf5.sat_pad_iff {ℓ r ℓ' r' : ℕ} (hℓ : ℓ ≤ ℓ') (hr : r ≤ r') (φ : Cnf5 (Fin (2 ^ ℓ)) (Fin (2 ^ ℓ)) (Fin (2 ^ r)) (Fin (2 ^ r)) (Fin (2 ^ r))) (a b : Fin (2 ^ ℓ') → Bool) (w₁ w₂ w₃ : Fin (2 ^ r') → Bool) : (pad hℓ hr φ).Sat a b w₁ w₂ w₃ ↔ φ.Sat (a ∘ blockInclusion hℓ) (b ∘ blockInclusion hℓ) (w₁ ∘ blockInclusion hr) (w₂ ∘ blockInclusion hr) (w₃ ∘ blockInclusion hr) ∧ (∀ (i : Fin (2 ^ ℓ')), 2 ^ ℓ ≤ ↑i → a i = decide (↑i % 2 = 0)) ∧ ∀ (i : Fin (2 ^ ℓ')), 2 ^ ℓ ≤ ↑i → b i = decide (↑i % 2 = 0)

Padding satisfaction is exactly original satisfaction and both complete blank tails.

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

Beyond twice the answer length the tape is 10, starting at the even position.

theorem MIPRE.SAT.Circuit.DescribesDecider.of_pad {C C' : Circuit} {ℓ r ℓ' r' : ℕ} {D : Decider} {n T : ℕ} {x y : Cost.BitStr} (hC : C.DescribesDecider ℓ r D n x y T) (hℓ : ℓ ≤ ℓ') (hr : r ≤ r') (hT : 2 * T ≤ 2 ^ ℓ) (hpad : C'.formula5 ℓ' r' = Cnf5.pad hℓ hr (C.formula5 ℓ r)) : C'.DescribesDecider ℓ' r' D n x y T

A circuit implementing the padded clause set still describes the same decider, including the entire answer tapes and their blank tails.