The honest PCP of a pair of answers, slot by slot

The honest strategy of the answer-reduced game (slice P4d of planning/aldous-lyons-track.md) answers with the polynomials of the honest PCP pairPcp of the input answers (cor:functional_viewpoint_final): the oracle with all of them, an isolated player with the two of its own answer. This file records what the strategy's proof needs of them, slot by slot.

• slot_pairPcp_alice, slot_pairPcp_bob: an isolated player's polynomials depend only on its own question and answer, so the oracle's are the player's (the consistency check).
• slot_pairPcp_readable: a readable polynomial depends only on the readable answers.
• slot_pairPcp_affine: a linear polynomial is F₂-affine in the linear answers, the readable ones fixed.
• indDeg_pairPcp, identities_pairPcp: its individual degree is at most 17, and when the input game accepts the answers it satisfies the thirteen checks identically.
• HonestHyp: the hypotheses on the parameters and on each seed's circuit under which that holds at every seed (HonestHyp.identities), what the completeness of the answer-reduced game takes.

Encodings read only the cube

theorem MIPRE.Tailored.AnsRed.encTbl_congr {F : Type u_1} [Field F] {k : ℕ} {t t' : ℕ → F} (h : ∀ c < 2 ^ k, t c = t' c) : encTbl k t = encTbl k t'

theorem MIPRE.Tailored.AnsRed.encB_congr {F : Type u_1} [Field F] {k : ℕ} {t t' : ℕ → Bool} (h : ∀ c < 2 ^ k, t c = t' c) : encB k t = encB k t'

theorem MIPRE.Tailored.AnsRed.encZ_congr {F : Type u_1} [Field F] [CharP F 2] {k : ℕ} {f f' : ℕ → ZMod 2} (h : ∀ c < 2 ^ k, f c = f' c) : encZ k f = encZ k f'

Readable and linear slots of Induce

theorem MIPRE.Tailored.AnsRed.slot_induce_readable {F : Type u_1} [Field F] {L : PcpDims} [CharP F 2] (T : MvPolynomial (Fin L.m) F) (R : RTables) (Lt Lt' : LTables) (s : Slot L) (hs : s.readable = true) : (induce L T R Lt).slot s = (induce L T R Lt').slot s

A readable polynomial of the honest PCP depends only on the readable tables.

theorem MIPRE.Tailored.AnsRed.assignCert_zero {F : Type u_1} [Field F] {k : ℕ} : assignCert 0 = 0

theorem MIPRE.Tailored.AnsRed.slot_induce_affine {F : Type u_1} [Field F] {L : PcpDims} [CharP F 2] (T : MvPolynomial (Fin L.m) F) (R : RTables) (Lt₁ Lt₂ : LTables) (s : Slot L) (hs : s.readable = false) : (induce L T R (Lt₁ + Lt₂)).slot s + (induce L T R 0).slot s = (induce L T R Lt₁).slot s + (induce L T R Lt₂).slot s

A linear polynomial of the honest PCP is F₂-affine in the linear tables.

theorem MIPRE.Tailored.AnsRed.LTables.add_self (X : LTables) : X + X = 0

theorem MIPRE.Tailored.AnsRed.Pcp.IndDeg.slot {F : Type u_1} [Field F] {L : PcpDims} {P : Pcp L F} {d : ℕ} (h : P.IndDeg d) (s : Slot L) (i : Fin s.size) : MvPolynomial.degreeOf i (P.slot s) ≤ d

The degrees of the slots of a PCP of individual degree at most d.

The honest PCP of an answer pair

