ZPC completeness of the tailored question reduction: the honest strategy

Phase 3c of planning/aldous-lyons-track.md (issue #281). The tailored presentation of the introspection verifier seven (MIPRE.Tailored.Intro.Complete.hasPerfectZPC_tpresented) has a perfect permutation strategy as soon as the reference verifier's typed game rawGame has a perfect PCC strategy that charges only encodable answers and whose bit observables along the padded layout enc are signed permutations, diagonal at the readable bits. This file proves that the honest strategy HonestChain.raw is one, for every input whose strategy has signed-permutation answer bits, diagonal at the readable ones (the input of a tailored verifier):

• raw_isXBit (hperm): every bit of enc at every typed question is a signed permutation;
• raw_isDiag (hdiag): the readable ones, below Typed.lenR, are diagonal;
• raw_support (hsupp): a byte answer with a nonzero projection satisfies Complete.okT: it is well formed for the layout (Complete.OkL), and its register satisfies the readable conditions (Typed.readOK) — the input's answer fits the cutoff, the prefix guard of Read and Hide, and Introspect's register is a source output.

The input is any perfect PCC strategy RW of the normal form verifier W at index 2^n whose answers at a question have the lengths the tailored verifier V assigns to it and whose answer bits are signed permutations, diagonal below the readable length (honest_zpc). inputSync is such a strategy, built by lem:zpc-pcc from a permutation strategy of V (PermStrategy.toSync, extended by zero to the answers of V.ofTNFV U), and inputSyncT is the same strategy on the game of V.ofTNFVT U, which is that of V.ofTNFV U (honest_zpc_ofTNFVT).

theorem MIPRE.Tailored.Intro.HonestChain.pauliRead_eq_true {T : QLD.Ty} (h : pauliRead T = true) : T = QLD.Ty.pauli QLD.Bas.Z

theorem MIPRE.Tailored.Intro.HonestChain.canonical_bits {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (he : Even c) (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (V : TailoredVerifier 7) (hc : 2 ≤ c) (hlen : ∀ (p : Bool × W.Questions (2 ^ n)) (a : Verifier.Answers ((2 ^ n) ^ lam)), RW.P.M p a ≠ 0 → List.length ↑a = V.lenOf (2 ^ n) (CL.toBits p.2) false + V.lenOf (2 ^ n) (CL.toBits p.2) true) (hX : ∀ (p : Bool × W.Questions (2 ^ n)) (j : ℕ), IsXBit (RW.P.M p) fun (a : Verifier.Answers ((2 ^ n) ^ lam)) => List.getD (↑a) j false) (hZ : ∀ (p : Bool × W.Questions (2 ^ n)), ∀ j < V.lenOf (2 ^ n) (CL.toBits p.2) false, IsZBit (RW.P.M p) fun (a : Verifier.Answers ((2 ^ n) ^ lam)) => List.getD (↑a) j false) (q : Bool × CL.Detyping.Question Introspection.DecisionKernel.Label (Fin (Introspection.PauliSampler.dimension c lam n))) (i : ℕ) : IsXBit ((canonical W RW ⋯ he hs).P.M q) (fbit hc ((2 ^ n) ^ lam) (srcSplitR V W hs) q.2.1 i) ∧ (i < Typed.lenR (Introspection.SourceCompiler.fieldBits c lam n) (Introspection.PauliSamplerParameters.selectorBits c lam n) ((2 ^ n) ^ lam) q.2.1 → IsZBit ((canonical W RW ⋯ he hs).P.M q) (fbit hc ((2 ^ n) ^ lam) (srcSplitR V W hs) q.2.1 i))

Every bit of the honest measurement at a typed question is a signed permutation, and the readable ones are diagonal.

The honest strategy of the typed game

theorem MIPRE.Tailored.Intro.HonestChain.bitObs_mergeAnswersByQuestion {X : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B] {G : SynchronousGame X A} (S : SyncStrategy G) (H : SynchronousGame X B) (f : X → A → B) (x : X) (g : B → Bool) : (pvmObs ((S.mergeAnswersByQuestion H f).P.M x) fun (b : B) => bitSign (g b)) = bitObs (S.P.M x) (g ∘ f x)

theorem MIPRE.Tailored.Intro.HonestChain.raw_isXBit {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (he : Even c) (V : TailoredVerifier 7) (hc : 2 ≤ c) (hlen : ∀ (p : Bool × W.Questions (2 ^ n)) (a : Verifier.Answers ((2 ^ n) ^ lam)), RW.P.M p a ≠ 0 → List.length ↑a = V.lenOf (2 ^ n) (CL.toBits p.2) false + V.lenOf (2 ^ n) (CL.toBits p.2) true) (hX : ∀ (p : Bool × W.Questions (2 ^ n)) (j : ℕ), IsXBit (RW.P.M p) fun (a : Verifier.Answers ((2 ^ n) ^ lam)) => List.getD (↑a) j false) (hZ : ∀ (p : Bool × W.Questions (2 ^ n)), ∀ j < V.lenOf (2 ^ n) (CL.toBits p.2) false, IsZBit (RW.P.M p) fun (a : Verifier.Answers ((2 ^ n) ^ lam)) => List.getD (↑a) j false) (U : Cost.ClockedUniversalMachine) (hW : W.IsBounded lam) (hn : 1 ≤ n) (q : Bool × CL.Detyping.Question Introspection.DecisionKernel.Label (Fin (Introspection.PauliSampler.dimension c lam n))) (i : ℕ) : IsSignedPerm (pvmObs ((raw W RW hc he U hW hn).P.M q) fun (a : Verifier.Answers ((Introspection.DecisionCompiler.constantCutoff (Introspection.DecisionCompiler.outerBound c lam n)).outer n)) => bitSign (List.getD (Complete.encT V W c lam ⋯ q.2 a) i false))

hperm: every bit of the padded layout is a signed permutation observable of the honest strategy.

theorem MIPRE.Tailored.Intro.HonestChain.raw_isDiag {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (he : Even c) (V : TailoredVerifier 7) (hc : 2 ≤ c) (hlen : ∀ (p : Bool × W.Questions (2 ^ n)) (a : Verifier.Answers ((2 ^ n) ^ lam)), RW.P.M p a ≠ 0 → List.length ↑a = V.lenOf (2 ^ n) (CL.toBits p.2) false + V.lenOf (2 ^ n) (CL.toBits p.2) true) (hX : ∀ (p : Bool × W.Questions (2 ^ n)) (j : ℕ), IsXBit (RW.P.M p) fun (a : Verifier.Answers ((2 ^ n) ^ lam)) => List.getD (↑a) j false) (hZ : ∀ (p : Bool × W.Questions (2 ^ n)), ∀ j < V.lenOf (2 ^ n) (CL.toBits p.2) false, IsZBit (RW.P.M p) fun (a : Verifier.Answers ((2 ^ n) ^ lam)) => List.getD (↑a) j false) (U : Cost.ClockedUniversalMachine) (hW : W.IsBounded lam) (hn : 1 ≤ n) (q : Bool × CL.Detyping.Question Introspection.DecisionKernel.Label (Fin (Introspection.PauliSampler.dimension c lam n))) (i : ℕ) (hi : i < Typed.lenR (Introspection.SourceCompiler.fieldBits c lam n) (Introspection.PauliSamplerParameters.selectorBits c lam n) ((2 ^ n) ^ lam) q.2.1) : (pvmObs ((raw W RW hc he U hW hn).P.M q) fun (a : Verifier.Answers ((Introspection.DecisionCompiler.constantCutoff (Introspection.DecisionCompiler.outerBound c lam n)).outer n)) => bitSign (List.getD (Complete.encT V W c lam ⋯ q.2 a) i false)).IsDiag

hdiag: the readable bits are diagonal.

The support

theorem MIPRE.Tailored.Intro.HonestChain.mergeAnswersByQuestion_ne_zero {X : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B] {G : SynchronousGame X A} (S : SyncStrategy G) (H : SynchronousGame X B) (f : X → A → B) (x : X) (b : B) (h : (S.mergeAnswersByQuestion H f).P.M x b ≠ 0) : ∃ (a : A), f x a = b ∧ S.P.M x a ≠ 0

theorem MIPRE.Tailored.Intro.HonestChain.length_answerBits {k m d : ℕ} (E : SAT.BinField k) (q : QLD.Question E.carrier m) (a : QLD.Answer E.carrier m d) (h : q.fmtOk a = true) : List.length (QLD.PauliAnswerProgram.answerBits E a) = QLD.PauliAnswerProgram.count q.ty m d * QLD.PauliAnswerProgram.width q.ty k

theorem MIPRE.Tailored.Intro.HonestChain.binaryDecode_ty {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m t : ℕ} (π : F ≃ F) (b : Module.Basis (Fin t) (ZMod 2) F) (T : QLD.Ty) (x : Fin ((3 * m + 3) * t) → ZMod 2) : (QLD.PauliCL.ExplicitSeed.binaryDecode π b T x).ty = T

theorem MIPRE.Tailored.Intro.HonestChain.op_inl_eq_zero {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m d ℓ t : ℕ} [NeZero m] (L : Bool → CL.CLFun (ZMod 2) (Introspection.BinaryComplete.Coord m t) ℓ) (D : Introspection.BinaryComplete.Seed m t → Introspection.BinaryComplete.Seed m t → A → A → Bool) (R : SyncStrategy (Introspection.Honest.sourceGame L D).doubled) (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (T : QLD.Ty) (x : Fin ((3 * m + 3) * t) → ZMod 2) (a : Introspection.BinaryComplete.Answer F A m t d) (ha : ∀ (p : QLD.Answer F m d), a ≠ Introspection.ParsedAnswer.pauli p) : Introspection.BinaryComplete.op L D R hm b hL (Sum.inl T, x) a = 0

The binary operator at a Pauli label vanishes off the Pauli answers.

theorem MIPRE.Tailored.Intro.HonestChain.canonical_pauli_shape {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (he : Even c) (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (hc1 : 1 ≤ c) (w' : Bool) (T : QLD.Ty) (z : Fin (Introspection.PauliSampler.dimension c lam n) → CL.𝔽₂) (a : Introspection.CanonicalComplete.Answer c lam n) (ha : (canonical W RW hc1 he hs).P.M (w', Sum.inl T, z) a ≠ 0) : ∃ (x : QLD.Answer (Introspection.CanonicalGame.field c lam n).carrier (Introspection.SourceCompiler.registerPower c lam n) 1), a = Introspection.ParsedAnswer.pauli x

At a Pauli label the honest measurement charges only Pauli answers.

theorem MIPRE.Tailored.Intro.HonestChain.canonical_aux_ne_zero {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (he : Even c) (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (hc1 : 1 ≤ c) (w' : Bool) (t : Introspection.AuxType 7 × Bool) (z : Fin (Introspection.PauliSampler.dimension c lam n) → CL.𝔽₂) (a : Introspection.CanonicalComplete.Answer c lam n) (ha : (canonical W RW hc1 he hs).P.M (w', Sum.inr t, z) a ≠ 0) : Introspection.Honest.auxOp (family W hs) (decider W hs) (reindexed W RW hs) ⋯ t ((Introspection.AuxiliaryQuotient.answerEquiv (Introspection.CanonicalGame.numbering c lam n)) a) ≠ 0

The honest auxiliary measurements' support

theorem MIPRE.Tailored.Intro.HonestChain.parsedCoreOp_support {ι : Type u_1} {A : Type u_2} {PA : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] [Fintype PA] {ℓ : ℕ} (L : Bool → CL.CLFun CL.𝔽₂ ι ℓ) (D : (ι → CL.𝔽₂) → (ι → CL.𝔽₂) → A → A → Bool) (R : SyncStrategy (Introspection.Honest.sourceGame L D).doubled) (t : Introspection.Honest.CoreType) (b : Introspection.ParsedAnswer (ι → CL.𝔽₂) A PA) (h : Introspection.Honest.parsedCoreOp L D R t b ≠ 0) : ∃ (y : ι → CL.𝔽₂) (α : A), b = Introspection.ParsedAnswer.pair y α ∧ R.P.M (t.2, Introspection.Honest.originalQuestion L t y) α ≠ 0

theorem MIPRE.Tailored.Intro.HonestChain.parsedReadOp_support {ι : Type u_1} {A : Type u_2} {PA : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] [Fintype PA] {ℓ : ℕ} (L : Bool → CL.CLFun CL.𝔽₂ ι ℓ) (D : (ι → CL.𝔽₂) → (ι → CL.𝔽₂) → A → A → Bool) (R : SyncStrategy (Introspection.Honest.sourceGame L D).doubled) (w : Bool) (hL : (L w).SupportedOn Finset.univ) (b : Introspection.ParsedAnswer (ι → CL.𝔽₂) A PA) (h : Introspection.Honest.parsedReadOp L D R w hL b ≠ 0) : ∃ (y : ι → CL.𝔽₂) (yp : ι → CL.𝔽₂) (α : A), b = Introspection.ParsedAnswer.read y yp α ∧ R.P.M (w, y) α ≠ 0

theorem MIPRE.Tailored.Intro.HonestChain.parsedHideOp_support {ι : Type u_1} {A : Type u_2} {PA : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] [Fintype PA] {ℓ : ℕ} (L : Bool → CL.CLFun CL.𝔽₂ ι ℓ) (D : (ι → CL.𝔽₂) → (ι → CL.𝔽₂) → A → A → Bool) (R : SyncStrategy (Introspection.Honest.sourceGame L D).doubled) (w : Bool) (k : ℕ) (hL : (L w).SupportedOn Finset.univ) (b : Introspection.ParsedAnswer (ι → CL.𝔽₂) A PA) (h : Introspection.Honest.parsedHideOp L D R w k hL b ≠ 0) : ∃ (y : ι → CL.𝔽₂) (yp : ι → CL.𝔽₂) (x : ι → CL.𝔽₂), b = Introspection.ParsedAnswer.hide y yp x

The support of the honest strategy, label by label

theorem MIPRE.Tailored.Intro.HonestChain.srcSplitL_eq {c : ℕ} (W : Verifier 7) {lam n : ℕ} (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (V : TailoredVerifier 7) (t : Introspection.AuxType 7 × Bool) (ht : t.1 ≠ Introspection.AuxType.sample) (y : Fin (Introspection.SourceCompiler.registerBits c lam n) → CL.𝔽₂) : srcSplitL V W hs t (CL.toBits y) = V.lenOf (2 ^ n) (CL.toBits (CL.pull (Introspection.AuxiliaryProgram.firstEmbedding hs) y)) true

theorem MIPRE.Tailored.Intro.HonestChain.srcSplitL_sample {c : ℕ} (W : Verifier 7) {lam n : ℕ} (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (V : TailoredVerifier 7) (w : Bool) (y : Fin (Introspection.SourceCompiler.registerBits c lam n) → CL.𝔽₂) : srcSplitL V W hs (Introspection.AuxType.sample, w) (CL.toBits y) = V.lenOf (2 ^ n) (CL.toBits (CL.pull (Introspection.AuxiliaryProgram.firstEmbedding hs) ((Introspection.AuxiliaryDecision.padded W hs w).eval y))) true

theorem MIPRE.Tailored.Intro.HonestChain.srcSplitR_symm {c : ℕ} (W : Verifier 7) {lam n : ℕ} (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (V : TailoredVerifier 7) (t : Introspection.AuxType 7 × Bool) (ht : t.1 ≠ Introspection.AuxType.sample) (y : Introspection.BinaryComplete.Seed (Introspection.SourceCompiler.registerPower c lam n) (Introspection.SourceCompiler.fieldBits c lam n)) : srcSplitR V W hs t (CL.toBits ((CL.reindexEquiv (Introspection.CanonicalGame.numbering c lam n)).symm y)) = V.lenOf (2 ^ n) (CL.toBits (CL.pull (Introspection.AuxiliaryProgram.firstEmbedding hs) ((CL.reindexEquiv (Introspection.CanonicalGame.numbering c lam n)).symm y))) false

theorem MIPRE.Tailored.Intro.HonestChain.srcSplitL_symm {c : ℕ} (W : Verifier 7) {lam n : ℕ} (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (V : TailoredVerifier 7) (t : Introspection.AuxType 7 × Bool) (ht : t.1 ≠ Introspection.AuxType.sample) (y : Introspection.BinaryComplete.Seed (Introspection.SourceCompiler.registerPower c lam n) (Introspection.SourceCompiler.fieldBits c lam n)) : srcSplitL V W hs t (CL.toBits ((CL.reindexEquiv (Introspection.CanonicalGame.numbering c lam n)).symm y)) = V.lenOf (2 ^ n) (CL.toBits (CL.pull (Introspection.AuxiliaryProgram.firstEmbedding hs) ((CL.reindexEquiv (Introspection.CanonicalGame.numbering c lam n)).symm y))) true

theorem MIPRE.Tailored.Intro.HonestChain.encodeAnswer_pair {c lam n : ℕ} (hc : 2 ≤ c) (y : Introspection.BinaryComplete.Seed (Introspection.SourceCompiler.registerPower c lam n) (Introspection.SourceCompiler.fieldBits c lam n)) (α : Verifier.Answers ((2 ^ n) ^ lam)) : ↑(Introspection.CanonicalComplete.encodeAnswer c hc lam n ((Introspection.AuxiliaryQuotient.answerEquiv (Introspection.CanonicalGame.numbering c lam n)).symm (Introspection.ParsedAnswer.pair y α))) = Introspection.AnswerParser.pairBits (CL.toBits ((CL.reindexEquiv (Introspection.CanonicalGame.numbering c lam n)).symm y)) ↑α

theorem MIPRE.Tailored.Intro.HonestChain.take_enc_pair {c : ℕ} (W : Verifier 7) {lam n : ℕ} (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (V : TailoredVerifier 7) {t : Introspection.AuxType 7 × Bool} (ht : t.1 = Introspection.AuxType.introspect ∨ t.1 = Introspection.AuxType.sample) {y α : Cost.BitStr} (hy : List.length y = Introspection.SourceCompiler.registerBits c lam n) : win (enc (Introspection.SourceCompiler.registerBits c lam n) ((2 ^ n) ^ lam) (srcSplitR V W hs) (Sum.inr t) (Introspection.AnswerParser.pairBits y α)) 0 (Typed.Q (Introspection.SourceCompiler.fieldBits c lam n) (Introspection.PauliSamplerParameters.selectorBits c lam n)) = y

theorem MIPRE.Tailored.Intro.HonestChain.support_introspect {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (he : Even c) (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (V : TailoredVerifier 7) (hc : 2 ≤ c) (hlen : ∀ (p : Bool × W.Questions (2 ^ n)) (a : Verifier.Answers ((2 ^ n) ^ lam)), RW.P.M p a ≠ 0 → List.length ↑a = V.lenOf (2 ^ n) (CL.toBits p.2) false + V.lenOf (2 ^ n) (CL.toBits p.2) true) (w' w : Bool) (z : Fin (Introspection.PauliSampler.dimension c lam n) → CL.𝔽₂) (a : Introspection.CanonicalComplete.Answer c lam n) (ha : (canonical W RW ⋯ he hs).P.M (w', Sum.inr (Introspection.AuxType.introspect, w), z) a ≠ 0) : Complete.OkL (Introspection.SourceCompiler.fieldBits c lam n) (Introspection.PauliSamplerParameters.selectorBits c lam n) ((2 ^ n) ^ lam) V W hs (Sum.inr (Introspection.AuxType.introspect, w)) ↑(Introspection.CanonicalComplete.encodeAnswer c hc lam n a) ∧ Typed.readOK (Introspection.SourceCompiler.fieldBits c lam n) (Introspection.PauliSamplerParameters.selectorBits c lam n) ((2 ^ n) ^ lam) V W hs (Sum.inr (Introspection.AuxType.introspect, w)) (enc (Introspection.SourceCompiler.registerBits c lam n) ((2 ^ n) ^ lam) (srcSplitR V W hs) (Sum.inr (Introspection.AuxType.introspect, w)) ↑(Introspection.CanonicalComplete.encodeAnswer c hc lam n a))

The support at an Introspect label.

theorem MIPRE.Tailored.Intro.HonestChain.srcSplitR_sample_symm {c : ℕ} (W : Verifier 7) {lam n : ℕ} (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (V : TailoredVerifier 7) (w : Bool) (y : Introspection.BinaryComplete.Seed (Introspection.SourceCompiler.registerPower c lam n) (Introspection.SourceCompiler.fieldBits c lam n)) : srcSplitR V W hs (Introspection.AuxType.sample, w) (CL.toBits ((CL.reindexEquiv (Introspection.CanonicalGame.numbering c lam n)).symm y)) = V.lenOf (2 ^ n) (CL.toBits (CL.pull (Introspection.AuxiliaryProgram.firstEmbedding hs) ((Introspection.AuxiliaryDecision.padded W hs w).eval ((CL.reindexEquiv (Introspection.CanonicalGame.numbering c lam n)).symm y)))) false

theorem MIPRE.Tailored.Intro.HonestChain.srcSplitL_sample_symm {c : ℕ} (W : Verifier 7) {lam n : ℕ} (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (V : TailoredVerifier 7) (w : Bool) (y : Introspection.BinaryComplete.Seed (Introspection.SourceCompiler.registerPower c lam n) (Introspection.SourceCompiler.fieldBits c lam n)) : srcSplitL V W hs (Introspection.AuxType.sample, w) (CL.toBits ((CL.reindexEquiv (Introspection.CanonicalGame.numbering c lam n)).symm y)) = V.lenOf (2 ^ n) (CL.toBits (CL.pull (Introspection.AuxiliaryProgram.firstEmbedding hs) ((Introspection.AuxiliaryDecision.padded W hs w).eval ((CL.reindexEquiv (Introspection.CanonicalGame.numbering c lam n)).symm y)))) true

theorem MIPRE.Tailored.Intro.HonestChain.support_sample {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (he : Even c) (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (V : TailoredVerifier 7) (hc : 2 ≤ c) (hlen : ∀ (p : Bool × W.Questions (2 ^ n)) (a : Verifier.Answers ((2 ^ n) ^ lam)), RW.P.M p a ≠ 0 → List.length ↑a = V.lenOf (2 ^ n) (CL.toBits p.2) false + V.lenOf (2 ^ n) (CL.toBits p.2) true) (w' w : Bool) (z : Fin (Introspection.PauliSampler.dimension c lam n) → CL.𝔽₂) (a : Introspection.CanonicalComplete.Answer c lam n) (ha : (canonical W RW ⋯ he hs).P.M (w', Sum.inr (Introspection.AuxType.sample, w), z) a ≠ 0) : Complete.OkL (Introspection.SourceCompiler.fieldBits c lam n) (Introspection.PauliSamplerParameters.selectorBits c lam n) ((2 ^ n) ^ lam) V W hs (Sum.inr (Introspection.AuxType.sample, w)) ↑(Introspection.CanonicalComplete.encodeAnswer c hc lam n a) ∧ Typed.readOK (Introspection.SourceCompiler.fieldBits c lam n) (Introspection.PauliSamplerParameters.selectorBits c lam n) ((2 ^ n) ^ lam) V W hs (Sum.inr (Introspection.AuxType.sample, w)) (enc (Introspection.SourceCompiler.registerBits c lam n) ((2 ^ n) ^ lam) (srcSplitR V W hs) (Sum.inr (Introspection.AuxType.sample, w)) ↑(Introspection.CanonicalComplete.encodeAnswer c hc lam n a))

The support at a Sample label.

theorem MIPRE.Tailored.Intro.HonestChain.take_enc_read {c : ℕ} (W : Verifier 7) {lam n : ℕ} (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (V : TailoredVerifier 7) (w : Bool) {y yp α : Cost.BitStr} (hy : List.length y = Introspection.SourceCompiler.registerBits c lam n) (hyp : List.length yp = Introspection.SourceCompiler.registerBits c lam n) : win (enc (Introspection.SourceCompiler.registerBits c lam n) ((2 ^ n) ^ lam) (srcSplitR V W hs) (Sum.inr (Introspection.AuxType.read, w)) (Introspection.AnswerParser.tripleBits y yp α)) 0 (Typed.Q (Introspection.SourceCompiler.fieldBits c lam n) (Introspection.PauliSamplerParameters.selectorBits c lam n)) = y

theorem MIPRE.Tailored.Intro.HonestChain.take_enc_hide {c : ℕ} (W : Verifier 7) {lam n : ℕ} (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (V : TailoredVerifier 7) (k : Fin 7) (w : Bool) {y yp x : Cost.BitStr} (hy : List.length y = Introspection.SourceCompiler.registerBits c lam n) (hyp : List.length yp = Introspection.SourceCompiler.registerBits c lam n) : win (enc (Introspection.SourceCompiler.registerBits c lam n) ((2 ^ n) ^ lam) (srcSplitR V W hs) (Sum.inr (Introspection.AuxType.hide k, w)) (Introspection.AnswerParser.tripleBits y yp x)) 0 (Typed.Q (Introspection.SourceCompiler.fieldBits c lam n) (Introspection.PauliSamplerParameters.selectorBits c lam n)) = y

theorem MIPRE.Tailored.Intro.HonestChain.ofBits_toBits_symm {c lam n : ℕ} (y : Introspection.BinaryComplete.Seed (Introspection.SourceCompiler.registerPower c lam n) (Introspection.SourceCompiler.fieldBits c lam n)) : CL.ofBits (Typed.Q (Introspection.SourceCompiler.fieldBits c lam n) (Introspection.PauliSamplerParameters.selectorBits c lam n)) (CL.toBits ((CL.reindexEquiv (Introspection.CanonicalGame.numbering c lam n)).symm y)) = (CL.reindexEquiv (Introspection.CanonicalGame.numbering c lam n)).symm y

theorem MIPRE.Tailored.Intro.HonestChain.support_read {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (he : Even c) (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (V : TailoredVerifier 7) (hc : 2 ≤ c) (hlen : ∀ (p : Bool × W.Questions (2 ^ n)) (a : Verifier.Answers ((2 ^ n) ^ lam)), RW.P.M p a ≠ 0 → List.length ↑a = V.lenOf (2 ^ n) (CL.toBits p.2) false + V.lenOf (2 ^ n) (CL.toBits p.2) true) (w' w : Bool) (z : Fin (Introspection.PauliSampler.dimension c lam n) → CL.𝔽₂) (a : Introspection.CanonicalComplete.Answer c lam n) (ha : (canonical W RW ⋯ he hs).P.M (w', Sum.inr (Introspection.AuxType.read, w), z) a ≠ 0) : Complete.OkL (Introspection.SourceCompiler.fieldBits c lam n) (Introspection.PauliSamplerParameters.selectorBits c lam n) ((2 ^ n) ^ lam) V W hs (Sum.inr (Introspection.AuxType.read, w)) ↑(Introspection.CanonicalComplete.encodeAnswer c hc lam n a) ∧ Typed.readOK (Introspection.SourceCompiler.fieldBits c lam n) (Introspection.PauliSamplerParameters.selectorBits c lam n) ((2 ^ n) ^ lam) V W hs (Sum.inr (Introspection.AuxType.read, w)) (enc (Introspection.SourceCompiler.registerBits c lam n) ((2 ^ n) ^ lam) (srcSplitR V W hs) (Sum.inr (Introspection.AuxType.read, w)) ↑(Introspection.CanonicalComplete.encodeAnswer c hc lam n a))

The support at a Read label.

theorem MIPRE.Tailored.Intro.HonestChain.support_hide {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (he : Even c) (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (V : TailoredVerifier 7) (hc : 2 ≤ c) (w' : Bool) (k : Fin 7) (w : Bool) (z : Fin (Introspection.PauliSampler.dimension c lam n) → CL.𝔽₂) (a : Introspection.CanonicalComplete.Answer c lam n) (ha : (canonical W RW ⋯ he hs).P.M (w', Sum.inr (Introspection.AuxType.hide k, w), z) a ≠ 0) : Complete.OkL (Introspection.SourceCompiler.fieldBits c lam n) (Introspection.PauliSamplerParameters.selectorBits c lam n) ((2 ^ n) ^ lam) V W hs (Sum.inr (Introspection.AuxType.hide k, w)) ↑(Introspection.CanonicalComplete.encodeAnswer c hc lam n a) ∧ Typed.readOK (Introspection.SourceCompiler.fieldBits c lam n) (Introspection.PauliSamplerParameters.selectorBits c lam n) ((2 ^ n) ^ lam) V W hs (Sum.inr (Introspection.AuxType.hide k, w)) (enc (Introspection.SourceCompiler.registerBits c lam n) ((2 ^ n) ^ lam) (srcSplitR V W hs) (Sum.inr (Introspection.AuxType.hide k, w)) ↑(Introspection.CanonicalComplete.encodeAnswer c hc lam n a))

The support at a Hide label.

theorem MIPRE.Tailored.Intro.HonestChain.support_pauli {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (he : Even c) (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (V : TailoredVerifier 7) (hc : 2 ≤ c) (w' : Bool) (T : QLD.Ty) (z : Fin (Introspection.PauliSampler.dimension c lam n) → CL.𝔽₂) (a : Introspection.CanonicalComplete.Answer c lam n) (ha : (canonical W RW ⋯ he hs).P.M (w', Sum.inl T, z) a ≠ 0) : Complete.OkL (Introspection.SourceCompiler.fieldBits c lam n) (Introspection.PauliSamplerParameters.selectorBits c lam n) ((2 ^ n) ^ lam) V W hs (Sum.inl T) ↑(Introspection.CanonicalComplete.encodeAnswer c hc lam n a) ∧ Typed.readOK (Introspection.SourceCompiler.fieldBits c lam n) (Introspection.PauliSamplerParameters.selectorBits c lam n) ((2 ^ n) ^ lam) V W hs (Sum.inl T) (enc (Introspection.SourceCompiler.registerBits c lam n) ((2 ^ n) ^ lam) (srcSplitR V W hs) (Sum.inl T) ↑(Introspection.CanonicalComplete.encodeAnswer c hc lam n a))

The support at a Pauli label.

theorem MIPRE.Tailored.Intro.HonestChain.canonical_support {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (he : Even c) (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (V : TailoredVerifier 7) (hc : 2 ≤ c) (hlen : ∀ (p : Bool × W.Questions (2 ^ n)) (a : Verifier.Answers ((2 ^ n) ^ lam)), RW.P.M p a ≠ 0 → List.length ↑a = V.lenOf (2 ^ n) (CL.toBits p.2) false + V.lenOf (2 ^ n) (CL.toBits p.2) true) (q : Bool × CL.Detyping.Question Introspection.DecisionKernel.Label (Fin (Introspection.PauliSampler.dimension c lam n))) (a : Introspection.CanonicalComplete.Answer c lam n) (ha : (canonical W RW ⋯ he hs).P.M q a ≠ 0) : Complete.OkL (Introspection.SourceCompiler.fieldBits c lam n) (Introspection.PauliSamplerParameters.selectorBits c lam n) ((2 ^ n) ^ lam) V W hs q.2.1 ↑(Introspection.CanonicalComplete.encodeAnswer c hc lam n a) ∧ Typed.readOK (Introspection.SourceCompiler.fieldBits c lam n) (Introspection.PauliSamplerParameters.selectorBits c lam n) ((2 ^ n) ^ lam) V W hs q.2.1 (enc (Introspection.SourceCompiler.registerBits c lam n) ((2 ^ n) ^ lam) (srcSplitR V W hs) q.2.1 ↑(Introspection.CanonicalComplete.encodeAnswer c hc lam n a))

The support of the honest strategy of the guarded game.

theorem MIPRE.Tailored.Intro.HonestChain.raw_support {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (he : Even c) (V : TailoredVerifier 7) (hc : 2 ≤ c) (hlen : ∀ (p : Bool × W.Questions (2 ^ n)) (a : Verifier.Answers ((2 ^ n) ^ lam)), RW.P.M p a ≠ 0 → List.length ↑a = V.lenOf (2 ^ n) (CL.toBits p.2) false + V.lenOf (2 ^ n) (CL.toBits p.2) true) (U : Cost.ClockedUniversalMachine) (hW : W.IsBounded lam) (hn : 1 ≤ n) (q : Bool × CL.Detyping.Question Introspection.DecisionKernel.Label (Fin (Introspection.PauliSampler.dimension c lam n))) (a : Verifier.Answers (Introspection.DecisionCompiler.outerBound c lam n)) (ha : (raw W RW hc he U hW hn).P.M q a ≠ 0) : Complete.okT V W c lam ⋯ q.2 a

hsupp: the honest strategy of the typed game charges only well-formed byte answers whose registers satisfy the readable conditions.

The input: a permutation strategy of the tailored verifier

noncomputable def MIPRE.Tailored.Intro.HonestChain.inputSync (V : TailoredVerifier 7) (U : Cost.UniversalMachine) {n T : ℕ} (hT : (V.tgame (2 ^ n)).maxLen ≤ T) (SV : PermStrategy (V.tgame (2 ^ n)).doubled) : SyncStrategy ((V.ofTNFV U).game (2 ^ n) T).doubled

The input's strategy (lem:zpc-pcc): the measurements of a permutation strategy of the doubled tailored game on answer strings (PermStrategy.toSync), extended by zero to the answers of the normal form verifier V.ofTNFV U.

Equations

• MIPRE.Tailored.Intro.HonestChain.inputSync V U hT SV = SV.toSync.extend ((V.ofTNFV U).game (2 ^ n) T).doubled (MIPRE.Verifier.Answers.castLE hT)

theorem MIPRE.Tailored.Intro.HonestChain.inputSync_isPCC (V : TailoredVerifier 7) (U : Cost.UniversalMachine) {n T : ℕ} (hT : (V.tgame (2 ^ n)).maxLen ≤ T) (SV : PermStrategy (V.tgame (2 ^ n)).doubled) : (inputSync V U hT SV).IsPCC

theorem MIPRE.Tailored.Intro.HonestChain.inputSync_value (V : TailoredVerifier 7) (U : Cost.UniversalMachine) {n T : ℕ} (hT : (V.tgame (2 ^ n)).maxLen ≤ T) (SV : PermStrategy (V.tgame (2 ^ n)).doubled) (h : SV.value = 1) : (inputSync V U hT SV).value = 1

theorem MIPRE.Tailored.Intro.HonestChain.inputSync_M (V : TailoredVerifier 7) (U : Cost.UniversalMachine) {n T : ℕ} (hT : (V.tgame (2 ^ n)).maxLen ≤ T) (SV : PermStrategy (V.tgame (2 ^ n)).doubled) (p : Bool × V.Questions (2 ^ n)) : (inputSync V U hT SV).P.M p = Function.extend (⇑(Verifier.Answers.castLE hT)) (SV.ansProj (V.tgame (2 ^ n)).maxLen p) 0

theorem MIPRE.Tailored.Intro.HonestChain.inputSync_len (V : TailoredVerifier 7) (U : Cost.UniversalMachine) {n T : ℕ} (hT : (V.tgame (2 ^ n)).maxLen ≤ T) (SV : PermStrategy (V.tgame (2 ^ n)).doubled) (p : Bool × V.Questions (2 ^ n)) (a : Verifier.Answers T) (ha : (inputSync V U hT SV).P.M p a ≠ 0) : List.length ↑a = V.lenOf (2 ^ n) (CL.toBits p.2) false + V.lenOf (2 ^ n) (CL.toBits p.2) true

The input's answers have the tailored verifier's lengths.

theorem MIPRE.Tailored.Intro.HonestChain.inputSync_bit (V : TailoredVerifier 7) (U : Cost.UniversalMachine) {n T : ℕ} (hT : (V.tgame (2 ^ n)).maxLen ≤ T) (SV : PermStrategy (V.tgame (2 ^ n)).doubled) (p : Bool × V.Questions (2 ^ n)) (j : ℕ) : (IsXBit ((inputSync V U hT SV).P.M p) fun (a : Verifier.Answers T) => List.getD (↑a) j false) ∧ (j < V.lenOf (2 ^ n) (CL.toBits p.2) false → IsZBit ((inputSync V U hT SV).P.M p) fun (a : Verifier.Answers T) => List.getD (↑a) j false)

The input's answer bits are signed permutations, diagonal below the readable length.

The honest strategy, in one statement

theorem MIPRE.Tailored.Intro.HonestChain.honest_zpc (c : ℕ) (hc : 2 ≤ c) (he : Even c) (U : Cost.ClockedUniversalMachine) (W : Verifier 7) (lam n : ℕ) (hW : W.IsBounded lam) (hn : 1 ≤ n) (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (hRW : RW.IsPCC) (hv : RW.value = 1) (V : TailoredVerifier 7) (hlen : ∀ (p : Bool × W.Questions (2 ^ n)) (a : Verifier.Answers ((2 ^ n) ^ lam)), RW.P.M p a ≠ 0 → List.length ↑a = V.lenOf (2 ^ n) (CL.toBits p.2) false + V.lenOf (2 ^ n) (CL.toBits p.2) true) (hX : ∀ (p : Bool × W.Questions (2 ^ n)) (j : ℕ), IsXBit (RW.P.M p) fun (a : Verifier.Answers ((2 ^ n) ^ lam)) => List.getD (↑a) j false) (hZ : ∀ (p : Bool × W.Questions (2 ^ n)), ∀ j < V.lenOf (2 ^ n) (CL.toBits p.2) false, IsZBit (RW.P.M p) fun (a : Verifier.Answers ((2 ^ n) ^ lam)) => List.getD (↑a) j false) : ∃ (R : SyncStrategy (Introspection.DecisionCompiler.rawGame c ⋯ he U (W.sampler.prog, W.decider.prog) lam n).doubled), R.IsPCC ∧ R.value = 1 ∧ (∀ (q : Bool × CL.Detyping.Question (Introspection.QuestionType QLD.Ty 7) (Fin ((Introspection.DecisionCompiler.extendedSampler c ⋯ he lam).dim n))) (a : Verifier.Answers (Introspection.DecisionCompiler.outerBound c lam n)), ¬Complete.okT V W c lam ⋯ q.2 a → R.P.M q a = 0) ∧ (∀ (q : Bool × CL.Detyping.Question (Introspection.QuestionType QLD.Ty 7) (Fin ((Introspection.DecisionCompiler.extendedSampler c ⋯ he lam).dim n))) (i : ℕ), IsSignedPerm (pvmObs (R.P.M q) fun (a : Verifier.Answers ((Introspection.DecisionCompiler.constantCutoff (Introspection.DecisionCompiler.outerBound c lam n)).outer n)) => bitSign (List.getD (Complete.encT V W c lam ⋯ q.2 a) i false))) ∧ ∀ (q : Bool × CL.Detyping.Question (Introspection.QuestionType QLD.Ty 7) (Fin ((Introspection.DecisionCompiler.extendedSampler c ⋯ he lam).dim n))), ∀ i < Typed.lenR (Introspection.SourceCompiler.fieldBits c lam n) (Introspection.PauliSamplerParameters.selectorBits c lam n) ((2 ^ n) ^ lam) q.2.1, (pvmObs (R.P.M q) fun (a : Verifier.Answers ((Introspection.DecisionCompiler.constantCutoff (Introspection.DecisionCompiler.outerBound c lam n)).outer n)) => bitSign (List.getD (Complete.encT V W c lam ⋯ q.2 a) i false)).IsDiag

ZPC completeness of the tailored question reduction, the strategy (P3c): for an input normal form verifier W presenting the tailored verifier V, with a perfect PCC strategy RW at index 2^n whose answers have V's lengths and whose answer bits are signed permutations, diagonal below V's readable length, the honest strategy raw of the reference verifier's typed game is a perfect PCC strategy that charges only well-formed answers satisfying the readable conditions (hsupp), whose bit observables along the padded layout are signed permutations (hperm), diagonal at the readable bits (hdiag).

noncomputable def MIPRE.Tailored.Intro.HonestChain.inputSyncT (V : TailoredVerifier 7) (U0 : Cost.UniversalMachine) {n T : ℕ} (hT : (V.tgame (2 ^ n)).maxLen ≤ T) (SV : PermStrategy (V.tgame (2 ^ n)).doubled) : SyncStrategy ((V.ofTNFVT U0).game (2 ^ n) T).doubled

The input's strategy on the game of V.ofTNFVT U0, the same game as that of V.ofTNFV U0 (ofTNFVT_game).

Equations

• MIPRE.Tailored.Intro.HonestChain.inputSyncT V U0 hT SV = (MIPRE.Tailored.Intro.HonestChain.inputSync V U0 hT SV).copy ((V.ofTNFVT U0).game (2 ^ n) T).doubled

theorem MIPRE.Tailored.Intro.HonestChain.inputSyncT_isPCC (V : TailoredVerifier 7) (U0 : Cost.UniversalMachine) {n T : ℕ} (hT : (V.tgame (2 ^ n)).maxLen ≤ T) (SV : PermStrategy (V.tgame (2 ^ n)).doubled) : (inputSyncT V U0 hT SV).IsPCC

theorem MIPRE.Tailored.Intro.HonestChain.inputSyncT_value (V : TailoredVerifier 7) (U0 : Cost.UniversalMachine) {n T : ℕ} (hT : (V.tgame (2 ^ n)).maxLen ≤ T) (SV : PermStrategy (V.tgame (2 ^ n)).doubled) (h : SV.value = 1) : (inputSyncT V U0 hT SV).value = 1

theorem MIPRE.Tailored.Intro.HonestChain.honest_zpc_ofTNFVT (c : ℕ) (hc : 2 ≤ c) (he : Even c) (U : Cost.ClockedUniversalMachine) (T : TailoredVerifier 7) (U0 : Cost.UniversalMachine) (lam n : ℕ) (hW : (T.ofTNFVT U0).IsBounded lam) (hn : 1 ≤ n) (hT : (T.tgame (2 ^ n)).maxLen ≤ (2 ^ n) ^ lam) (hV : T.HasPerfectZPC (2 ^ n)) : ∃ (R : SyncStrategy (Introspection.DecisionCompiler.rawGame c ⋯ he U ((T.ofTNFVT U0).sampler.prog, (T.ofTNFVT U0).decider.prog) lam n).doubled), R.IsPCC ∧ R.value = 1 ∧ (∀ (q : Bool × CL.Detyping.Question (Introspection.QuestionType QLD.Ty 7) (Fin ((Introspection.DecisionCompiler.extendedSampler c ⋯ he lam).dim n))) (a : Verifier.Answers (Introspection.DecisionCompiler.outerBound c lam n)), ¬Complete.okT T (T.ofTNFVT U0) c lam ⋯ q.2 a → R.P.M q a = 0) ∧ (∀ (q : Bool × CL.Detyping.Question (Introspection.QuestionType QLD.Ty 7) (Fin ((Introspection.DecisionCompiler.extendedSampler c ⋯ he lam).dim n))) (i : ℕ), IsSignedPerm (pvmObs (R.P.M q) fun (a : Verifier.Answers ((Introspection.DecisionCompiler.constantCutoff (Introspection.DecisionCompiler.outerBound c lam n)).outer n)) => bitSign (List.getD (Complete.encT T (T.ofTNFVT U0) c lam ⋯ q.2 a) i false))) ∧ ∀ (q : Bool × CL.Detyping.Question (Introspection.QuestionType QLD.Ty 7) (Fin ((Introspection.DecisionCompiler.extendedSampler c ⋯ he lam).dim n))), ∀ i < Typed.lenR (Introspection.SourceCompiler.fieldBits c lam n) (Introspection.PauliSamplerParameters.selectorBits c lam n) ((2 ^ n) ^ lam) q.2.1, (pvmObs (R.P.M q) fun (a : Verifier.Answers ((Introspection.DecisionCompiler.constantCutoff (Introspection.DecisionCompiler.outerBound c lam n)).outer n)) => bitSign (List.getD (Complete.encT T (T.ofTNFVT U0) c lam ⋯ q.2 a) i false)).IsDiag

ZPC completeness of the tailored question reduction, the instance (P3c): the input T.ofTNFVT U0 of a tailored verifier T with a perfect ZPC strategy at index 2^n whose answers fit the cutoff (2^n)^lam. The honest strategy of the reference verifier's typed game meets the hypotheses hsupp, hperm, hdiag of Complete.hasPerfectZPC_tpresented.