The layout of the PCP coordinates

Piece AR-3d of planning/answer-reduction.md: how a program reads a vector of V^pcp.

• The coordinates are numbered in three runs (coordIndex): the concatenated point register V_{6,pt} (pt6, m' coordinates), the concatenated direction register V_{6,dir} (dir6), and the six seeds. A vector of V^pcp is thus the three lists ptOf6, dirOf6, seedsOf.
• Each copy of the test is a contiguous run of V_{6,pt} and of V_{6,dir} with its own seed (regsAt): copy i ≤ 5 at offset i·m and length m (regs_eq), copy 6 at offset 0 and length m' (regs6_eq).
• The bits of the downsized vector, numbered by bitIndex, are the field elements' Shoup bits in that order (toBits_pcp), so a program reads them by cutting k-bit blocks.

The concatenated registers

theorem MIPRE.AnswerReduction.Pcp.dir6_block (P : SAT.PcpParams) (i : Fin 5) (j : Fin P.m) : dir6 P ⟨↑i * P.m + ↑j, ⋯⟩ = Coord.dir i j

theorem MIPRE.AnswerReduction.Pcp.pt6_aux (P : SAT.PcpParams) (j : Fin (5 + P.s)) : pt6 P ⟨5 * P.m + ↑j, ⋯⟩ = Coord.auxPt j

theorem MIPRE.AnswerReduction.Pcp.dir6_aux (P : SAT.PcpParams) (j : Fin (5 + P.s)) : dir6 P ⟨5 * P.m + ↑j, ⋯⟩ = Coord.auxDir j

theorem MIPRE.AnswerReduction.Pcp.pt6_ne_coord (P : SAT.PcpParams) (r : Fin P.m') (c : Fin 6) : pt6 P r ≠ Coord.coord c

theorem MIPRE.AnswerReduction.Pcp.dir6_ne_coord (P : SAT.PcpParams) (r : Fin P.m') (c : Fin 6) : dir6 P r ≠ Coord.coord c

A copy of the test as a run of the concatenated registers

def MIPRE.AnswerReduction.Pcp.regsAt (P : SAT.PcpParams) (o sz : ℕ) (c : Fin 6) (h : o + sz ≤ P.m') : LIDT.CL.Regs (Coord P) sz

The registers of a copy at offset o and length sz of the concatenated registers, with the seed c.

Equations

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

theorem MIPRE.AnswerReduction.Pcp.regs_le (P : SAT.PcpParams) (i : Fin 5) : ↑i * P.m + P.m ≤ P.m'

theorem MIPRE.AnswerReduction.Pcp.regs_eq (P : SAT.PcpParams) (i : Fin 5) : regs P i = regsAt P (↑i * P.m) P.m i.castSucc ⋯

theorem MIPRE.AnswerReduction.Pcp.regs6_eq (P : SAT.PcpParams) : regs6 P = regsAt P 0 P.m' 5 ⋯

The three runs

def MIPRE.AnswerReduction.Pcp.ptOf6 (P : SAT.PcpParams) {F : Type u_1} (x : Coord P → F) : Fin P.m' → F

The concatenated point register of a vector.

Equations

• MIPRE.AnswerReduction.Pcp.ptOf6 P x r = x (MIPRE.AnswerReduction.Pcp.pt6 P r)

def MIPRE.AnswerReduction.Pcp.dirOf6 (P : SAT.PcpParams) {F : Type u_1} (x : Coord P → F) : Fin P.m' → F

The concatenated direction register of a vector.

Equations

• MIPRE.AnswerReduction.Pcp.dirOf6 P x r = x (MIPRE.AnswerReduction.Pcp.dir6 P r)

def MIPRE.AnswerReduction.Pcp.seedsOf (P : SAT.PcpParams) {F : Type u_1} (x : Coord P → F) : Fin 6 → F

The six seeds of a vector.

Equations

• MIPRE.AnswerReduction.Pcp.seedsOf P x c = x (MIPRE.AnswerReduction.Pcp.Coord.coord c)

def MIPRE.AnswerReduction.Pcp.layout (P : SAT.PcpParams) : Coord P ≃ Fin P.m' ⊕ Fin P.m' ⊕ Fin 6

The three runs of the coordinates.

Equations

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

@[reducible, inline]

abbrev MIPRE.AnswerReduction.Pcp.pcpDim (P : SAT.PcpParams) : ℕ

The number of coordinates of V^pcp, in the three runs.

Equations

• MIPRE.AnswerReduction.Pcp.pcpDim P = P.m' + (P.m' + 6)

theorem MIPRE.AnswerReduction.Pcp.pcpDim_eq (P : SAT.PcpParams) : pcpDim P = 10 * P.m + 2 * P.s + 16

def MIPRE.AnswerReduction.Pcp.coordIndex (P : SAT.PcpParams) : Coord P ≃ Fin (pcpDim P)

The numbering of the coordinates: V_{6,pt}, then V_{6,dir}, then the seeds.

Equations

• MIPRE.AnswerReduction.Pcp.coordIndex P = (MIPRE.AnswerReduction.Pcp.layout P).trans (((Equiv.refl (Fin P.m')).sumCongr finSumFinEquiv).trans finSumFinEquiv)

theorem MIPRE.AnswerReduction.Pcp.layout_pt6 (P : SAT.PcpParams) (r : Fin P.m') : (layout P) (pt6 P r) = Sum.inl r

theorem MIPRE.AnswerReduction.Pcp.layout_dir6 (P : SAT.PcpParams) (r : Fin P.m') : (layout P) (dir6 P r) = Sum.inr (Sum.inl r)

theorem MIPRE.AnswerReduction.Pcp.layout_coord (P : SAT.PcpParams) (c : Fin 6) : (layout P) (Coord.coord c) = Sum.inr (Sum.inr c)

@[simp]

theorem MIPRE.AnswerReduction.Pcp.coordIndex_symm_castAdd (P : SAT.PcpParams) (r : Fin P.m') : (coordIndex P).symm (Fin.castAdd (P.m' + 6) r) = pt6 P r

@[simp]

theorem MIPRE.AnswerReduction.Pcp.coordIndex_symm_natAdd_castAdd (P : SAT.PcpParams) (r : Fin P.m') : (coordIndex P).symm (Fin.natAdd P.m' (Fin.castAdd 6 r)) = dir6 P r

@[simp]

theorem MIPRE.AnswerReduction.Pcp.coordIndex_symm_natAdd_natAdd (P : SAT.PcpParams) (c : Fin 6) : (coordIndex P).symm (Fin.natAdd P.m' (Fin.natAdd P.m' c)) = Coord.coord c

theorem MIPRE.AnswerReduction.Pcp.ofFn_coordIndex (P : SAT.PcpParams) {α : Type u_2} (g : Coord P → α) : (List.ofFn fun (r : Fin (pcpDim P)) => g ((coordIndex P).symm r)) = ((List.ofFn fun (r : Fin P.m') => g (pt6 P r)) ++ List.ofFn fun (r : Fin P.m') => g (dir6 P r)) ++ List.ofFn fun (c : Fin 6) => g (Coord.coord c)

Reading a vector in the numbering is reading its three runs.

The bits of a downsized vector

def MIPRE.AnswerReduction.Pcp.bitIndex (P : SAT.PcpParams) (k : ℕ) : Coord P × Fin k ≃ Fin (pcpDim P * k)

The numbering of the bits: coordinate by coordinate, k bits each.

Equations

• MIPRE.AnswerReduction.Pcp.bitIndex P k = ((MIPRE.AnswerReduction.Pcp.coordIndex P).prodCongr (Equiv.refl (Fin k))).trans finProdFinEquiv

noncomputable def MIPRE.AnswerReduction.Pcp.flatBits (P : SAT.PcpParams) {k : ℕ} (hk : 1 ≤ k) (v : Coord P → (SAT.shoupBinField k hk).carrier) : Cost.BitStr

The Shoup bits of a vector of V^pcp, in the numbering.

Equations

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

theorem MIPRE.AnswerReduction.Pcp.vecBits_coordIndex (P : SAT.PcpParams) {k : ℕ} (hk : 1 ≤ k) (v : Coord P → (SAT.shoupBinField k hk).carrier) : ((SAT.shoupBinField k hk).vecBits fun (r : Fin (pcpDim P)) => v ((coordIndex P).symm r)) = (SAT.shoupBinField k hk).vecBits (ptOf6 P v) ++ (SAT.shoupBinField k hk).vecBits (dirOf6 P v) ++ (SAT.shoupBinField k hk).vecBits (seedsOf P v)

theorem MIPRE.AnswerReduction.Pcp.repr_shoup {k : ℕ} (hk : 1 ≤ k) (a : (SAT.shoupBinField k hk).carrier) : (List.ofFn fun (j : Fin k) => decide (((SAT.shoupPowerBasis k hk).repr a) j = 1)) = (SAT.shoupBinField k hk).toBits a

theorem MIPRE.AnswerReduction.Pcp.bitIndex_symm (P : SAT.PcpParams) {k : ℕ} (r : Fin (pcpDim P)) (j : Fin k) (h : ↑r * k + ↑j < pcpDim P * k) : (bitIndex P k).symm ⟨↑r * k + ↑j, h⟩ = ((coordIndex P).symm r, j)

theorem MIPRE.AnswerReduction.Pcp.toBits_pcp (P : SAT.PcpParams) {k : ℕ} (hk : 1 ≤ k) (v : Coord P → (SAT.shoupBinField k hk).carrier) : CL.toBits ((CL.reindexEquiv (bitIndex P k)) ((CL.downsizeEquiv (SAT.shoupPowerBasis k hk)) v)) = flatBits P hk v

The bits of the downsized vector are its coordinates' Shoup bits, in the numbering.

theorem MIPRE.AnswerReduction.Pcp.exists_flatBits (P : SAT.PcpParams) {k : ℕ} (hk : 1 ≤ k) {z : Cost.BitStr} (hz : List.length z = pcpDim P * k) : ∃ (v : Coord P → (SAT.shoupBinField k hk).carrier), z = flatBits P hk v

Every bit string of the right length is the bits of a vector of V^pcp.