The queries of a copy of the PCP sampler, run by run

Piece AR-3d of planning/answer-reduction.md. A copy of the seeded test in the PCP sampler is a run [o, o + sz) of the concatenated registers with a seed c (regsAt). This file writes what its presentation's queries return in the three runs of MIPRE/Background/AnswerReduction/ Layout (ptOf6, dirOf6, seedsOf), which is the form a program computes:

• the marginals (comps_marginal): the seed on the seed run, the cut-down direction placed at o on the direction run for a diagonal line, the line's base point placed at o on the point run;
• the stage maps from a prefix (comps_map_zero, comps_map_one, comps_map_two);
• the factor spaces, run by run (mem_coordSet_*, mem_dirSet_*, mem_finalSet_*).

Placing and slicing vectors

def MIPRE.AnswerReduction.Pcp.placeV {F : Type u_1} [Zero F] {N sz : ℕ} (o : ℕ) (w : Fin sz → F) : Fin N → F

A vector of length sz placed at offset o of Fin N, zero elsewhere.

Equations

• MIPRE.AnswerReduction.Pcp.placeV o w r = if h : o ≤ ↑r ∧ ↑r < o + sz then w ⟨↑r - o, ⋯⟩ else 0

def MIPRE.AnswerReduction.Pcp.sliceV {F : Type u_1} {N : ℕ} (o sz : ℕ) (h : o + sz ≤ N) (v : Fin N → F) : Fin sz → F

The run [o, o + sz) of a vector of length N.

Equations

• MIPRE.AnswerReduction.Pcp.sliceV o sz h v j = v ⟨o + ↑j, ⋯⟩

The runs of the three kinds of vectors a copy writes

@[simp]

theorem MIPRE.AnswerReduction.Pcp.ptOf6_add (P : SAT.PcpParams) {F : Type u_1} [Field F] (x y : Coord P → F) : ptOf6 P (x + y) = ptOf6 P x + ptOf6 P y

@[simp]

theorem MIPRE.AnswerReduction.Pcp.dirOf6_add (P : SAT.PcpParams) {F : Type u_1} [Field F] (x y : Coord P → F) : dirOf6 P (x + y) = dirOf6 P x + dirOf6 P y

@[simp]

theorem MIPRE.AnswerReduction.Pcp.seedsOf_add (P : SAT.PcpParams) {F : Type u_1} [Field F] (x y : Coord P → F) : seedsOf P (x + y) = seedsOf P x + seedsOf P y

@[simp]

theorem MIPRE.AnswerReduction.Pcp.ptOf6_zero (P : SAT.PcpParams) {F : Type u_1} [Field F] : ptOf6 P 0 = 0

@[simp]

theorem MIPRE.AnswerReduction.Pcp.dirOf6_zero (P : SAT.PcpParams) {F : Type u_1} [Field F] : dirOf6 P 0 = 0

@[simp]

theorem MIPRE.AnswerReduction.Pcp.seedsOf_zero (P : SAT.PcpParams) {F : Type u_1} [Field F] : seedsOf P 0 = 0

