The measurement of the honest strategy at a typed question

The honest strategy of the guarded game (HonestChain.canonical) measures, at a typed question (w, (p, z)), the honest binary operator of the label p (BinaryComplete.op), relabelled to the binary Weyl coordinates of the answers (AuxiliaryQuotient.answerEquiv) and conjugated by the numbering of its space (canonical_M). This file reduces a bit of its outcome to a bit of the honest Pauli measurement (QLD.Honest.answerOp, at a Pauli label) or of the honest auxiliary measurement (Honest.auxOp, at an auxiliary label), whose bits MIPRE.Tailored.Intro.HonestPauli and MIPRE.Tailored.Intro.HonestAux compute.

theorem MIPRE.Tailored.Intro.HonestChain.canonical_M {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (hc1 : 1 ≤ c) (he : Even c) (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (w : Bool) (p : Introspection.QuestionType QLD.Ty 7) (z : Fin (Introspection.PauliSampler.dimension c lam n) → CL.𝔽₂) (a : Introspection.CanonicalComplete.Answer c lam n) : (canonical W RW hc1 he hs).P.M (w, p, z) a = (Introspection.BinaryComplete.op (family W hs) (decider W hs) (reindexed W RW hs) ⋯ (Introspection.CanonicalGame.basis c he lam n) ⋯ ((Introspection.ExplicitGame.questionEquiv (Introspection.CanonicalGame.permutation c lam n) (Introspection.CanonicalGame.basis c he lam n)) (p, z)) ((Introspection.AuxiliaryQuotient.answerEquiv (Introspection.CanonicalGame.numbering c lam n)) a)).submatrix ⇑(Fintype.equivFin (Introspection.BinaryComplete.Space (family W hs) (decider W hs) (reindexed W RW hs))).symm ⇑(Fintype.equivFin (Introspection.BinaryComplete.Space (family W hs) (decider W hs) (reindexed W RW hs))).symm

The honest measurement at a typed question.

theorem MIPRE.Tailored.Intro.HonestChain.isXBit_canonical {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (hc1 : 1 ≤ c) (he : Even c) (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (w : Bool) (p : Introspection.QuestionType QLD.Ty 7) (z : Fin (Introspection.PauliSampler.dimension c lam n) → CL.𝔽₂) (g : Introspection.CanonicalComplete.Answer c lam n → Bool) (h : IsXBit (Introspection.BinaryComplete.op (family W hs) (decider W hs) (reindexed W RW hs) ⋯ (Introspection.CanonicalGame.basis c he lam n) ⋯ ((Introspection.ExplicitGame.questionEquiv (Introspection.CanonicalGame.permutation c lam n) (Introspection.CanonicalGame.basis c he lam n)) (p, z))) (g ∘ ⇑(Introspection.AuxiliaryQuotient.answerEquiv (Introspection.CanonicalGame.numbering c lam n)).symm)) : IsXBit ((canonical W RW hc1 he hs).P.M (w, p, z)) g

A bit of the honest measurement at a typed question is a bit of the binary operator, read through the relabelling of the answers.

theorem MIPRE.Tailored.Intro.HonestChain.isZBit_canonical {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (hc1 : 1 ≤ c) (he : Even c) (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (w : Bool) (p : Introspection.QuestionType QLD.Ty 7) (z : Fin (Introspection.PauliSampler.dimension c lam n) → CL.𝔽₂) (g : Introspection.CanonicalComplete.Answer c lam n → Bool) (h : IsZBit (Introspection.BinaryComplete.op (family W hs) (decider W hs) (reindexed W RW hs) ⋯ (Introspection.CanonicalGame.basis c he lam n) ⋯ ((Introspection.ExplicitGame.questionEquiv (Introspection.CanonicalGame.permutation c lam n) (Introspection.CanonicalGame.basis c he lam n)) (p, z))) (g ∘ ⇑(Introspection.AuxiliaryQuotient.answerEquiv (Introspection.CanonicalGame.numbering c lam n)).symm)) : IsZBit ((canonical W RW hc1 he hs).P.M (w, p, z)) g

Pauli labels

theorem MIPRE.Tailored.Intro.HonestChain.pauli_injective {V : Type u_1} {A : Type u_2} {PA : Type u_3} : Function.Injective Introspection.ParsedAnswer.pauli

theorem MIPRE.Tailored.Intro.HonestChain.parsedPauliOp_eq_extend {I : Type u_1} {V : Type u_2} {A : Type u_3} {PA : Type u_4} [Fintype I] [DecidableEq I] (M : PA → Matrix I I ℂ) : Introspection.Honest.parsedPauliOp M = Function.extend Introspection.ParsedAnswer.pauli M 0

noncomputable def MIPRE.Tailored.Intro.HonestChain.fbit {c lam n : ℕ} (hc : 2 ≤ c) (R : ℕ) (splitR : Introspection.AuxType 7 × Bool → Cost.BitStr → ℕ) (p : Introspection.QuestionType QLD.Ty 7) (i : ℕ) (a : Introspection.CanonicalComplete.Answer c lam n) : Bool

The i-th bit of the tailored encoding of an answer of the guarded game.

Equations

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

theorem MIPRE.Tailored.Intro.HonestChain.fbit_pauli {c lam n : ℕ} (hc : 2 ≤ c) (R : ℕ) (splitR : Introspection.AuxType 7 × Bool → Cost.BitStr → ℕ) (T : QLD.Ty) (i : ℕ) (a : QLD.Answer (Introspection.CanonicalGame.field c lam n).carrier (Introspection.SourceCompiler.registerPower c lam n) 1) : fbit hc R splitR (Sum.inl T) i (Introspection.ParsedAnswer.pauli a) = answerBit ⋯ i a

theorem MIPRE.Tailored.Intro.HonestChain.isXBit_canonical_pauli {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (hc1 : 1 ≤ c) (he : Even c) (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (hc : 2 ≤ c) (R : ℕ) (splitR : Introspection.AuxType 7 × Bool → Cost.BitStr → ℕ) (w : Bool) (T : QLD.Ty) (z : Fin (Introspection.PauliSampler.dimension c lam n) → CL.𝔽₂) (i : ℕ) : IsXBit ((canonical W RW hc1 he hs).P.M (w, Sum.inl T, z)) (fbit hc R splitR (Sum.inl T) i)

At a Pauli label every bit is a signed permutation.

theorem MIPRE.Tailored.Intro.HonestChain.isZBit_canonical_pauliZ {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (hc1 : 1 ≤ c) (he : Even c) (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (hc : 2 ≤ c) (R : ℕ) (splitR : Introspection.AuxType 7 × Bool → Cost.BitStr → ℕ) (w : Bool) (z : Fin (Introspection.PauliSampler.dimension c lam n) → CL.𝔽₂) (i : ℕ) : IsZBit ((canonical W RW hc1 he hs).P.M (w, Sum.inl (QLD.Ty.pauli QLD.Bas.Z), z)) (fbit hc R splitR (Sum.inl (QLD.Ty.pauli QLD.Bas.Z)) i)

At the (Pauli, Z) label every bit is a ±1 diagonal.

The input's answer bits

The honest strategy measures the input's strategy RW at the question read off the register. What it needs of RW: its answer bits are signed permutations, diagonal below the readable length the tailored verifier V assigns to the question.

theorem MIPRE.Tailored.Intro.HonestChain.isZBit_input_readable (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (V : TailoredVerifier 7) (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) (p : Bool × W.Questions (2 ^ n)) (j : ℕ) : IsZBit (RW.P.M p) fun (a : Verifier.Answers ((2 ^ n) ^ lam)) => if j < V.lenOf (2 ^ n) (CL.toBits p.2) false then List.getD (↑a) j false else false

The input's readable answer slot j: the j-th answer bit below the readable length, 0 above.

theorem MIPRE.Tailored.Intro.HonestChain.toBits_getD {Q : ℕ} (v : Fin Q → CL.𝔽₂) (j : ℕ) : List.getD (CL.toBits v) j false = if h : j < Q then decide (v ⟨j, h⟩ = 1) else false

theorem MIPRE.Tailored.Intro.HonestChain.isXBit_pair_input {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (V : TailoredVerifier 7) (R : ℕ) {t : Introspection.AuxType 7 × Bool} (ht : t.1 = Introspection.AuxType.introspect ∨ t.1 = Introspection.AuxType.sample) (splitR : Introspection.AuxType 7 × Bool → Cost.BitStr → ℕ) (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) (p : Bool × W.Questions (2 ^ n)) {yb : Cost.BitStr} (hyb : List.length yb = Introspection.SourceCompiler.registerBits c lam n) (hsp : splitR t yb = V.lenOf (2 ^ n) (CL.toBits p.2) false) (hR : V.lenOf (2 ^ n) (CL.toBits p.2) false ≤ R) (i : ℕ) : (IsXBit (RW.P.M p) fun (α : Verifier.Answers ((2 ^ n) ^ lam)) => List.getD (enc (Introspection.SourceCompiler.registerBits c lam n) R splitR (Sum.inr t) (Introspection.AnswerParser.pairBits yb ↑α)) i false) ∧ (i < Introspection.SourceCompiler.registerBits c lam n + R → IsZBit (RW.P.M p) fun (α : Verifier.Answers ((2 ^ n) ^ lam)) => List.getD (enc (Introspection.SourceCompiler.registerBits c lam n) R splitR (Sum.inr t) (Introspection.AnswerParser.pairBits yb ↑α)) i false)

The bits of an Introspect or Sample answer, at a fixed register, as bits of the input's answer.

theorem MIPRE.Tailored.Intro.HonestChain.isXBit_read_input {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (V : TailoredVerifier 7) (R : ℕ) {w : Bool} (splitR : Introspection.AuxType 7 × Bool → Cost.BitStr → ℕ) (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) (p : Bool × W.Questions (2 ^ n)) {yb ypb : Cost.BitStr} (hyb : List.length yb = Introspection.SourceCompiler.registerBits c lam n) (hypb : List.length ypb = Introspection.SourceCompiler.registerBits c lam n) (hsp : splitR (Introspection.AuxType.read, w) yb = V.lenOf (2 ^ n) (CL.toBits p.2) false) (hR : V.lenOf (2 ^ n) (CL.toBits p.2) false ≤ R) (i : ℕ) (hi : ¬(¬i < Introspection.SourceCompiler.registerBits c lam n ∧ ¬i - Introspection.SourceCompiler.registerBits c lam n < R ∧ i - Introspection.SourceCompiler.registerBits c lam n - R < Introspection.SourceCompiler.registerBits c lam n)) : (IsXBit (RW.P.M p) fun (α : Verifier.Answers ((2 ^ n) ^ lam)) => List.getD (enc (Introspection.SourceCompiler.registerBits c lam n) R splitR (Sum.inr (Introspection.AuxType.read, w)) (Introspection.AnswerParser.tripleBits yb ypb ↑α)) i false) ∧ (i < Introspection.SourceCompiler.registerBits c lam n + R → IsZBit (RW.P.M p) fun (α : Verifier.Answers ((2 ^ n) ^ lam)) => List.getD (enc (Introspection.SourceCompiler.registerBits c lam n) R splitR (Sum.inr (Introspection.AuxType.read, w)) (Introspection.AnswerParser.tripleBits yb ypb ↑α)) i false)

The bits of a Read answer outside its dual register, at a fixed register, as bits of the input's answer.

Auxiliary labels

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

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

theorem MIPRE.Tailored.Intro.HonestChain.lenOf_le (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (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) (p : Bool × W.Questions (2 ^ n)) (κ : Bool) : V.lenOf (2 ^ n) (CL.toBits p.2) κ ≤ (2 ^ n) ^ lam

The input's readable length is at most the answer bound: some answer has a nonzero projection, and it has the input's length.

theorem MIPRE.Tailored.Intro.HonestChain.srcSplitR_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.𝔽₂) : srcSplitR V W hs t (CL.toBits y) = V.lenOf (2 ^ n) (CL.toBits (CL.pull (Introspection.AuxiliaryProgram.firstEmbedding hs) y)) false

theorem MIPRE.Tailored.Intro.HonestChain.srcSplitR_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.𝔽₂) : srcSplitR 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))) false

theorem MIPRE.Tailored.Intro.HonestChain.reindexed_M {c : ℕ} (W : Verifier 7) {lam n : ℕ} (RW : SyncStrategy (W.game (2 ^ n) ((2 ^ n) ^ lam)).doubled) (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (w : Bool) (y : Introspection.BinaryComplete.Seed (Introspection.SourceCompiler.registerPower c lam n) (Introspection.SourceCompiler.fieldBits c lam n)) : (reindexed W RW hs).P.M (w, y) = RW.P.M (w, CL.pull (Introspection.AuxiliaryProgram.firstEmbedding hs) ((CL.reindexEquiv (Introspection.CanonicalGame.numbering c lam n)).symm y))

theorem MIPRE.Tailored.Intro.HonestChain.fbit_pair {c lam n : ℕ} (hc : 2 ≤ c) (splitR : Introspection.AuxType 7 × Bool → Cost.BitStr → ℕ) (t : Introspection.AuxType 7 × Bool) (i : ℕ) (y : Introspection.BinaryComplete.Seed (Introspection.SourceCompiler.registerPower c lam n) (Introspection.SourceCompiler.fieldBits c lam n)) : (fun (α : Verifier.Answers ((2 ^ n) ^ lam)) => (fbit hc ((2 ^ n) ^ lam) splitR (Sum.inr t) i ∘ ⇑(Introspection.AuxiliaryQuotient.answerEquiv (Introspection.CanonicalGame.numbering c lam n)).symm) (Introspection.ParsedAnswer.pair y α)) = fun (α : Verifier.Answers ((2 ^ n) ^ lam)) => List.getD (enc (Introspection.SourceCompiler.registerBits c lam n) ((2 ^ n) ^ lam) splitR (Sum.inr t) (Introspection.AnswerParser.pairBits (CL.toBits ((CL.reindexEquiv (Introspection.CanonicalGame.numbering c lam n)).symm y)) ↑α)) i false

theorem MIPRE.Tailored.Intro.HonestChain.bits_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) (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) (w' w : Bool) (z : Fin (Introspection.PauliSampler.dimension c lam n) → CL.𝔽₂) (i : ℕ) : IsXBit ((canonical W RW ⋯ he hs).P.M (w', Sum.inr (Introspection.AuxType.introspect, w), z)) (fbit hc ((2 ^ n) ^ lam) (srcSplitR V W hs) (Sum.inr (Introspection.AuxType.introspect, w)) i) ∧ (i < Introspection.SourceCompiler.registerBits c lam n + (2 ^ n) ^ lam → IsZBit ((canonical W RW ⋯ he hs).P.M (w', Sum.inr (Introspection.AuxType.introspect, w), z)) (fbit hc ((2 ^ n) ^ lam) (srcSplitR V W hs) (Sum.inr (Introspection.AuxType.introspect, w)) i))

The bits at an Introspect label.

theorem MIPRE.Tailored.Intro.HonestChain.family_eval_symm {c : ℕ} (W : Verifier 7) {lam n : ℕ} (hs : W.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n) (w : Bool) (z : Introspection.BinaryComplete.Seed (Introspection.SourceCompiler.registerPower c lam n) (Introspection.SourceCompiler.fieldBits c lam n)) : (CL.reindexEquiv (Introspection.CanonicalGame.numbering c lam n)).symm ((family W hs w).eval z) = (Introspection.AuxiliaryDecision.padded W hs w).eval ((CL.reindexEquiv (Introspection.CanonicalGame.numbering c lam n)).symm z)

theorem MIPRE.Tailored.Intro.HonestChain.bits_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) (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) (w' w : Bool) (z : Fin (Introspection.PauliSampler.dimension c lam n) → CL.𝔽₂) (i : ℕ) : IsXBit ((canonical W RW ⋯ he hs).P.M (w', Sum.inr (Introspection.AuxType.sample, w), z)) (fbit hc ((2 ^ n) ^ lam) (srcSplitR V W hs) (Sum.inr (Introspection.AuxType.sample, w)) i) ∧ (i < Introspection.SourceCompiler.registerBits c lam n + (2 ^ n) ^ lam → IsZBit ((canonical W RW ⋯ he hs).P.M (w', Sum.inr (Introspection.AuxType.sample, w), z)) (fbit hc ((2 ^ n) ^ lam) (srcSplitR V W hs) (Sum.inr (Introspection.AuxType.sample, w)) i))

The bits at a Sample label.

theorem MIPRE.Tailored.Intro.HonestChain.length_toBits_symm {c lam n : ℕ} (y : Introspection.BinaryComplete.Seed (Introspection.SourceCompiler.registerPower c lam n) (Introspection.SourceCompiler.fieldBits c lam n)) : List.length (CL.toBits ((CL.reindexEquiv (Introspection.CanonicalGame.numbering c lam n)).symm y)) = Introspection.SourceCompiler.registerBits c lam n

theorem MIPRE.Tailored.Intro.HonestChain.encodeAnswer_read {c lam n : ℕ} (hc : 2 ≤ c) (y yp : 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.read y yp α))) = Introspection.AnswerParser.tripleBits (CL.toBits ((CL.reindexEquiv (Introspection.CanonicalGame.numbering c lam n)).symm y)) (CL.toBits ((CL.reindexEquiv (Introspection.CanonicalGame.numbering c lam n)).symm yp)) ↑α

theorem MIPRE.Tailored.Intro.HonestChain.encodeAnswer_hide {c lam n : ℕ} (hc : 2 ≤ c) (y yp x : Introspection.BinaryComplete.Seed (Introspection.SourceCompiler.registerPower c lam n) (Introspection.SourceCompiler.fieldBits c lam n)) : ↑(Introspection.CanonicalComplete.encodeAnswer c hc lam n ((Introspection.AuxiliaryQuotient.answerEquiv (Introspection.CanonicalGame.numbering c lam n)).symm (Introspection.ParsedAnswer.hide y yp x))) = Introspection.AnswerParser.tripleBits (CL.toBits ((CL.reindexEquiv (Introspection.CanonicalGame.numbering c lam n)).symm y)) (CL.toBits ((CL.reindexEquiv (Introspection.CanonicalGame.numbering c lam n)).symm yp)) (CL.toBits ((CL.reindexEquiv (Introspection.CanonicalGame.numbering c lam n)).symm x))

theorem MIPRE.Tailored.Intro.HonestChain.toBits_symm_getD {c lam n : ℕ} (y : Introspection.BinaryComplete.Seed (Introspection.SourceCompiler.registerPower c lam n) (Introspection.SourceCompiler.fieldBits c lam n)) (j : ℕ) (hj : j < Introspection.SourceCompiler.registerBits c lam n) : List.getD (CL.toBits ((CL.reindexEquiv (Introspection.CanonicalGame.numbering c lam n)).symm y)) j false = decide ((LinearMap.proj ((Introspection.CanonicalGame.numbering c lam n) ⟨j, hj⟩)) y = 1)

A bit of a reindexed register is a coordinate functional.

theorem MIPRE.Tailored.Intro.HonestChain.bits_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) (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) (w' w : Bool) (z : Fin (Introspection.PauliSampler.dimension c lam n) → CL.𝔽₂) (i : ℕ) : IsXBit ((canonical W RW ⋯ he hs).P.M (w', Sum.inr (Introspection.AuxType.read, w), z)) (fbit hc ((2 ^ n) ^ lam) (srcSplitR V W hs) (Sum.inr (Introspection.AuxType.read, w)) i) ∧ (i < Introspection.SourceCompiler.registerBits c lam n + (2 ^ n) ^ lam → IsZBit ((canonical W RW ⋯ he hs).P.M (w', Sum.inr (Introspection.AuxType.read, w), z)) (fbit hc ((2 ^ n) ^ lam) (srcSplitR V W hs) (Sum.inr (Introspection.AuxType.read, w)) i))

The bits at a Read label.

theorem MIPRE.Tailored.Intro.HonestChain.bits_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.𝔽₂) (i : ℕ) : IsXBit ((canonical W RW ⋯ he hs).P.M (w', Sum.inr (Introspection.AuxType.hide k, w), z)) (fbit hc ((2 ^ n) ^ lam) (srcSplitR V W hs) (Sum.inr (Introspection.AuxType.hide k, w)) i) ∧ (i < Introspection.SourceCompiler.registerBits c lam n → IsZBit ((canonical W RW ⋯ he hs).P.M (w', Sum.inr (Introspection.AuxType.hide k, w), z)) (fbit hc ((2 ^ n) ^ lam) (srcSplitR V W hs) (Sum.inr (Introspection.AuxType.hide k, w)) i))

The bits at a Hide label.