Clause indices and the five Boolean PCP blocks

The describer reads five little-endian indices followed by their signs. This module identifies that input format with the Boolean coordinates used by the low-degree PCP, including both directions of the index encoding.

def MIPRE.SAT.cubeIndex {m : ℕ} (y : Fin m → Bool) : Fin (2 ^ m)

A Boolean cube point as a little-endian index.

Equations

• MIPRE.SAT.cubeIndex y = ⟨MIPRE.Cost.bitsVal (List.ofFn y), ⋯⟩

def MIPRE.SAT.indexCube {m : ℕ} (i : Fin (2 ^ m)) : Fin m → Bool

The Boolean cube point named by a little-endian index.

Equations

• MIPRE.SAT.indexCube i j = (↑i).testBit ↑j

@[simp]

theorem MIPRE.SAT.bitsOfNat_cubeIndex {m : ℕ} (y : Fin m → Bool) : bitsOfNat m ↑(cubeIndex y) = List.ofFn y

@[simp]

theorem MIPRE.SAT.cubeIndex_indexCube {m : ℕ} (i : Fin (2 ^ m)) : cubeIndex (indexCube i) = i

@[simp]

theorem MIPRE.SAT.indexCube_cubeIndex {m : ℕ} (y : Fin m → Bool) : indexCube (cubeIndex y) = y

def MIPRE.SAT.cubeIndexEquiv (m : ℕ) : (Fin m → Bool) ≃ Fin (2 ^ m)

The concrete bijection used when decoding the five answer assignments.

Equations

• MIPRE.SAT.cubeIndexEquiv m = { toFun := MIPRE.SAT.cubeIndex, invFun := MIPRE.SAT.indexCube, left_inv := ⋯, right_inv := ⋯ }

theorem MIPRE.SAT.bitsOfNat_injective_fin (m : ℕ) : Function.Injective fun (i : Fin (2 ^ m)) => bitsOfNat m ↑i

theorem MIPRE.SAT.clauseInput5_injective (m : ℕ) : Function.Injective (clauseInput5 m m)

Equal-width clause encodings lose neither an index nor a sign.

def MIPRE.SAT.Clause5.literals {V : Type u_1} (c : Clause5 V V V V V) : Fin 5 → Lit V

Uniformly indexed literals of a clause with equally sized variable blocks.

Equations

• c.literals = ![c.l₁, c.l₂, c.l₃, c.l₄, c.l₅]

def MIPRE.SAT.Clause5.ofLiterals {V : Type u_1} (l : Fin 5 → Lit V) : Clause5 V V V V V

Equations

• MIPRE.SAT.Clause5.ofLiterals l = { l₁ := l 0, l₂ := l 1, l₃ := l 2, l₄ := l 3, l₅ := l 4 }

@[simp]

theorem MIPRE.SAT.Clause5.literals_ofLiterals {V : Type u_1} (l : Fin 5 → Lit V) : (ofLiterals l).literals = l

@[simp]

theorem MIPRE.SAT.Clause5.ofLiterals_literals {V : Type u_1} (c : Clause5 V V V V V) : ofLiterals c.literals = c

theorem MIPRE.SAT.Clause5.lit_true_iff {V : Type u_1} (l : Lit V) (a : V → Bool) : Lit.eval a l = true ↔ a l.var = l.pos

theorem MIPRE.SAT.Clause5.eval_iff_exists {V : Type u_1} (c : Clause5 V V V V V) (a : Fin 5 → V → Bool) : eval (a 0) (a 1) (a 2) (a 3) (a 4) c = true ↔ ∃ (i : Fin 5), a i (c.literals i).var = (c.literals i).pos

The five Boolean disjuncts are precisely the satisfying-literal condition in the algebraic PCP completeness and decoding lemmas.

def MIPRE.SAT.PcpParams.pointClause (P : PcpParams) (y : Fin P.m' → Bool) : Clause5 (Fin (2 ^ P.m)) (Fin (2 ^ P.m)) (Fin (2 ^ P.m)) (Fin (2 ^ P.m)) (Fin (2 ^ P.m))

The clause described by the first five blocks and sign coordinates of a point.

Equations

• P.pointClause y = MIPRE.SAT.Clause5.ofLiterals fun (i : Fin 5) => { var := MIPRE.SAT.cubeIndex (P.block i y), pos := y (P.signIndex i) }

@[simp]

theorem MIPRE.SAT.PcpParams.pointClause_literals (P : PcpParams) (y : Fin P.m' → Bool) (i : Fin 5) : (P.pointClause y).literals i = { var := cubeIndex (P.block i y), pos := y (P.signIndex i) }

def MIPRE.SAT.PcpParams.inputSlice (P : PcpParams) (y : Fin P.m' → Bool) : List Bool

The circuit-input slice of a Boolean PCP point.

Equations

• P.inputSlice y = List.ofFn fun (j : Fin (5 * P.m + 5)) => y ⟨↑j, ⋯⟩

@[simp]

theorem MIPRE.SAT.PcpParams.length_inputSlice (P : PcpParams) (y : Fin P.m' → Bool) : (P.inputSlice y).length = 5 * P.m + 5

theorem MIPRE.SAT.PcpParams.clauseInput5_pointClause (P : PcpParams) (y : Fin P.m' → Bool) : clauseInput5 P.m P.m (P.pointClause y) = P.inputSlice y

The describer's actual input order agrees with the five PCP blocks and signs.

def MIPRE.SAT.PcpParams.pointFromClause (P : PcpParams) (c : Clause5 (Fin (2 ^ P.m)) (Fin (2 ^ P.m)) (Fin (2 ^ P.m)) (Fin (2 ^ P.m)) (Fin (2 ^ P.m))) : Fin P.m' → Bool

Extend a described clause to a PCP point, initially setting all gate coordinates to false. Those coordinates may subsequently be replaced by a witness.

Equations

• P.pointFromClause c j = (MIPRE.SAT.clauseInput5 P.m P.m c).getD (↑j) false

theorem MIPRE.SAT.PcpParams.inputSlice_pointFromClause (P : PcpParams) (c : Clause5 (Fin (2 ^ P.m)) (Fin (2 ^ P.m)) (Fin (2 ^ P.m)) (Fin (2 ^ P.m)) (Fin (2 ^ P.m))) : P.inputSlice (P.pointFromClause c) = clauseInput5 P.m P.m c

@[simp]

theorem MIPRE.SAT.PcpParams.pointClause_pointFromClause (P : PcpParams) (c : Clause5 (Fin (2 ^ P.m)) (Fin (2 ^ P.m)) (Fin (2 ^ P.m)) (Fin (2 ^ P.m)) (Fin (2 ^ P.m))) : P.pointClause (P.pointFromClause c) = c

@[simp]

theorem MIPRE.SAT.PcpParams.sign_pointFromClause (P : PcpParams) (c : Clause5 (Fin (2 ^ P.m)) (Fin (2 ^ P.m)) (Fin (2 ^ P.m)) (Fin (2 ^ P.m)) (Fin (2 ^ P.m))) (i : Fin 5) : P.pointFromClause c (P.signIndex i) = (c.literals i).pos