The padded five-block clause describer

The construction in prop:exciting-padding-prop of answer_reduction.tex, applied to the formula used by the existing decoupled describer. Five index blocks acquire the common width m; the two answer tails are forced to be blank. Formula renaming preserves the original tree, so the construction remains polynomial in the old formula and the new width.

def MIPRE.TM.CookLevin.Pad.layout (ℓ r m : ℕ) : List ℕ

Where the original five blocks and signs lie in the padded input.

Equations

• MIPRE.TM.CookLevin.Pad.layout ℓ r m = List.range' 0 ℓ ++ List.range' m ℓ ++ List.range' (2 * m) r ++ List.range' (3 * m) r ++ List.range' (4 * m) r ++ List.range' (5 * m) 5

@[simp]

theorem MIPRE.TM.CookLevin.Pad.length_layout (ℓ r m : ℕ) : (layout ℓ r m).length = 2 * ℓ + 3 * r + 5

def MIPRE.TM.CookLevin.Pad.low (base old m : ℕ) : SAT.Fml

Test that the m-bit index at base is below 2^old. The comparison uses one extra zero bit, so it also works at old = m.

Equations

• MIPRE.TM.CookLevin.Pad.low base old m = MIPRE.SAT.Fml.ltConst (MIPRE.SAT.Fml.padTo (m + 1) (MIPRE.SAT.Fml.field base m)) (MIPRE.TM.CookLevin.Desc.nbits (m + 1) (2 ^ old))

theorem MIPRE.TM.CookLevin.Pad.eval_low (base old m : ℕ) (hm : old ≤ m) (x : ℕ → Bool) : SAT.Fml.eval x (low base old m) = true ↔ SAT.Fml.val (SAT.Fml.field base m) x < 2 ^ old

def MIPRE.TM.CookLevin.Pad.blankSign (base sign : ℕ) : SAT.Fml

The positive-at-even, negative-at-odd blank sign for one answer index.

Equations

• MIPRE.TM.CookLevin.Pad.blankSign base sign = (MIPRE.SAT.Fml.inp sign).xnor (MIPRE.SAT.Fml.inp base).not

def MIPRE.TM.CookLevin.Pad.formula (ℓ r m : ℕ) (f : SAT.Fml) : SAT.Fml

The padded formula: old clauses on old indices, or either answer-tail clause.

Equations

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

def MIPRE.TM.CookLevin.Pad.circuit (ℓ r m : ℕ) (f : SAT.Fml) : SAT.Circuit

The padded circuit, before padding its number of gates to the exact PCP count.

Equations

• MIPRE.TM.CookLevin.Pad.circuit ℓ r m f = MIPRE.SAT.Fml.toCircuit (5 * m + 5) (MIPRE.TM.CookLevin.Pad.formula ℓ r m f)

theorem MIPRE.TM.CookLevin.Pad.take_bitsOfNat (n m j : ℕ) (h : n ≤ m) : List.take n (SAT.bitsOfNat m j) = SAT.bitsOfNat n j

theorem MIPRE.TM.CookLevin.Pad.slice_index (pre post : Cost.BitStr) (m n j : ℕ) (hn : n ≤ m) : (Desc.ibOf (List.length pre) n fun (i : ℕ) => List.getD (pre ++ SAT.bitsOfNat m j ++ post) i false) = SAT.bitsOfNat n j

theorem MIPRE.TM.CookLevin.Pad.map_layout_clause {ℓ r m : ℕ} (hℓ : ℓ ≤ m) (hr : r ≤ m) (c : SAT.Clause5 (Fin (2 ^ ℓ)) (Fin (2 ^ ℓ)) (Fin (2 ^ r)) (Fin (2 ^ r)) (Fin (2 ^ r))) : List.map (fun (i : ℕ) => (SAT.clauseInput5 m m (SAT.Clause5.map (SAT.Cnf5.blockInclusion hℓ) (SAT.Cnf5.blockInclusion hℓ) (SAT.Cnf5.blockInclusion hr) (SAT.Cnf5.blockInclusion hr) (SAT.Cnf5.blockInclusion hr) c)).getD i false) (layout ℓ r m) = SAT.clauseInput5 ℓ r c

Reading the renaming table in a padded clause recovers the original input bits.

