The bits of the honest auxiliary measurements

The honest strategy of the introspection verifier answers its auxiliary questions with the measurements of MIPRE.Introspection.Honest.auxOp, on a register of F₂-valued coordinates tensor the input's space: Introspect and Sample read the register in the computational basis and measure the input's strategy at the question read (coreOp); Read measures the adaptive Z-linear and X-dual-linear registers (readOp) and the input's strategy at the Z-outcome (fullReadOp); Hide measures the adaptive hiding registers (hideOp). This file computes the observables of their answer bits:

• isXBit_readRegister, isXBit_hideRegister: an F₂-linear bit of the dual outcome y' of Read, or of the dual outcome and the X tail (y', x) of Hide, is a signed permutation. By induction along the CL presentation: at each level the measurement is Z-syndrome ⊗ X-syndrome followed by a continuation selected by the Z-syndrome, so the bit's observable is a controlled sum of the continuation's, times the X-syndrome's linear bit, which is a shift wX c (linear data processing, exists_encObs_proj_linear);
• isZBit_readOp_fst, isZBit_hideOp_fst: any bit of the Z outcome y is a ±1 diagonal, the marginal on y being a read-out;
• auxOp_*: the bits of the four auxiliary measurements, the input's answer bits entering controlled on the register read.

Generic shapes

theorem MIPRE.Tailored.Intro.bitObs_indicator {I : Type u_1} [Fintype I] [DecidableEq I] {Λ : Type u_3} [Fintype Λ] [DecidableEq Λ] (a₀ : Λ) (f : Λ → Bool) : bitObs (fun (a : Λ) => if a = a₀ then 1 else 0) f = bitSign (f a₀) • 1

theorem MIPRE.Tailored.Intro.isXBit_indicator {I : Type u_1} [Fintype I] [DecidableEq I] {Λ : Type u_3} [Fintype Λ] [DecidableEq Λ] (a₀ : Λ) (f : Λ → Bool) : IsXBit (fun (a : Λ) => if a = a₀ then 1 else 0) f

