The answer bits of the honest answers

The honest strategy of the answer-reduced game data-processes the measurements of a Z-aligned permutation strategy of the input (slice P4d of planning/aldous-lyons-track.md). Its answer bits are signed permutations, diagonal at the readable bits, because of how they depend on the input answers (cor:encodings, II:1150):

• a readable bit reads only the readable codewords (getD_honestBits_readable), so it is a function of the readable input bits (getD_pairPcp_readable);
• every bit is, the readable input bits fixed, F₂-affine in the linear input bits (ofBool_getD_pairPcp_affine): the honest PCP is affine in the linear tables, and its values, restrictions and the canonical bits of field elements are additive.

ControlledBits turns these into the bit properties: isXBit_diag, isZBit_diag for an isolated player, who measures the input strategy at its question, and isXBit_pair, isZBit_pair for the oracle, who measures the input strategy at both questions of its seed.

The bits of an honest answer

theorem MIPRE.Tailored.AnsRed.Typed.getD_honestBits {t : ℕ} {ht : 1 ≤ t} {j : ℕ} (d : ℕ) (hM : 2 ^ j ∣ Fintype.card (Fq t ht)) (S : LIDT.CL.Ty) {k : ℕ} (G : Fin k → MvPolynomial (Fin (2 ^ j)) (Fq t ht)) (q : LIDT.CL.Question (Fq t ht) (2 ^ j)) {i : ℕ} (hi : i < k * ncoef j d S * t) : List.getD (honestBits d hM S G q) i false = decide ((SAT.shoupCoordinateEquiv t ht) (honestCoef hM G q (i / (ncoef j d S * t)) (i / t % ncoef j d S)) ⟨i % t, ⋯⟩ = 1)

theorem MIPRE.Tailored.AnsRed.Typed.getD_honestBits_of_le {t : ℕ} {ht : 1 ≤ t} {j : ℕ} (d : ℕ) (hM : 2 ^ j ∣ Fintype.card (Fq t ht)) (S : LIDT.CL.Ty) {k : ℕ} (G : Fin k → MvPolynomial (Fin (2 ^ j)) (Fq t ht)) (q : LIDT.CL.Question (Fq t ht) (2 ^ j)) {i : ℕ} (hi : k * ncoef j d S * t ≤ i) : List.getD (honestBits d hM S G q) i false = false

theorem MIPRE.Tailored.AnsRed.Typed.honestCoef_add {t : ℕ} {ht : 1 ≤ t} {j : ℕ} (hM : 2 ^ j ∣ Fintype.card (Fq t ht)) {k : ℕ} (G G' : Fin k → MvPolynomial (Fin (2 ^ j)) (Fq t ht)) (q : LIDT.CL.Question (Fq t ht) (2 ^ j)) (c e : ℕ) : honestCoef hM (G + G') q c e = honestCoef hM G q c e + honestCoef hM G' q c e

theorem MIPRE.Tailored.AnsRed.Typed.ofBool_getD_honestBits_affine {t : ℕ} {ht : 1 ≤ t} {j : ℕ} (d : ℕ) (hM : 2 ^ j ∣ Fintype.card (Fq t ht)) (S : LIDT.CL.Ty) {k : ℕ} {G₁₂ G₀ G₁ G₂ : Fin k → MvPolynomial (Fin (2 ^ j)) (Fq t ht)} (hG : ∀ (c : Fin k), G₁₂ c + G₀ c = G₁ c + G₂ c) (q : LIDT.CL.Question (Fq t ht) (2 ^ j)) (i : ℕ) : LowDegree.ofBool (List.getD (honestBits d hM S G₁₂ q) i false) + LowDegree.ofBool (List.getD (honestBits d hM S G₀ q) i false) = LowDegree.ofBool (List.getD (honestBits d hM S G₁ q) i false) + LowDegree.ofBool (List.getD (honestBits d hM S G₂ q) i false)

A bit of honest answers is F₂-affine in the codewords.