theorem MIPRE.TM.CookLevin.Pad.eval_renamed_clause {ℓ r m : ℕ} (hℓ : ℓ ≤ m) (hr : r ≤ m) (f : SAT.Fml) (hf : SAT.Fml.InputsLt (2 * ℓ + 3 * r + 5) f) (c : SAT.Clause5 (Fin (2 ^ ℓ)) (Fin (2 ^ ℓ)) (Fin (2 ^ r)) (Fin (2 ^ r)) (Fin (2 ^ r))) : SAT.Fml.eval (fun (i : ℕ) => (SAT.clauseInput5 m m (SAT.Clause5.map (SAT.Cnf5.blockInclusion hℓ) (SAT.Cnf5.blockInclusion hℓ) (SAT.Cnf5.blockInclusion hr) (SAT.Cnf5.blockInclusion hr) (SAT.Cnf5.blockInclusion hr) c)).getD i false) (SAT.Fml.rename (fun (i : ℕ) => (layout ℓ r m).getD i 0) f) = SAT.Fml.eval (fun (i : ℕ) => (SAT.clauseInput5 ℓ r c).getD i false) f

On an embedded clause, the renamed old formula has exactly its old value.

theorem MIPRE.TM.CookLevin.Pad.eval_blankSigns {m : ℕ} (hm : 1 ≤ m) (c : SAT.Clause5 (Fin (2 ^ m)) (Fin (2 ^ m)) (Fin (2 ^ m)) (Fin (2 ^ m)) (Fin (2 ^ m))) : (SAT.Fml.eval (fun (i : ℕ) => (SAT.clauseInput5 m m c).getD i false) (blankSign 0 (5 * m)) = true ↔ c.l₁.pos = decide (↑c.l₁.var % 2 = 0)) ∧ (SAT.Fml.eval (fun (i : ℕ) => (SAT.clauseInput5 m m c).getD i false) (blankSign m (5 * m + 1)) = true ↔ c.l₂.pos = decide (↑c.l₂.var % 2 = 0))

The two answer-tail predicates have precisely the source's repaired parity.

theorem MIPRE.TM.CookLevin.Pad.formula5_circuit {ℓ r m : ℕ} (hℓ : ℓ ≤ m) (hr : r ≤ m) (hm : 1 ≤ m) (f : SAT.Fml) (hf : SAT.Fml.InputsLt (2 * ℓ + 3 * r + 5) f) : (circuit ℓ r m f).formula5 m m = SAT.Cnf5.pad hℓ hr ((SAT.Fml.toCircuit (2 * ℓ + 3 * r + 5) f).formula5 ℓ r)

The constructed circuit describes exactly the padded clause set.

theorem MIPRE.TM.CookLevin.Pad.describes {ℓ r m n T : ℕ} {D : Decider} {x y : Cost.BitStr} (hℓ : ℓ ≤ m) (hr : r ≤ m) (hm : 1 ≤ m) (hT : 2 * T ≤ 2 ^ ℓ) (f : SAT.Fml) (hf : SAT.Fml.InputsLt (2 * ℓ + 3 * r + 5) f) (hC : (SAT.Fml.toCircuit (2 * ℓ + 3 * r + 5) f).DescribesDecider ℓ r D n x y T) : (circuit ℓ r m f).DescribesDecider m m D n x y T

Input-width padding preserves the full decider description.

theorem MIPRE.TM.CookLevin.Pad.mem_layout_lt {ℓ r m j : ℕ} (hℓ : ℓ ≤ m) (hr : r ≤ m) (hj : j ∈ layout ℓ r m) : j < 5 * m + 5

theorem MIPRE.TM.CookLevin.Pad.formula_inputsLt {ℓ r m : ℕ} (hℓ : ℓ ≤ m) (hr : r ≤ m) (f : SAT.Fml) (hf : SAT.Fml.InputsLt (2 * ℓ + 3 * r + 5) f) : SAT.Fml.InputsLt (5 * m + 5) (formula ℓ r m f)

Padding does not introduce references beyond the new input arity.

theorem MIPRE.TM.CookLevin.Pad.circuit_wellFormed {ℓ r m : ℕ} (hℓ : ℓ ≤ m) (hr : r ≤ m) (f : SAT.Fml) (hf : SAT.Fml.InputsLt (2 * ℓ + 3 * r + 5) f) : (circuit ℓ r m f).WellFormed

The constructed circuit is well formed in the existing circuit interface.