theorem MIPRE.Tailored.Intro.bitObs_adaptive_xor {I : Type u_1} {J : Type u_2} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] {K : Type u_3} {K' : Type u_4} {B : Type u_5} [Fintype K] [Fintype K'] [Fintype B] (P : K → Matrix I I ℂ) (P' : K' → Matrix I I ℂ) (Q : K → B → Matrix J J ℂ) (g : K' → Bool) (h : K → B → Bool) : (bitObs (fun (zb : (K × K') × B) => Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (P zb.1.1 * P' zb.1.2) (Q zb.1.1 zb.2)) fun (zb : (K × K') × B) => g zb.1.2 ^^ h zb.1.1 zb.2) = (∑ z : K, Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (P z) (bitObs (Q z) (h z))) * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (bitObs P' g) 1

A bit of an adaptive tensor of a joint measurement: if the outcome ((z, z'), b) has measurement (P z * P' z') ⊗ Q z b, the bit g z' ⊕ h z b has observable (∑_z P z ⊗ (bit h z of Q z)) (bit g of P' ⊗ 1).

theorem MIPRE.Tailored.Intro.sum_filter_fst {A : Type u_3} {B : Type u_4} {M : Type u_5} [Fintype A] [Fintype B] [DecidableEq A] [AddCommMonoid M] (P : A × B → M) (a : A) : ∑ ab : A × B with ab.1 = a, P ab = ∑ b : B, P (a, b)

The binary register

theorem MIPRE.Tailored.Intro.decide_add_eq_one_xor (a b : ZMod 2) : decide (a + b = 1) = (decide (a = 1) ^^ decide (b = 1))

decide (a + b = 1) is the exclusive or of the two bits.

theorem MIPRE.Tailored.Intro.isXBit_synOf_wX {n : Type u_2} [Fintype n] [DecidableEq n] {C : Type u_3} [Fintype C] [DecidableEq C] (ψ : (n → ZMod 2) → C) (φ : Module.Dual (ZMod 2) (n → ZMod 2)) (g : C → Bool) (hg : ∀ (e : n → ZMod 2), g (ψ e) = decide (φ e = 1)) : IsSignedPerm (bitObs (Weyl.synOf Weyl.wX ψ) g)

The X-syndrome measurement's linear bits are shifts.

def MIPRE.Tailored.Intro.insertRegisterL {ι : Type u_1} [DecidableEq ι] (V : Finset ι) : (↥V → ZMod 2) →ₗ[ZMod 2] ι → ZMod 2

The inclusion of a register, as a linear map.

Equations

• MIPRE.Tailored.Intro.insertRegisterL V = { toFun := MIPRE.Introspection.Honest.insertRegister V, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem MIPRE.Tailored.Intro.insertRegisterL_apply {ι : Type u_1} [Fintype ι] [DecidableEq ι] (V : Finset ι) (x : ↥V → ZMod 2) : (insertRegisterL V) x = Introspection.Honest.insertRegister V x

Read

theorem MIPRE.Tailored.Intro.isXBit_readRegister {ι : Type u_1} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun (ZMod 2) ι ℓ) (V : Finset ι) (h : P.SupportedOn V) (φ : Module.Dual (ZMod 2) (ι → ZMod 2)) : IsXBit (Introspection.Honest.readRegister P V h) fun (a : Introspection.Honest.ReadLabel (ZMod 2) ι) => decide (φ a.2 = 1)

A linear bit of the dual outcome of the adaptive Read measurement is a signed permutation.

Hide

theorem MIPRE.Tailored.Intro.exists_dual_stopHideAnswer {ι : Type u_1} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun (ZMod 2) ι ℓ) (V : Finset ι) (φ χ : Module.Dual (ZMod 2) (ι → ZMod 2)) : ∃ (ψ : Module.Dual (ZMod 2) (↥V → ZMod 2)), ∀ (e : ↥V → ZMod 2), φ (Introspection.Honest.stopHideAnswer P V e).2.1 + χ (Introspection.Honest.stopHideAnswer P V e).2.2 = ψ e

The dual value and the X tail of the stopping Hide answer are linear in the X outcome.

theorem MIPRE.Tailored.Intro.isXBit_stopHide {ι : Type u_1} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun (ZMod 2) ι ℓ) (V : Finset ι) (φ χ : Module.Dual (ZMod 2) (ι → ZMod 2)) : IsXBit (Introspection.Honest.stopHide P V) fun (a : Introspection.Honest.HideLabel (ZMod 2) ι) => decide (φ a.2.1 + χ a.2.2 = 1)

theorem MIPRE.Tailored.Intro.isXBit_hideRegister {ι : Type u_1} [Fintype ι] [DecidableEq ι] (k : ℕ) {ℓ : ℕ} (P : CL.CLFun (ZMod 2) ι ℓ) (V : Finset ι) (h : P.SupportedOn V) (φ χ : Module.Dual (ZMod 2) (ι → ZMod 2)) : IsXBit (Introspection.Honest.hideRegister P k V h) fun (a : Introspection.Honest.HideLabel (ZMod 2) ι) => decide (φ a.2.1 + χ a.2.2 = 1)

A linear bit of the dual outcome and the X tail of the adaptive Hide measurement is a signed permutation.

The ambient registers

theorem MIPRE.Tailored.Intro.isXBit_readOp {ι : Type u_1} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun (ZMod 2) ι ℓ) (h : P.SupportedOn Finset.univ) (φ : Module.Dual (ZMod 2) (ι → ZMod 2)) : IsXBit (Introspection.Honest.readOp P h) fun (a : Introspection.Honest.ReadLabel (ZMod 2) ι) => decide (φ a.2 = 1)

theorem MIPRE.Tailored.Intro.isXBit_hideOp {ι : Type u_1} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun (ZMod 2) ι ℓ) (k : ℕ) (h : P.SupportedOn Finset.univ) (φ χ : Module.Dual (ZMod 2) (ι → ZMod 2)) : IsXBit (Introspection.Honest.hideOp P k h) fun (a : Introspection.Honest.HideLabel (ZMod 2) ι) => decide (φ a.2.1 + χ a.2.2 = 1)

