The input strategy's answer bits

The honest strategy of the introspection verifier runs the input's strategy, as the synchronous strategy of lem:zpc-pcc (PermStrategy.toSync): at a question x it measures answer strings, charging those of length len x with the Fourier transform of the observables at x. The introspection verifier's answers carry the input's answer, re-encoded (padded), so the bit observables of the honest strategy include those of ansProj along an encoding of the input's answers. This file computes them: a bit that copies the j-th answer bit has observable U(x, j) (encObs_ansProj_bit), and a constant bit has observable ±1 (encObs_ansProj_const).

theorem MIPRE.Tailored.PermStrategy.encObs_ansProj {X : Type u_1} [Fintype X] {G : TailoredGame X} (S : PermStrategy G) {T k : ℕ} (x : X) (hT : G.len x ≤ T) (enc : Verifier.Answers T → Fin k → Bool) (i : Fin k) : encObs (S.ansProj T x) enc i = pvmObs (S.proj x) fun (v : Fin (G.len x) → Bool) => bitSign (enc (ofVec hT v) i)

The bit observables of the measurement on answer strings, as weightings of the measurement on answer vectors.

theorem MIPRE.Tailored.PermStrategy.encObs_ansProj_bit {X : Type u_1} [Fintype X] {G : TailoredGame X} (S : PermStrategy G) {T k : ℕ} (x : X) (hT : G.len x ≤ T) (enc : Verifier.Answers T → Fin k → Bool) (i : Fin k) (j : Fin (G.len x)) (h : ∀ (v : Fin (G.len x) → Bool), enc (ofVec hT v) i = v j) : encObs (S.ansProj T x) enc i = S.U x j

A bit copying the j-th answer bit has observable U(x, j).

theorem MIPRE.Tailored.PermStrategy.encObs_ansProj_const {X : Type u_1} [Fintype X] {G : TailoredGame X} (S : PermStrategy G) {T k : ℕ} (x : X) (hT : G.len x ≤ T) (enc : Verifier.Answers T → Fin k → Bool) (i : Fin k) (c : Bool) (h : ∀ (v : Fin (G.len x) → Bool), enc (ofVec hT v) i = c) : encObs (S.ansProj T x) enc i = bitSign c • 1

A constant bit has observable ±1.