Soundness of answer reduction: the low-degree test inside the predicate

Piece AR-5b of planning/answer-reduction.md (claim:ar-3, claim:ar-4): on the nine type pairs of one copy of the low-degree test, at a role pair where the answer-reduced predicate runs that copy's test, acceptance of the predicate implies acceptance of the seeded CL test on the questions the copy's presentation computes (cl_accepts_of_accepts, cl_accepts_of_accepts6). The copies tested are copy v for the isolated player v (step 3), copies 3, 4, 5 and the sixth for two oracles (step 4); an oracle's copies 1 and 2 are tested only through the isolated players.

The CL test's equality subtest on equal types is the predicate's step 1, its format check is the preamble, and its point-against-line subtests are steps 3 and 4, in either order of the players (CL.accepts_comm).

theorem MIPRE.LIDT.CL.subtests_comm {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d ldc : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (x y : Question F m) (a b : Answer F m d ldc) : subtests hm x y a b = subtests hm y x b a

theorem MIPRE.LIDT.CL.accepts_comm {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d ldc : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (x y : Question F m) (a b : Answer F m d ldc) : accepts hm x y a b = accepts hm y x b a

The seeded test is symmetric in the two players.

def MIPRE.AnswerReduction.LDStep (r : Role) (i : Fin 5) : Prop

The role pairs and copies at which the predicate runs a copy's low-degree test: copy v for the isolated player v, copies 3, 4, 5 for two oracles.

Equations

• MIPRE.AnswerReduction.LDStep r i = (MIPRE.AnswerReduction.roleIdx r = some i ∨ r = MIPRE.Role.oracle ∧ 2 ≤ ↑i)

theorem MIPRE.AnswerReduction.fmtOk_of_ansFmt {P : SAT.PcpParams} {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [NeZero P.m] {hm : P.m ∣ Fintype.card F} (S : LIDT.CL.Sel F P.m hm) {i : Fin 5} {τ : LIDT.CL.Ty} {u : Ans P F} (h : ansFmt (i.castSucc, τ) u = true) (y : Pcp.Coord P → F) : (q1 S i τ y).fmtOk (ans1 u) = true

theorem MIPRE.AnswerReduction.fmtOk_of_ansFmt6 {P : SAT.PcpParams} {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {hm' : P.m' ∣ Fintype.card F} (S' : LIDT.CL.Sel F P.m' hm') {i : Fin 6} (hi : ↑i = 5) {τ : LIDT.CL.Ty} {u : Ans P F} (h : ansFmt (i, τ) u = true) (y : Pcp.Coord P → F) : (q6 S' τ y).fmtOk (ans6 u) = true

theorem MIPRE.AnswerReduction.cl_accepts_of_side {P : SAT.PcpParams} {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [NeZero P.m] {hm : P.m ∣ Fintype.card F} {hm' : P.m' ∣ Fintype.card F} (S : LIDT.CL.Sel F P.m hm) (S' : LIDT.CL.Sel F P.m' hm') {X : Type u_2} (check : X → (Fin P.m' → F) → (Fin (P.m' + 6) → F) → Bool) {r : Role} {i : Fin 5} (hr : LDStep r i) {τ' : LIDT.CL.Ty} (hτ' : τ' ≠ LIDT.CL.Ty.point) {x x' : X} {y y' : Pcp.Coord P → F} {u v : Ans P F} (h : side S S' check ((r, i.castSucc, LIDT.CL.Ty.point), x, y) ((r, i.castSucc, τ'), x', y') u v = true) : LIDT.CL.accepts hm (q1 S i LIDT.CL.Ty.point y) (q1 S i τ' y') (ans1 u) (ans1 v) = true

Step 3 or step 4(b), read off one side: a point answer of copy i against a line answer of the same copy, at a role pair where the copy is tested.

theorem MIPRE.AnswerReduction.cl_accepts_of_accepts {P : SAT.PcpParams} {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [NeZero P.m] {hm : P.m ∣ Fintype.card F} {hm' : P.m' ∣ Fintype.card F} (S : LIDT.CL.Sel F P.m hm) (S' : LIDT.CL.Sel F P.m' hm') {X : Type u_2} (check : X → (Fin P.m' → F) → (Fin (P.m' + 6) → F) → Bool) {r : Role} {i : Fin 5} (hr : LDStep r i) (τ τ' : LIDT.CL.Ty) {x x' : X} {y y' : Pcp.Coord P → F} {u v : Ans P F} (h : accepts S S' check ((r, i.castSucc, τ), x, y) ((r, i.castSucc, τ'), x', y') u v = true) : LIDT.CL.accepts hm (q1 S i τ y) (q1 S i τ' y') (ans1 u) (ans1 v) = true

The copy's test inside the predicate: on the nine type pairs of copy i ≤ 5, at a role pair where the copy is tested, acceptance of the answer-reduced predicate implies acceptance of the seeded CL test on the questions the copy's registers carry.

theorem MIPRE.AnswerReduction.cl_accepts_of_side6 {P : SAT.PcpParams} {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [NeZero P.m] {hm : P.m ∣ Fintype.card F} {hm' : P.m' ∣ Fintype.card F} (S : LIDT.CL.Sel F P.m hm) (S' : LIDT.CL.Sel F P.m' hm') {X : Type u_2} (check : X → (Fin P.m' → F) → (Fin (P.m' + 6) → F) → Bool) {i : Fin 6} (hi : ↑i = 5) {τ' : LIDT.CL.Ty} (hτ' : τ' ≠ LIDT.CL.Ty.point) {x x' : X} {y y' : Pcp.Coord P → F} {u v : Ans P F} (h : side S S' check ((Role.oracle, i, LIDT.CL.Ty.point), x, y) ((Role.oracle, i, τ'), x', y') u v = true) : LIDT.CL.accepts hm' (q6 S' LIDT.CL.Ty.point y) (q6 S' τ' y') (ans6 u) (ans6 v) = true

Step 4(c), read off one side: the sixth copy's point answer against its line answer, for two oracles.

theorem MIPRE.AnswerReduction.cl_accepts_of_accepts6 {P : SAT.PcpParams} {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [NeZero P.m] {hm : P.m ∣ Fintype.card F} {hm' : P.m' ∣ Fintype.card F} (S : LIDT.CL.Sel F P.m hm) (S' : LIDT.CL.Sel F P.m' hm') {X : Type u_2} (check : X → (Fin P.m' → F) → (Fin (P.m' + 6) → F) → Bool) {i : Fin 6} (hi : ↑i = 5) (τ τ' : LIDT.CL.Ty) {x x' : X} {y y' : Pcp.Coord P → F} {u v : Ans P F} (h : accepts S S' check ((Role.oracle, i, τ), x, y) ((Role.oracle, i, τ'), x', y') u v = true) : LIDT.CL.accepts hm' (q6 S' τ y) (q6 S' τ' y') (ans6 u) (ans6 v) = true

The sixth copy's test inside the predicate, for two oracles.