noncomputable def MIPRE.Tailored.AnsRed.pairPcp {F : Type u_1} [Field F] (L : PcpDims) [CharP F 2] {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (T : MvPolynomial (Fin L.m) F) (Cc : SAT.Circuit) (xq yq : V.Questions n) (a b : Cost.BitStr) : Pcp L F

The honest PCP of an answer pair (a, b) at the questions (x, y) (cor:functional_viewpoint_final), for a circuit polynomial T and a circuit Cc whose formula's witnesses the readable tables carry: Induce of the readable tables of the readable parts and the linear tables of the linear parts.

Equations

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

theorem MIPRE.Tailored.AnsRed.indDeg_pairPcp {F : Type u_1} [Field F] {L : PcpDims} [CharP F 2] {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (T : MvPolynomial (Fin L.m) F) (Cc : SAT.Circuit) (xq yq : V.Questions n) (a b : Cost.BitStr) : (pairPcp L V n T Cc xq yq a b).IndDeg 17

theorem MIPRE.Tailored.AnsRed.slot_pairPcp_readable {F : Type u_1} [Field F] {L : PcpDims} [CharP F 2] {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (T : MvPolynomial (Fin L.m) F) (Cc : SAT.Circuit) (xq yq : V.Questions n) {a a' b b' : Cost.BitStr} (ha : List.take ((V.tgame n).lenR xq) a = List.take ((V.tgame n).lenR xq) a') (hb : List.take ((V.tgame n).lenR yq) b = List.take ((V.tgame n).lenR yq) b') (s : Slot L) (hs : s.readable = true) : (pairPcp L V n T Cc xq yq a b).slot s = (pairPcp L V n T Cc xq yq a' b').slot s

A readable polynomial of the honest PCP depends only on the readable answers.

theorem MIPRE.Tailored.AnsRed.toBits_add {N : ℕ} (u w : Fin N → CL.𝔽₂) : LowDegree.BinaryPolynomial.xorBits (CL.toBits u) (CL.toBits w) = CL.toBits (u + w)

theorem MIPRE.Tailored.AnsRed.honestL_toBits_add {L : PcpDims} {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (xq yq : V.Questions n) (aR bR : Cost.BitStr) {NA NB : ℕ} (u₁ u₂ : Fin NA → CL.𝔽₂) (w₁ w₂ : Fin NB → CL.𝔽₂) : honestL L V n xq yq aR (CL.toBits (u₁ + u₂)) bR (CL.toBits (w₁ + w₂)) = honestL L V n xq yq aR (CL.toBits u₁) bR (CL.toBits w₁) + honestL L V n xq yq aR (CL.toBits u₂) bR (CL.toBits w₂)

theorem MIPRE.Tailored.AnsRed.honestL_toBits_zero {L : PcpDims} {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (xq yq : V.Questions n) (aR bR : Cost.BitStr) (NA NB : ℕ) : honestL L V n xq yq aR (CL.toBits 0) bR (CL.toBits 0) = 0

theorem MIPRE.Tailored.AnsRed.slot_pairPcp_affine {F : Type u_1} [Field F] {L : PcpDims} [CharP F 2] {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (T : MvPolynomial (Fin L.m) F) (Cc : SAT.Circuit) (xq yq : V.Questions n) {aR bR : Cost.BitStr} (haR : List.length aR = (V.tgame n).lenR xq) (hbR : List.length bR = (V.tgame n).lenR yq) {NA NB : ℕ} (u₁ u₂ : Fin NA → CL.𝔽₂) (w₁ w₂ : Fin NB → CL.𝔽₂) (s : Slot L) (hs : s.readable = false) : (pairPcp L V n T Cc xq yq (aR ++ CL.toBits (u₁ + u₂)) (bR ++ CL.toBits (w₁ + w₂))).slot s + (pairPcp L V n T Cc xq yq (aR ++ CL.toBits 0) (bR ++ CL.toBits 0)).slot s = (pairPcp L V n T Cc xq yq (aR ++ CL.toBits u₁) (bR ++ CL.toBits w₁)).slot s + (pairPcp L V n T Cc xq yq (aR ++ CL.toBits u₂) (bR ++ CL.toBits w₂)).slot s

A linear polynomial of the honest PCP is F₂-affine in the linear answers, the readable answers fixed.

The isolated players' polynomials

theorem MIPRE.Tailored.AnsRed.slot_pairPcp_alice {F : Type u_1} [Field F] {L : PcpDims} [CharP F 2] {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (T T' : MvPolynomial (Fin L.m) F) (Cc Cc' : SAT.Circuit) (xq yq yq' : V.Questions n) {a b b' : Cost.BitStr} (ha : (V.tgame n).lenR xq ≤ List.length a) (hR : (V.tgame n).lenR xq ≤ 2 ^ L.ℓ) (s : Slot L) (hs : s ∈ slotsOf L Role.alice) : (pairPcp L V n T Cc xq yq a b).slot s = (pairPcp L V n T' Cc' xq yq' a b').slot s

Alice's polynomials depend only on her question and answer, when her answer carries its readable part and that part fits the table.

theorem MIPRE.Tailored.AnsRed.slot_pairPcp_bob {F : Type u_1} [Field F] {L : PcpDims} [CharP F 2] {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (T T' : MvPolynomial (Fin L.m) F) (Cc Cc' : SAT.Circuit) (xq xq' yq : V.Questions n) (a a' b : Cost.BitStr) (s : Slot L) (hs : s ∈ slotsOf L Role.bob) : (pairPcp L V n T Cc xq yq a b).slot s = (pairPcp L V n T' Cc' xq' yq a' b).slot s

Bob's polynomials depend only on his question and answer.

Accepted answers

theorem MIPRE.Tailored.AnsRed.accepts_halts {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) {xq yq : V.Questions n} {a b : Cost.BitStr} (hacc : (V.tgame n).Accepts xq yq a b) : V.LenDefined n (CL.toBits xq) ∧ V.LenDefined n (CL.toBits yq) ∧ ∃ (cs : List Cost.BitStr), LpIs V.lp n (CL.toBits xq) (CL.toBits yq) (List.take ((V.tgame n).lenR xq) a) (List.take ((V.tgame n).lenR yq) b) cs

An accepted answer pair makes the verifier's programs halt: otherwise the constraints are the one that rejects everything.

theorem MIPRE.Tailored.AnsRed.identities_pairPcp {F : Type u_1} [Field F] {L : PcpDims} [CharP F 2] {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (prm : Cost.PolyTimeFun ℕ (Cost.Unary × Cost.Unary)) (hℓ : List.length (prm.toFun n).1 = L.ℓ) (hdm : List.length (prm.toFun n).2 = L.dm) {Cc : SAT.Circuit} {Tt : ℕ} (hWF : Cc.WellFormed) (hin : Cc.inputs = L.nIn) (hm : Cc.inputs + Cc.size = L.m) (xq yq : V.Questions n) (hdesc : Cc.DescribesWindows (L.ℓ + 1) (L.ℓ + 1) (L.oW + 1) L.r (lstar prm V) n (CL.toBits xq) (CL.toBits yq) Tt) {a b : Cost.BitStr} (hT : (lstar prm V).Accepts n (CL.toBits xq) (CL.toBits yq) (honestA L V n xq yq (List.take ((V.tgame n).lenR xq) a) (List.take ((V.tgame n).lenR yq) b)) (honestB L V n yq (List.take ((V.tgame n).lenR yq) b)) → (lstar prm V).AcceptsWithin n (CL.toBits xq) (CL.toBits yq) (honestA L V n xq yq (List.take ((V.tgame n).lenR xq) a) (List.take ((V.tgame n).lenR yq) b)) (honestB L V n yq (List.take ((V.tgame n).lenR yq) b)) Tt) (hTlen : 2 ^ L.ℓ + 2 ^ L.oW ≤ Tt) (hRx : (V.tgame n).lenR xq ≤ 2 ^ L.ℓ) (hLx : (V.tgame n).lenL xq ≤ 2 ^ L.ℓ) (hRy : (V.tgame n).lenR yq ≤ 2 ^ L.ℓ) (hLy : (V.tgame n).lenL yq ≤ 2 ^ L.ℓ) (hD : ((V.tgame n).cons xq yq (List.take ((V.tgame n).lenR xq) a) (List.take ((V.tgame n).lenR yq) b)).length * (2 ^ L.ℓ + 2 ^ L.ℓ) + (2 ^ L.ℓ + 2 ^ L.ℓ) ≤ 2 ^ L.dm) (hacc : (V.tgame n).Accepts xq yq a b) : Pcp.Identities ((MvPolynomial.rename (Fin.cast hm)) Cc.finiteArith) (pairPcp L V n ((MvPolynomial.rename (Fin.cast hm)) Cc.finiteArith) Cc xq yq a b)

The honest PCP of an accepted answer pair satisfies the thirteen checks identically (identities_honest), at parameters the lengths fit, for a circuit that describes the output indicator through the windows within a time L* meets.

At every seed

noncomputable def MIPRE.Tailored.AnsRed.circOf {F : Type u_1} [Field F] (L : PcpDims) {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (Cc : V.Questions n → SAT.Circuit) (hm : ∀ (z : V.Questions n), (Cc z).inputs + (Cc z).size = L.m) (z : V.Questions n) : MvPolynomial (Fin L.m) F

The circuit polynomial of each seed: the arithmetization of its circuit, on the PCP's variables.

Equations

• MIPRE.Tailored.AnsRed.circOf L V n Cc hm z = (MvPolynomial.rename (Fin.cast ⋯)) (Cc z).finiteArith

structure MIPRE.Tailored.AnsRed.HonestHyp (L : PcpDims) {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (prm : Cost.PolyTimeFun ℕ (Cost.Unary × Cost.Unary)) (Cc : V.Questions n → SAT.Circuit) (Tt : ℕ) : Prop

The hypotheses of the honest PCPs at every seed: the parameters fit the lengths and the constraints of the n-th game, and each seed's circuit is well formed, has the PCP's inputs, and describes the output indicator L* through the windows at the seed's question pair, within a time L* meets on the honest strings.

• hℓ : List.length (prm.toFun n).1 = L.ℓ
• hdm : List.length (prm.toFun n).2 = L.dm
• wf (z : V.Questions n) : (Cc z).WellFormed
• inputs (z : V.Questions n) : (Cc z).inputs = L.nIn
• desc (z : V.Questions n) : (Cc z).DescribesWindows (L.ℓ + 1) (L.ℓ + 1) (L.oW + 1) L.r (lstar prm V) n (CL.toBits ((V.sampler.cl n Player.alice).eval z)) (CL.toBits ((V.sampler.cl n Player.bob).eval z)) Tt
• time (z : Fin (V.sampler.dim n) → CL.𝔽₂) (aR bR : Cost.BitStr) : (lstar prm V).Accepts n (CL.toBits ((V.sampler.cl n Player.alice).eval z)) (CL.toBits ((V.sampler.cl n Player.bob).eval z)) (honestA L V n ((V.sampler.cl n Player.alice).eval z) ((V.sampler.cl n Player.bob).eval z) aR bR) (honestB L V n ((V.sampler.cl n Player.bob).eval z) bR) → (lstar prm V).AcceptsWithin n (CL.toBits ((V.sampler.cl n Player.alice).eval z)) (CL.toBits ((V.sampler.cl n Player.bob).eval z)) (honestA L V n ((V.sampler.cl n Player.alice).eval z) ((V.sampler.cl n Player.bob).eval z) aR bR) (honestB L V n ((V.sampler.cl n Player.bob).eval z) bR) Tt
• hTlen : 2 ^ L.ℓ + 2 ^ L.oW ≤ Tt
• lenR (x : V.Questions n) : (V.tgame n).lenR x ≤ 2 ^ L.ℓ
• lenL (x : V.Questions n) : (V.tgame n).lenL x ≤ 2 ^ L.ℓ
• cons (x y : V.Questions n) (aR bR : Cost.BitStr) : List.length aR ≤ (V.tgame n).lenR x → List.length bR ≤ (V.tgame n).lenR y → ((V.tgame n).cons x y aR bR).length * (2 ^ L.ℓ + 2 ^ L.ℓ) + (2 ^ L.ℓ + 2 ^ L.ℓ) ≤ 2 ^ L.dm

theorem MIPRE.Tailored.AnsRed.HonestHyp.identities {F : Type u_1} [Field F] {L : PcpDims} [CharP F 2] {ℓV : ℕ} {V : TailoredVerifier ℓV} {n : ℕ} {prm : Cost.PolyTimeFun ℕ (Cost.Unary × Cost.Unary)} {Cc : V.Questions n → SAT.Circuit} {Tt : ℕ} (H : HonestHyp L V n prm Cc Tt) (hm : ∀ (z : V.Questions n), (Cc z).inputs + (Cc z).size = L.m) (z : V.Questions n) {a b : Cost.BitStr} (hacc : (V.tgame n).Accepts ((V.sampler.cl n Player.alice).eval z) ((V.sampler.cl n Player.bob).eval z) a b) : Pcp.Identities (circOf L V n Cc hm z) (pairPcp L V n (circOf L V n Cc hm z) (Cc z) ((V.sampler.cl n Player.alice).eval z) ((V.sampler.cl n Player.bob).eval z) a b)

At every seed, the honest PCP of an accepted answer pair satisfies the checks identically.