noncomputable def MIPRE.TM.CookLevin.Pad.baseR {ι : Type u_1} [Cost.SizedEncoding ι] (mu : Cost.PolyTimeFun ι Cost.Unary) (k : ℕ) : Cost.PolyTimeFun ι ℕ

Equations

• MIPRE.TM.CookLevin.Pad.baseR mu k = MIPRE.Cost.PolyTimeFun.unaryToBin.ap₁ ((MIPRE.TM.CookLevin.Desc.nsmulU k).ap₁ mu)

theorem MIPRE.TM.CookLevin.Pad.baseR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (mu : Cost.PolyTimeFun ι Cost.Unary) (k : ℕ) (i : ι) : (baseR mu k).toFun i = k * List.length (mu.toFun i)

noncomputable def MIPRE.TM.CookLevin.Pad.layoutR {ι : Type u_1} [Cost.SizedEncoding ι] (lu ru mu : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι (List ℕ)

The five-block offset table as an ambient program.

Equations

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

theorem MIPRE.TM.CookLevin.Pad.layoutR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (lu ru mu : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : (layoutR lu ru mu).toFun i = layout (List.length (lu.toFun i)) (List.length (ru.toFun i)) (List.length (mu.toFun i))

noncomputable def MIPRE.TM.CookLevin.Pad.lowR {ι : Type u_1} [Cost.SizedEncoding ι] (base : Cost.PolyTimeFun ι ℕ) (old mu : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι SAT.Fml

The original-width test, including the boundary case where both widths agree.

Equations

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

theorem MIPRE.TM.CookLevin.Pad.lowR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (base : Cost.PolyTimeFun ι ℕ) (old mu : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : (lowR base old mu).toFun i = low (base.toFun i) (List.length (old.toFun i)) (List.length (mu.toFun i))

noncomputable def MIPRE.TM.CookLevin.Pad.blankSignR {ι : Type u_1} [Cost.SizedEncoding ι] (base sign : Cost.PolyTimeFun ι ℕ) : Cost.PolyTimeFun ι SAT.Fml

Equations

• MIPRE.TM.CookLevin.Pad.blankSignR base sign = MIPRE.TM.CookLevin.Desc.xnorR (MIPRE.SAT.Fml.inpF.ap₁ sign) (MIPRE.TM.CookLevin.Desc.notR (MIPRE.SAT.Fml.inpF.ap₁ base))

theorem MIPRE.TM.CookLevin.Pad.blankSignR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (base sign : Cost.PolyTimeFun ι ℕ) (i : ι) : (blankSignR base sign).toFun i = blankSign (base.toFun i) (sign.toFun i)

noncomputable def MIPRE.TM.CookLevin.Pad.formulaR {ι : Type u_1} [Cost.SizedEncoding ι] (lu ru mu : Cost.PolyTimeFun ι Cost.Unary) (f : Cost.PolyTimeFun ι SAT.Fml) : Cost.PolyTimeFun ι SAT.Fml

The padded clause formula, constructed uniformly in polynomial time.

Equations

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

theorem MIPRE.TM.CookLevin.Pad.formulaR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (lu ru mu : Cost.PolyTimeFun ι Cost.Unary) (f : Cost.PolyTimeFun ι SAT.Fml) (i : ι) : (formulaR lu ru mu f).toFun i = formula (List.length (lu.toFun i)) (List.length (ru.toFun i)) (List.length (mu.toFun i)) (f.toFun i)

noncomputable def MIPRE.TM.CookLevin.Pad.circuitR {ι : Type u_1} [Cost.SizedEncoding ι] (lu ru mu : Cost.PolyTimeFun ι Cost.Unary) (f : Cost.PolyTimeFun ι SAT.Fml) : Cost.PolyTimeFun ι SAT.Circuit

The padded circuit itself, with the correct input count, as an ambient program.

Equations

• MIPRE.TM.CookLevin.Pad.circuitR lu ru mu f = MIPRE.SAT.Fml.toCircuitF.ap₂ ((MIPRE.TM.CookLevin.Desc.incN 5).ap₁ (MIPRE.TM.CookLevin.Pad.baseR mu 5)) (MIPRE.TM.CookLevin.Pad.formulaR lu ru mu f)

theorem MIPRE.TM.CookLevin.Pad.circuitR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (lu ru mu : Cost.PolyTimeFun ι Cost.Unary) (f : Cost.PolyTimeFun ι SAT.Fml) (i : ι) : (circuitR lu ru mu f).toFun i = circuit (List.length (lu.toFun i)) (List.length (ru.toFun i)) (List.length (mu.toFun i)) (f.toFun i)

Applying the construction to the existing decoupled describer

noncomputable def MIPRE.TM.CookLevin.Pad.innerDim (T σ : ℕ) : ℕ

The common power-of-two index width. The old auxiliary width dominates the old answer width, so this pads all five blocks.

Equations

• MIPRE.TM.CookLevin.Pad.innerDim T σ = MIPRE.SAT.ceilPower (MIPRE.TM.CookLevin.Desc.mParam T σ)

theorem MIPRE.TM.CookLevin.Pad.innerDim_isPow (T σ : ℕ) : ∃ (j : ℕ), innerDim T σ = 2 ^ j

theorem MIPRE.TM.CookLevin.Pad.oldWidth_le_innerDim (T σ : ℕ) : Desc.mParam T σ ≤ innerDim T σ

theorem MIPRE.TM.CookLevin.Pad.answerWidth_le_innerDim (T σ : ℕ) : Desc.lOf T ≤ innerDim T σ

theorem MIPRE.TM.CookLevin.Pad.innerDim_pos (T σ : ℕ) : 1 ≤ innerDim T σ

theorem MIPRE.TM.CookLevin.Pad.two_mul_le_innerDim (T σ : ℕ) : 2 * T ≤ 2 ^ innerDim T σ

theorem MIPRE.TM.CookLevin.Pad.innerDim_le : ∃ (c : ℕ), ∀ (T σ : ℕ), innerDim T σ ≤ c * (T.size + σ.size + 1)

noncomputable def MIPRE.TM.CookLevin.Pad.innerDimU : Cost.PolyTimeFun SAT.DescInput Cost.Unary

The common width in unary, computed directly from the succinct parameters.

Equations

• MIPRE.TM.CookLevin.Pad.innerDimU = MIPRE.SAT.ceilPowerProg.comp (MIPRE.TM.CookLevin.Desc.mU MIPRE.TM.CookLevin.Desc.dEu)

theorem MIPRE.TM.CookLevin.Pad.innerDimU_length (p : SAT.DescInput) : List.length (innerDimU.toFun p) = innerDim p.1.2.2.1 p.1.2.2.2.2

noncomputable def MIPRE.TM.CookLevin.Pad.describe : Cost.PolyTimeFun SAT.DescInput SAT.Circuit

The effective padded describer, before exact gate-count padding.

Equations

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

theorem MIPRE.TM.CookLevin.Pad.describe_apply (p : SAT.DescInput) : describe.toFun p = circuit (Desc.lOf p.1.2.2.1) (Desc.mParam p.1.2.2.1 p.1.2.2.2.2) (innerDim p.1.2.2.1 p.1.2.2.2.2) (Desc.descFml5 (Desc.lOf p.1.2.2.1) p.1.2.2.1 (Desc.eOf p.1.2.2.1 p.1.2.2.2.2) p.1.1 p.1.2.1 p.2.1 p.2.2)

theorem MIPRE.TM.CookLevin.Pad.describe_wellFormed (p : SAT.DescInput) : (describe.toFun p).WellFormed

theorem MIPRE.TM.CookLevin.Pad.describe_describes (D : Decider) (n T Q σ : ℕ) (x y : Cost.BitStr) (hV : SAT.Valid D.prog n T Q σ x y) : (describe.toFun ((D.prog, n, T, Q, σ), x, y)).DescribesDecider (innerDim T σ) (innerDim T σ) D n x y T

noncomputable def MIPRE.TM.CookLevin.Pad.gatePoly : Polynomial ℕ

A polynomial bound for the padded circuit, derived from its verified program.

Equations

• MIPRE.TM.CookLevin.Pad.gatePoly = MIPRE.TM.CookLevin.Pad.describe.timeBound.comp (Polynomial.C 25 * Polynomial.X + Polynomial.C 12)

theorem MIPRE.TM.CookLevin.Pad.describe_size_le (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) (hV : SAT.Valid D n T Q σ x y) : (describe.toFun ((D, n, T, Q, σ), x, y)).size ≤ Desc.roundUp gatePoly n T Q σ