theorem MIPRE.Tailored.Intro.isZBit_hideOp_fst {ι : Type u_1} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun (ZMod 2) ι ℓ) (k : ℕ) (h : P.SupportedOn Finset.univ) (g : (ι → ZMod 2) → Bool) : IsZBit (Introspection.Honest.hideOp P k h) fun (a : Introspection.Honest.HideLabel (ZMod 2) ι) => g a.1

Any bit of the Z outcome of Hide is a ±1 diagonal: the marginal is a read-out.

The four auxiliary measurements

theorem MIPRE.Tailored.Intro.parsedCoreOp_eq_extend {ι : Type u_1} [Fintype ι] [DecidableEq ι] {A : Type u_2} {PA : Type u_3} [Fintype A] [DecidableEq A] [Fintype PA] {ℓ : ℕ} (L : Bool → CL.CLFun (ZMod 2) ι ℓ) (D : (ι → ZMod 2) → (ι → ZMod 2) → A → A → Bool) (R : SyncStrategy (Introspection.Honest.sourceGame L D).doubled) (t : Introspection.Honest.CoreType) : Introspection.Honest.parsedCoreOp L D R t = Function.extend (fun (ya : (ι → ZMod 2) × A) => Introspection.ParsedAnswer.pair ya.1 ya.2) (Introspection.Honest.coreOp L D R t) 0

theorem MIPRE.Tailored.Intro.parsedReadOp_eq_extend {ι : Type u_1} [Fintype ι] [DecidableEq ι] {A : Type u_2} {PA : Type u_3} [Fintype A] [DecidableEq A] [Fintype PA] {ℓ : ℕ} (L : Bool → CL.CLFun (ZMod 2) ι ℓ) (D : (ι → ZMod 2) → (ι → ZMod 2) → A → A → Bool) (R : SyncStrategy (Introspection.Honest.sourceGame L D).doubled) (w : Bool) (h : (L w).SupportedOn Finset.univ) : Introspection.Honest.parsedReadOp L D R w h = Function.extend (fun (a : Introspection.Honest.ReadLabel (ZMod 2) ι × A) => Introspection.ParsedAnswer.read a.1.1 a.1.2 a.2) (Introspection.Honest.fullReadOp L D R w h) 0

theorem MIPRE.Tailored.Intro.parsedHideOp_eq_extend {ι : Type u_1} [Fintype ι] [DecidableEq ι] {A : Type u_2} {PA : Type u_3} [Fintype A] [DecidableEq A] [Fintype PA] {ℓ : ℕ} (L : Bool → CL.CLFun (ZMod 2) ι ℓ) (D : (ι → ZMod 2) → (ι → ZMod 2) → A → A → Bool) (R : SyncStrategy (Introspection.Honest.sourceGame L D).doubled) (w : Bool) (k : ℕ) (h : (L w).SupportedOn Finset.univ) : Introspection.Honest.parsedHideOp L D R w k h = Function.extend (fun (a : Introspection.Honest.HideLabel (ZMod 2) ι) => Introspection.ParsedAnswer.hide a.1 a.2.1 a.2.2) (fun (a : Introspection.Honest.HideLabel (ZMod 2) ι) => Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Introspection.Honest.hideOp (L w) k h a) 1) 0

theorem MIPRE.Tailored.Intro.isXBit_parsedCoreOp {ι : Type u_1} [Fintype ι] [DecidableEq ι] {A : Type u_2} {PA : Type u_3} [Fintype A] [DecidableEq A] [Fintype PA] {ℓ : ℕ} (L : Bool → CL.CLFun (ZMod 2) ι ℓ) (D : (ι → ZMod 2) → (ι → ZMod 2) → A → A → Bool) (R : SyncStrategy (Introspection.Honest.sourceGame L D).doubled) (t : Introspection.Honest.CoreType) (f : Introspection.ParsedAnswer (ι → ZMod 2) A PA → Bool) (hf : ∀ (y : ι → ZMod 2), IsXBit (R.P.M (t.2, Introspection.Honest.originalQuestion L t y)) fun (α : A) => f (Introspection.ParsedAnswer.pair y α)) : IsXBit (Introspection.Honest.parsedCoreOp L D R t) f