theorem MIPRE.AnswerReduction.Pcp.dirOf_regsAt (P : SAT.PcpParams) {F : Type u_1} (o sz : ℕ) (c : Fin 6) (h : o + sz ≤ P.m') (x : Coord P → F) : (regsAt P o sz c h).dirOf x = sliceV o sz h (dirOf6 P x)

theorem MIPRE.AnswerReduction.Pcp.pt6_eq_iff (P : SAT.PcpParams) (o sz : ℕ) (c : Fin 6) (h : o + sz ≤ P.m') (r : Fin P.m') (j : Fin sz) : (regsAt P o sz c h).pt j = pt6 P r ↔ ↑r = o + ↑j

theorem MIPRE.AnswerReduction.Pcp.dir6_eq_iff (P : SAT.PcpParams) (o sz : ℕ) (c : Fin 6) (h : o + sz ≤ P.m') (r : Fin P.m') (j : Fin sz) : (regsAt P o sz c h).dir j = dir6 P r ↔ ↑r = o + ↑j

theorem MIPRE.AnswerReduction.Pcp.ptOf6_putPt (P : SAT.PcpParams) {F : Type u_1} [Field F] (o sz : ℕ) (c : Fin 6) (h : o + sz ≤ P.m') (w : Fin sz → F) : ptOf6 P ((regsAt P o sz c h).putPt w) = placeV o w

theorem MIPRE.AnswerReduction.Pcp.dirOf6_putDir (P : SAT.PcpParams) {F : Type u_1} [Field F] (o sz : ℕ) (c : Fin 6) (h : o + sz ≤ P.m') (w : Fin sz → F) : dirOf6 P ((regsAt P o sz c h).putDir w) = placeV o w

theorem MIPRE.AnswerReduction.Pcp.dirOf6_putPt (P : SAT.PcpParams) {F : Type u_1} [Field F] (o sz : ℕ) (c : Fin 6) (h : o + sz ≤ P.m') (w : Fin sz → F) : dirOf6 P ((regsAt P o sz c h).putPt w) = 0

theorem MIPRE.AnswerReduction.Pcp.seedsOf_putPt (P : SAT.PcpParams) {F : Type u_1} [Field F] (o sz : ℕ) (c : Fin 6) (h : o + sz ≤ P.m') (w : Fin sz → F) : seedsOf P ((regsAt P o sz c h).putPt w) = 0

theorem MIPRE.AnswerReduction.Pcp.ptOf6_putDir (P : SAT.PcpParams) {F : Type u_1} [Field F] (o sz : ℕ) (c : Fin 6) (h : o + sz ≤ P.m') (w : Fin sz → F) : ptOf6 P ((regsAt P o sz c h).putDir w) = 0

theorem MIPRE.AnswerReduction.Pcp.seedsOf_putDir (P : SAT.PcpParams) {F : Type u_1} [Field F] (o sz : ℕ) (c : Fin 6) (h : o + sz ≤ P.m') (w : Fin sz → F) : seedsOf P ((regsAt P o sz c h).putDir w) = 0

theorem MIPRE.AnswerReduction.Pcp.mem_coordSet_pt6 (P : SAT.PcpParams) (o sz : ℕ) (c : Fin 6) (h : o + sz ≤ P.m') (r : Fin P.m') : pt6 P r ∉ (regsAt P o sz c h).coordSet

theorem MIPRE.AnswerReduction.Pcp.mem_coordSet_dir6 (P : SAT.PcpParams) (o sz : ℕ) (c : Fin 6) (h : o + sz ≤ P.m') (r : Fin P.m') : dir6 P r ∉ (regsAt P o sz c h).coordSet

theorem MIPRE.AnswerReduction.Pcp.mem_coordSet_coord (P : SAT.PcpParams) (o sz : ℕ) (c : Fin 6) (h : o + sz ≤ P.m') (c' : Fin 6) : Coord.coord c' ∈ (regsAt P o sz c h).coordSet ↔ c' = c

theorem MIPRE.AnswerReduction.Pcp.mem_dirSet_pt6 (P : SAT.PcpParams) (o sz : ℕ) (c : Fin 6) (h : o + sz ≤ P.m') (r : Fin P.m') : pt6 P r ∉ (regsAt P o sz c h).dirSet

theorem MIPRE.AnswerReduction.Pcp.mem_dirSet_dir6 (P : SAT.PcpParams) (o sz : ℕ) (c : Fin 6) (h : o + sz ≤ P.m') (r : Fin P.m') : dir6 P r ∈ (regsAt P o sz c h).dirSet ↔ o ≤ ↑r ∧ ↑r < o + sz

theorem MIPRE.AnswerReduction.Pcp.mem_dirSet_coord (P : SAT.PcpParams) (o sz : ℕ) (c : Fin 6) (h : o + sz ≤ P.m') (c' : Fin 6) : Coord.coord c' ∉ (regsAt P o sz c h).dirSet

theorem MIPRE.AnswerReduction.Pcp.mem_finalSet_pt6 (P : SAT.PcpParams) (o sz : ℕ) (c : Fin 6) (h : o + sz ≤ P.m') (r : Fin P.m') : pt6 P r ∈ (regsAt P o sz c h).finalSet

theorem MIPRE.AnswerReduction.Pcp.mem_finalSet_dir6 (P : SAT.PcpParams) (o sz : ℕ) (c : Fin 6) (h : o + sz ≤ P.m') (r : Fin P.m') : dir6 P r ∈ (regsAt P o sz c h).finalSet ↔ ¬(o ≤ ↑r ∧ ↑r < o + sz)

theorem MIPRE.AnswerReduction.Pcp.mem_finalSet_coord (P : SAT.PcpParams) (o sz : ℕ) (c : Fin 6) (h : o + sz ≤ P.m') (c' : Fin 6) : Coord.coord c' ∈ (regsAt P o sz c h).finalSet ↔ c' ≠ c

theorem MIPRE.AnswerReduction.Pcp.seedsOf_proj_coordSet (P : SAT.PcpParams) {F : Type u_1} [Field F] (o sz : ℕ) (c : Fin 6) (h : o + sz ≤ P.m') (x : Coord P → F) : seedsOf P ((CL.proj (regsAt P o sz c h).coordSet) x) = Pi.single c (seedsOf P x c)

theorem MIPRE.AnswerReduction.Pcp.ptOf6_proj_coordSet (P : SAT.PcpParams) {F : Type u_1} [Field F] (o sz : ℕ) (c : Fin 6) (h : o + sz ≤ P.m') (x : Coord P → F) : ptOf6 P ((CL.proj (regsAt P o sz c h).coordSet) x) = 0

theorem MIPRE.AnswerReduction.Pcp.dirOf6_proj_coordSet (P : SAT.PcpParams) {F : Type u_1} [Field F] (o sz : ℕ) (c : Fin 6) (h : o + sz ≤ P.m') (x : Coord P → F) : dirOf6 P ((CL.proj (regsAt P o sz c h).coordSet) x) = 0

The queries, run by run

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

The three runs of a vector.

Equations

• MIPRE.AnswerReduction.Pcp.comps P x = (MIPRE.AnswerReduction.Pcp.ptOf6 P x, MIPRE.AnswerReduction.Pcp.dirOf6 P x, MIPRE.AnswerReduction.Pcp.seedsOf P x)

theorem MIPRE.AnswerReduction.Pcp.comps_add (P : SAT.PcpParams) {F : Type u_1} [Field F] (x y : Coord P → F) : comps P (x + y) = comps P x + comps P y

def MIPRE.AnswerReduction.Pcp.seedPart {F : Type u_1} [Field F] (c : Fin 6) (t : LIDT.CL.Ty) (s : F) : Fin 6 → F

The seed run of a line type's first stage.

Equations

• MIPRE.AnswerReduction.Pcp.seedPart c t s = if t = MIPRE.LIDT.CL.Ty.point then 0 else Pi.single c s

def MIPRE.AnswerReduction.Pcp.dirPart {F : Type u_1} [Field F] (sz : ℕ) [Fintype F] [DecidableEq F] [NeZero sz] {hsz : sz ∣ Fintype.card F} (S : LIDT.CL.Sel F sz hsz) (t : LIDT.CL.Ty) (s : F) (d : Fin sz → F) : Fin sz → F

The direction a diagonal line type's second stage writes, before placing.

Equations

• MIPRE.AnswerReduction.Pcp.dirPart sz S t s d = if t = MIPRE.LIDT.CL.Ty.dline then MIPRE.LIDT.CL.zeroBelow (S.χ s) d else 0

theorem MIPRE.AnswerReduction.Pcp.comps_seedLin (P : SAT.PcpParams) {F : Type u_1} [Field F] (o sz : ℕ) (c : Fin 6) (h : o + sz ≤ P.m') (t : LIDT.CL.Ty) (x : Coord P → F) : comps P (((regsAt P o sz c h).seedLin t) x) = (0, 0, seedPart c t (seedsOf P x c))

theorem MIPRE.AnswerReduction.Pcp.comps_secondLin (P : SAT.PcpParams) {F : Type u_1} [Field F] (o sz : ℕ) (c : Fin 6) (h : o + sz ≤ P.m') [Fintype F] [DecidableEq F] [NeZero sz] {hsz : sz ∣ Fintype.card F} (S : LIDT.CL.Sel F sz hsz) (t : LIDT.CL.Ty) (s : F) (x : Coord P → F) : comps P (((regsAt P o sz c h).secondLin S t s) x) = (0, placeV o (dirPart sz S t s (sliceV o sz h (dirOf6 P x))), 0)

theorem MIPRE.AnswerReduction.Pcp.comps_putPt (P : SAT.PcpParams) {F : Type u_1} [Field F] (o sz : ℕ) (c : Fin 6) (h : o + sz ≤ P.m') (w : Fin sz → F) : comps P ((regsAt P o sz c h).putPt w) = (placeV o w, 0, 0)

theorem MIPRE.AnswerReduction.Pcp.comps_marginal (P : SAT.PcpParams) {F : Type u_1} [Field F] (o sz : ℕ) (c : Fin 6) (h : o + sz ≤ P.m') [Fintype F] [DecidableEq F] [NeZero sz] {hsz : sz ∣ Fintype.card F} (S : LIDT.CL.Sel F sz hsz) (t : LIDT.CL.Ty) {j : ℕ} (hj : 1 ≤ j) (x : Coord P → F) : comps P ((CL.CLFun.truncate j ((regsAt P o sz c h).pres S t)).eval x) = (if 3 ≤ j then placeV o ((LIDT.CL.Regs.ptMap S t (seedsOf P x c) (dirPart sz S t (seedsOf P x c) (sliceV o sz h (dirOf6 P x)))) (sliceV o sz h (ptOf6 P x))) else 0, if 2 ≤ j then placeV o (dirPart sz S t (seedsOf P x c) (sliceV o sz h (dirOf6 P x))) else 0, seedPart c t (seedsOf P x c))

The marginals, run by run, from the first level on.

theorem MIPRE.AnswerReduction.Pcp.comps_map_zero (P : SAT.PcpParams) {F : Type u_1} [Field F] (o sz : ℕ) (c : Fin 6) (h : o + sz ≤ P.m') [Fintype F] [DecidableEq F] [NeZero sz] {hsz : sz ∣ Fintype.card F} (S : LIDT.CL.Sel F sz hsz) (t : LIDT.CL.Ty) (u y : Coord P → F) : comps P ((((regsAt P o sz c h).pres S t).mapOfPrefix 0 u) y) = (0, 0, seedPart c t (seedsOf P y c))

The first stage map, run by run.

theorem MIPRE.AnswerReduction.Pcp.comps_map_one (P : SAT.PcpParams) {F : Type u_1} [Field F] (o sz : ℕ) (c : Fin 6) (h : o + sz ≤ P.m') [Fintype F] [DecidableEq F] [NeZero sz] {hsz : sz ∣ Fintype.card F} (S : LIDT.CL.Sel F sz hsz) (t : LIDT.CL.Ty) (u y : Coord P → F) : comps P ((((regsAt P o sz c h).pres S t).mapOfPrefix 1 u) y) = (0, placeV o (dirPart sz S t (seedsOf P u c) (sliceV o sz h (dirOf6 P y))), 0)

The second stage map, run by run.

theorem MIPRE.AnswerReduction.Pcp.comps_map_two (P : SAT.PcpParams) {F : Type u_1} [Field F] (o sz : ℕ) (c : Fin 6) (h : o + sz ≤ P.m') [Fintype F] [DecidableEq F] [NeZero sz] {hsz : sz ∣ Fintype.card F} (S : LIDT.CL.Sel F sz hsz) (t : LIDT.CL.Ty) (u y : Coord P → F) : comps P ((((regsAt P o sz c h).pres S t).mapOfPrefix 2 u) y) = (placeV o ((LIDT.CL.Regs.ptMap S t (seedsOf P u c) (sliceV o sz h (dirOf6 P u))) (sliceV o sz h (ptOf6 P y))), 0, 0)

The third stage map, run by run.