theorem MIPRE.Tailored.AnsRed.Typed.getD_honestBits_readable {t : ℕ} {ht : 1 ≤ t} {j : ℕ} (d : ℕ) (hM : 2 ^ j ∣ Fintype.card (Fq t ht)) {L : PcpDims} (hLM : L.m ≤ 2 ^ j) (r : Role) (S : LIDT.CL.Ty) {P P' : Pcp L (Fq t ht)} (h : ∀ (s : Slot L), s.readable = true → P.slot s = P'.slot s) (q : LIDT.CL.Question (Fq t ht) (2 ^ j)) {i : ℕ} (hi : i < lenR t j d L (r, S)) : List.getD (honestBits d hM S (ldPolys L hLM P r) q) i false = List.getD (honestBits d hM S (ldPolys L hLM P' r) q) i false

A readable bit of an honest answer reads only the readable codewords.

theorem MIPRE.Tailored.AnsRed.Typed.getD_pairPcp_readable {t : ℕ} {ht : 1 ≤ t} {j : ℕ} (d : ℕ) (hM : 2 ^ j ∣ Fintype.card (Fq t ht)) {L : PcpDims} (hLM : L.m ≤ 2 ^ j) {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (r : Role) (S : LIDT.CL.Ty) (Tc : MvPolynomial (Fin L.m) (Fq t ht)) (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') (q : LIDT.CL.Question (Fq t ht) (2 ^ j)) {i : ℕ} (hi : i < lenR t j d L (r, S)) : List.getD (honestBits d hM S (ldPolys L hLM (pairPcp L V n Tc Cc xq yq a b) r) q) i false = List.getD (honestBits d hM S (ldPolys L hLM (pairPcp L V n Tc Cc xq yq a' b') r) q) i false

The readable bits of an honest answer depend only on the readable input bits.

theorem MIPRE.Tailored.AnsRed.Typed.take_append_of_length {aR : Cost.BitStr} {k : ℕ} (h : List.length aR = k) (l : Cost.BitStr) : List.take k (aR ++ l) = aR

theorem MIPRE.Tailored.AnsRed.Typed.ldPolys_pairPcp_affine {t : ℕ} {ht : 1 ≤ t} {j : ℕ} {L : PcpDims} (hLM : L.m ≤ 2 ^ j) {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (r : Role) (Tc : MvPolynomial (Fin L.m) (Fq t ht)) (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.𝔽₂) (c : Fin (slotsOf L r).length) : ldPolys L hLM (pairPcp L V n Tc Cc xq yq (aR ++ CL.toBits (u₁ + u₂)) (bR ++ CL.toBits (w₁ + w₂))) r c + ldPolys L hLM (pairPcp L V n Tc Cc xq yq (aR ++ CL.toBits 0) (bR ++ CL.toBits 0)) r c = ldPolys L hLM (pairPcp L V n Tc Cc xq yq (aR ++ CL.toBits u₁) (bR ++ CL.toBits w₁)) r c + ldPolys L hLM (pairPcp L V n Tc Cc xq yq (aR ++ CL.toBits u₂) (bR ++ CL.toBits w₂)) r c

The codewords of the honest PCP are F₂-affine in the linear input bits.

theorem MIPRE.Tailored.AnsRed.Typed.ofBool_getD_pairPcp_affine {t : ℕ} {ht : 1 ≤ t} {j : ℕ} (d : ℕ) (hM : 2 ^ j ∣ Fintype.card (Fq t ht)) {L : PcpDims} (hLM : L.m ≤ 2 ^ j) {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (r : Role) (S : LIDT.CL.Ty) (Tc : MvPolynomial (Fin L.m) (Fq t ht)) (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.𝔽₂) (q : LIDT.CL.Question (Fq t ht) (2 ^ j)) (i : ℕ) : LowDegree.ofBool (List.getD (honestBits d hM S (ldPolys L hLM (pairPcp L V n Tc Cc xq yq (aR ++ CL.toBits (u₁ + u₂)) (bR ++ CL.toBits (w₁ + w₂))) r) q) i false) + LowDegree.ofBool (List.getD (honestBits d hM S (ldPolys L hLM (pairPcp L V n Tc Cc xq yq (aR ++ CL.toBits 0) (bR ++ CL.toBits 0)) r) q) i false) = LowDegree.ofBool (List.getD (honestBits d hM S (ldPolys L hLM (pairPcp L V n Tc Cc xq yq (aR ++ CL.toBits u₁) (bR ++ CL.toBits w₁)) r) q) i false) + LowDegree.ofBool (List.getD (honestBits d hM S (ldPolys L hLM (pairPcp L V n Tc Cc xq yq (aR ++ CL.toBits u₂) (bR ++ CL.toBits w₂)) r) q) i false)

Every bit of an honest answer is F₂-affine in the linear input bits, the readable ones fixed.

Reading an answer through its readable and linear bits

theorem MIPRE.Tailored.AnsRed.Typed.decide_ofBool_eq_one (b : Bool) : decide (LowDegree.ofBool b = 1) = b

theorem MIPRE.Tailored.AnsRed.Typed.take_eq_ofFn {a : Cost.BitStr} {R : ℕ} (h : R ≤ List.length a) : List.take R a = List.take R (List.ofFn fun (m : Fin R) => List.getD a (↑m) false)

The first R bits of an answer of length at least R.

theorem MIPRE.Tailored.AnsRed.Typed.eq_ofFn_append_toBits {a : Cost.BitStr} {R N : ℕ} (h : List.length a = R + N) : a = (List.ofFn fun (m : Fin R) => List.getD a (↑m) false) ++ CL.toBits fun (m : Fin N) => LowDegree.ofBool (List.getD a (R + ↑m) false)

An answer of length R + N is its first R bits followed by the rest.

The bits at an isolated player

def MIPRE.Tailored.AnsRed.Typed.rdBits (lR : ℕ) (a : Cost.BitStr) : Fin lR → Bool

The readable bits of an answer at a question.

Equations

• MIPRE.Tailored.AnsRed.Typed.rdBits lR a m = List.getD a (↑m) false

def MIPRE.Tailored.AnsRed.Typed.lnBits (lR lL : ℕ) (a : Cost.BitStr) : Fin lL → Bool

The linear bits of an answer at a question.

Equations

• MIPRE.Tailored.AnsRed.Typed.lnBits lR lL a m = List.getD a (lR + ↑m) false

theorem MIPRE.Tailored.AnsRed.Typed.isXBit_diag {t : ℕ} {ht : 1 ≤ t} {j : ℕ} (d : ℕ) (hM : 2 ^ j ∣ Fintype.card (Fq t ht)) {L : PcpDims} (hLM : L.m ≤ 2 ^ j) {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (SV : PermStrategy (V.tgame n).doubled) (p : Bool × V.Questions n) (r : Role) (S : LIDT.CL.Ty) (Tc : MvPolynomial (Fin L.m) (Fq t ht)) (Cc₀ : SAT.Circuit) (q : LIDT.CL.Question (Fq t ht) (2 ^ j)) (i : ℕ) : IsXBit (SV.toSync.P.M p) fun (a : Verifier.Answers (V.tgame n).maxLen) => List.getD (honestBits d hM S (ldPolys L hLM (pairPcp L V n Tc Cc₀ p.2 p.2 ↑a ↑a) r) q) i false

The bits of an isolated player's honest answer are X-bits of the input strategy's measurement at its question: for each value of its readable bits, affine in its linear bits.

theorem MIPRE.Tailored.AnsRed.Typed.isZBit_diag {t : ℕ} {ht : 1 ≤ t} {j : ℕ} (d : ℕ) (hM : 2 ^ j ∣ Fintype.card (Fq t ht)) {L : PcpDims} (hLM : L.m ≤ 2 ^ j) {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (SV : PermStrategy (V.tgame n).doubled) (p : Bool × V.Questions n) (r : Role) (S : LIDT.CL.Ty) (Tc : MvPolynomial (Fin L.m) (Fq t ht)) (Cc₀ : SAT.Circuit) (q : LIDT.CL.Question (Fq t ht) (2 ^ j)) {i : ℕ} (hi : i < lenR t j d L (r, S)) : IsZBit (SV.toSync.P.M p) fun (a : Verifier.Answers (V.tgame n).maxLen) => List.getD (honestBits d hM S (ldPolys L hLM (pairPcp L V n Tc Cc₀ p.2 p.2 ↑a ↑a) r) q) i false

The readable bits of an isolated player's honest answer are Z-bits of the input strategy's measurement at its question: functions of its readable bits.

The bits at the oracle

noncomputable def MIPRE.Tailored.AnsRed.Typed.jointM {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (SV : PermStrategy (V.tgame n).doubled) (z : V.Questions n) : Verifier.Answers (V.tgame n).maxLen × Verifier.Answers (V.tgame n).maxLen → Matrix (Fin SV.toSync.d) (Fin SV.toSync.d) ℂ

The measurement of an oracle at a seed: the input strategy's measurements at both questions of the seed, jointly.

Equations

• MIPRE.Tailored.AnsRed.Typed.jointM V n SV z ab = SV.toSync.P.M (false, MIPRE.Tailored.AnsRed.Typed.qA V n z) ab.1 * SV.toSync.P.M (true, MIPRE.Tailored.AnsRed.Typed.qB V n z) ab.2

theorem MIPRE.Tailored.AnsRed.Typed.doubled_mu_pos_seed {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (z : V.Questions n) : 0 < (V.tgame n).toGame.doubled.μ (false, qA V n z) (true, qB V n z)

theorem MIPRE.Tailored.AnsRed.Typed.isPVMIn_jointM {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (SV : PermStrategy (V.tgame n).doubled) (z : V.Questions n) : IsPVMIn (jointM V n SV z)

theorem MIPRE.Tailored.AnsRed.Typed.jointM_ne_zero {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) {SV : PermStrategy (V.tgame n).doubled} {z : V.Questions n} {ab : Verifier.Answers (V.tgame n).maxLen × Verifier.Answers (V.tgame n).maxLen} (h : jointM V n SV z ab ≠ 0) : SV.toSync.P.M (false, qA V n z) ab.1 ≠ 0 ∧ SV.toSync.P.M (true, qB V n z) ab.2 ≠ 0

theorem MIPRE.Tailored.AnsRed.Typed.isZBit_jointM_fst {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (SV : PermStrategy (V.tgame n).doubled) (z : V.Questions n) {g : Verifier.Answers (V.tgame n).maxLen → Bool} (hg : IsZBit (SV.toSync.P.M (false, qA V n z)) g) : IsZBit (jointM V n SV z) fun (ab : Verifier.Answers (V.tgame n).maxLen × Verifier.Answers (V.tgame n).maxLen) => g ab.1

theorem MIPRE.Tailored.AnsRed.Typed.isZBit_jointM_snd {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (SV : PermStrategy (V.tgame n).doubled) (z : V.Questions n) {g : Verifier.Answers (V.tgame n).maxLen → Bool} (hg : IsZBit (SV.toSync.P.M (true, qB V n z)) g) : IsZBit (jointM V n SV z) fun (ab : Verifier.Answers (V.tgame n).maxLen × Verifier.Answers (V.tgame n).maxLen) => g ab.2

theorem MIPRE.Tailored.AnsRed.Typed.isXBit_jointM_fst {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (SV : PermStrategy (V.tgame n).doubled) (z : V.Questions n) {g : Verifier.Answers (V.tgame n).maxLen → Bool} (hg : IsXBit (SV.toSync.P.M (false, qA V n z)) g) : IsXBit (jointM V n SV z) fun (ab : Verifier.Answers (V.tgame n).maxLen × Verifier.Answers (V.tgame n).maxLen) => g ab.1

theorem MIPRE.Tailored.AnsRed.Typed.isXBit_jointM_snd {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (SV : PermStrategy (V.tgame n).doubled) (z : V.Questions n) {g : Verifier.Answers (V.tgame n).maxLen → Bool} (hg : IsXBit (SV.toSync.P.M (true, qB V n z)) g) : IsXBit (jointM V n SV z) fun (ab : Verifier.Answers (V.tgame n).maxLen × Verifier.Answers (V.tgame n).maxLen) => g ab.2

theorem MIPRE.Tailored.AnsRed.Typed.isXBit_pair {t : ℕ} {ht : 1 ≤ t} {j : ℕ} (d : ℕ) (hM : 2 ^ j ∣ Fintype.card (Fq t ht)) {L : PcpDims} (hLM : L.m ≤ 2 ^ j) {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (SV : PermStrategy (V.tgame n).doubled) (z : V.Questions n) (S : LIDT.CL.Ty) (Tc : MvPolynomial (Fin L.m) (Fq t ht)) (Cc₀ : SAT.Circuit) (q : LIDT.CL.Question (Fq t ht) (2 ^ j)) (i : ℕ) : IsXBit (jointM V n SV z) fun (ab : Verifier.Answers (V.tgame n).maxLen × Verifier.Answers (V.tgame n).maxLen) => List.getD (honestBits d hM S (ldPolys L hLM (pairPcp L V n Tc Cc₀ (qA V n z) (qB V n z) ↑ab.1 ↑ab.2) Role.oracle) q) i false

The bits of the oracle's honest answer are X-bits of its joint measurement: for each value of the readable bits of both input answers, affine in their linear bits.

theorem MIPRE.Tailored.AnsRed.Typed.isZBit_pair {t : ℕ} {ht : 1 ≤ t} {j : ℕ} (d : ℕ) (hM : 2 ^ j ∣ Fintype.card (Fq t ht)) {L : PcpDims} (hLM : L.m ≤ 2 ^ j) {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (SV : PermStrategy (V.tgame n).doubled) (z : V.Questions n) (S : LIDT.CL.Ty) (Tc : MvPolynomial (Fin L.m) (Fq t ht)) (Cc₀ : SAT.Circuit) (q : LIDT.CL.Question (Fq t ht) (2 ^ j)) {i : ℕ} (hi : i < lenR t j d L (Role.oracle, S)) : IsZBit (jointM V n SV z) fun (ab : Verifier.Answers (V.tgame n).maxLen × Verifier.Answers (V.tgame n).maxLen) => List.getD (honestBits d hM S (ldPolys L hLM (pairPcp L V n Tc Cc₀ (qA V n z) (qB V n z) ↑ab.1 ↑ab.2) Role.oracle) q) i false

The readable bits of the oracle's honest answer are Z-bits of its joint measurement: functions of the readable bits of both input answers.