The bits of Introspect and Sample: controlled by the register read, the input's bits at the question read.

theorem MIPRE.Tailored.Intro.isZBit_parsedCoreOp {ι : Type u_1} [Fintype ι] [DecidableEq ι] {A : Type u_2} {PA : Type u_3} [Fintype A] [DecidableEq A] [Fintype PA] {ℓ : ℕ} (L : Bool → CL.CLFun (ZMod 2) ι ℓ) (D : (ι → ZMod 2) → (ι → ZMod 2) → A → A → Bool) (R : SyncStrategy (Introspection.Honest.sourceGame L D).doubled) (t : Introspection.Honest.CoreType) (f : Introspection.ParsedAnswer (ι → ZMod 2) A PA → Bool) (hf : ∀ (y : ι → ZMod 2), IsZBit (R.P.M (t.2, Introspection.Honest.originalQuestion L t y)) fun (α : A) => f (Introspection.ParsedAnswer.pair y α)) : IsZBit (Introspection.Honest.parsedCoreOp L D R t) f

theorem MIPRE.Tailored.Intro.readOp_merge {ι : Type u_1} [Fintype ι] [DecidableEq ι] {A : Type u_2} [Fintype A] [DecidableEq A] {ℓ : ℕ} (L : Bool → CL.CLFun (ZMod 2) ι ℓ) (D : (ι → ZMod 2) → (ι → ZMod 2) → A → A → Bool) (R : SyncStrategy (Introspection.Honest.sourceGame L D).doubled) (w : Bool) (h : (L w).SupportedOn Finset.univ) : (fun (ya : (ι → ZMod 2) × A) => ∑ a : Introspection.Honest.ReadLabel (ZMod 2) ι × A with (a.1.1, a.2) = ya, Introspection.Honest.fullReadOp L D R w h a) = fun (ya : (ι → ZMod 2) × A) => Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Introspection.readout (L w).eval ya.1) (R.P.M (w, ya.1) ya.2)

theorem MIPRE.Tailored.Intro.isXBit_parsedReadOp_fst {ι : Type u_1} [Fintype ι] [DecidableEq ι] {A : Type u_2} {PA : Type u_3} [Fintype A] [DecidableEq A] [Fintype PA] {ℓ : ℕ} (L : Bool → CL.CLFun (ZMod 2) ι ℓ) (D : (ι → ZMod 2) → (ι → ZMod 2) → A → A → Bool) (R : SyncStrategy (Introspection.Honest.sourceGame L D).doubled) (w : Bool) (h : (L w).SupportedOn Finset.univ) (f : Introspection.ParsedAnswer (ι → ZMod 2) A PA → Bool) (F' : (ι → ZMod 2) × A → Bool) (hF : ∀ (y yp : ι → ZMod 2) (α : A), f (Introspection.ParsedAnswer.read y yp α) = F' (y, α)) (hf : ∀ (y : ι → ZMod 2), IsXBit (R.P.M (w, y)) fun (α : A) => F' (y, α)) : IsXBit (Introspection.Honest.parsedReadOp L D R w h) f

The bits of Read that depend on the register and the input's answer: controlled by the register.

theorem MIPRE.Tailored.Intro.isZBit_parsedReadOp_fst {ι : Type u_1} [Fintype ι] [DecidableEq ι] {A : Type u_2} {PA : Type u_3} [Fintype A] [DecidableEq A] [Fintype PA] {ℓ : ℕ} (L : Bool → CL.CLFun (ZMod 2) ι ℓ) (D : (ι → ZMod 2) → (ι → ZMod 2) → A → A → Bool) (R : SyncStrategy (Introspection.Honest.sourceGame L D).doubled) (w : Bool) (h : (L w).SupportedOn Finset.univ) (f : Introspection.ParsedAnswer (ι → ZMod 2) A PA → Bool) (F' : (ι → ZMod 2) × A → Bool) (hF : ∀ (y yp : ι → ZMod 2) (α : A), f (Introspection.ParsedAnswer.read y yp α) = F' (y, α)) (hf : ∀ (y : ι → ZMod 2), IsZBit (R.P.M (w, y)) fun (α : A) => F' (y, α)) : IsZBit (Introspection.Honest.parsedReadOp L D R w h) f

theorem MIPRE.Tailored.Intro.isXBit_parsedReadOp_dual {ι : Type u_1} [Fintype ι] [DecidableEq ι] {A : Type u_2} {PA : Type u_3} [Fintype A] [DecidableEq A] [Fintype PA] {ℓ : ℕ} (L : Bool → CL.CLFun (ZMod 2) ι ℓ) (D : (ι → ZMod 2) → (ι → ZMod 2) → A → A → Bool) (R : SyncStrategy (Introspection.Honest.sourceGame L D).doubled) (w : Bool) (h : (L w).SupportedOn Finset.univ) (f : Introspection.ParsedAnswer (ι → ZMod 2) A PA → Bool) (φ : Module.Dual (ZMod 2) (ι → ZMod 2)) (hF : ∀ (y yp : ι → ZMod 2) (α : A), f (Introspection.ParsedAnswer.read y yp α) = decide (φ yp = 1)) : IsXBit (Introspection.Honest.parsedReadOp L D R w h) f

A linear bit of the dual outcome of Read is a signed permutation.

theorem MIPRE.Tailored.Intro.hide_injective {ι : Type u_1} [Fintype ι] [DecidableEq ι] {A : Type u_2} {PA : Type u_3} [Fintype A] [DecidableEq A] [Fintype PA] : Function.Injective fun (a : Introspection.Honest.HideLabel (ZMod 2) ι) => Introspection.ParsedAnswer.hide a.1 a.2.1 a.2.2

theorem MIPRE.Tailored.Intro.isZBit_parsedHideOp_fst {ι : Type u_1} [Fintype ι] [DecidableEq ι] {A : Type u_2} {PA : Type u_3} [Fintype A] [DecidableEq A] [Fintype PA] {ℓ : ℕ} (L : Bool → CL.CLFun (ZMod 2) ι ℓ) (D : (ι → ZMod 2) → (ι → ZMod 2) → A → A → Bool) (R : SyncStrategy (Introspection.Honest.sourceGame L D).doubled) (w : Bool) (k : ℕ) (h : (L w).SupportedOn Finset.univ) (f : Introspection.ParsedAnswer (ι → ZMod 2) A PA → Bool) (g : (ι → ZMod 2) → Bool) (hF : ∀ (y yp x : ι → ZMod 2), f (Introspection.ParsedAnswer.hide y yp x) = g y) : IsZBit (Introspection.Honest.parsedHideOp L D R w k h) f

Any bit of the Z outcome of Hide is a ±1 diagonal.

theorem MIPRE.Tailored.Intro.isXBit_parsedHideOp_lin {ι : Type u_1} [Fintype ι] [DecidableEq ι] {A : Type u_2} {PA : Type u_3} [Fintype A] [DecidableEq A] [Fintype PA] {ℓ : ℕ} (L : Bool → CL.CLFun (ZMod 2) ι ℓ) (D : (ι → ZMod 2) → (ι → ZMod 2) → A → A → Bool) (R : SyncStrategy (Introspection.Honest.sourceGame L D).doubled) (w : Bool) (k : ℕ) (h : (L w).SupportedOn Finset.univ) (f : Introspection.ParsedAnswer (ι → ZMod 2) A PA → Bool) (φ χ : Module.Dual (ZMod 2) (ι → ZMod 2)) (hF : ∀ (y yp x : ι → ZMod 2), f (Introspection.ParsedAnswer.hide y yp x) = decide (φ yp + χ x = 1)) : IsXBit (Introspection.Honest.parsedHideOp L D R w k h) f

A linear bit of the dual outcome and the X tail of Hide is a signed permutation.