Transporting field-register extraction into binary coordinates

This is an exact change of computational basis, using a self-dual field basis. It neither assumes nor proves the existence of QLD extraction witnesses.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the change of basis is the relabelling of the register of the ancilla model's register model along the binary basis (BipartiteModel.regRelabel), composed after the extraction's local isometry.

theorem MIPRE.Introspection.RestrictedSoundness.binaryX {F : Type} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m t : ℕ} [NeZero m] (b : Module.Basis (Fin t) (ZMod 2) F) (hb : LowDegree.IsSelfDualBasis b) (x : BinaryComplete.Seed m t) : registerOp (Weyl.binEquiv b).symm (Weyl.proj Weyl.wX ((Weyl.binEquiv b).symm x)) = Honest.pauliXReadout (some x)

theorem MIPRE.Introspection.RestrictedSoundness.binaryZ {F : Type} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m t : ℕ} [NeZero m] (b : Module.Basis (Fin t) (ZMod 2) F) (hb : LowDegree.IsSelfDualBasis b) (x : BinaryComplete.Seed m t) : registerOp (Weyl.binEquiv b).symm (Weyl.proj Weyl.wZ ((Weyl.binEquiv b).symm x)) = readout some (some x)

structure MIPRE.Introspection.RestrictedSoundness.FieldExtraction {F : Type} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [PartialOrder ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (hm : m ∣ Fintype.card F) (R : M.ProjStrat (QLD.qldGame hm)) (δ : ℝ) : Type (max (max (max 1 u_2) u_3) u_4)

The conclusion of the Pauli basis test at the genuine full-register answers, in field coordinates: an ancilla model and a local isometry into it with the field register adjoined, the state within δ of the register state, and the X and Z effects of the genuine answers within δ of the honest generalized Pauli projectors in summed squared state norm.

• N : QLD.AncillaModel

  The ancilla model.

• Φ : M.LocalIsometry (self.N.N.reg (QLD.Honest.Register F m))

  The local isometry into the ancilla model with the field register adjoined.

• state_error : ‖self.Φ.W M.ψ - (self.N.N.reg (QLD.Honest.Register F m)).ψ‖ ≤ δ
• X_error : ∑ x : QLD.Honest.Register F m, (self.N.N.reg (QLD.Honest.Register F m)).stateSqNorm (self.Φ.ΦA ((R.PA (QLD.Question.pauli QLD.Bas.X)).op (QLD.Answer.pauliAns x)) - smulKron 1 (Weyl.proj Weyl.wX x)) ≤ δ
• Z_error : ∑ z : QLD.Honest.Register F m, (self.N.N.reg (QLD.Honest.Register F m)).swap.stateSqNorm (self.Φ.ΦB ((R.PB (QLD.Question.pauli QLD.Bas.Z)).op (QLD.Answer.pauliAns z)) - smulKron 1 (Weyl.proj Weyl.wZ z)) ≤ δ

def MIPRE.Introspection.RestrictedSoundness.FieldExtraction.mono {F : Type} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [PartialOrder ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {hm : m ∣ Fintype.card F} {R : M.ProjStrat (QLD.qldGame hm)} {δ δ' : ℝ} (w : FieldExtraction M hm R δ) (h : δ ≤ δ') : FieldExtraction M hm R δ'

Increasing the common error bound leaves the actual extraction data unchanged.

Equations

• w.mono h = { N := w.N, Φ := w.Φ, state_error := ⋯, X_error := ⋯, Z_error := ⋯ }

noncomputable def MIPRE.Introspection.RestrictedSoundness.FieldExtraction.toBinary {F : Type} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m t d : ℕ} [NeZero m] {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [PartialOrder ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {hm : m ∣ Fintype.card F} {R : M.ProjStrat (QLD.qldGame hm)} {δ : ℝ} (w : FieldExtraction M hm R δ) (b : Module.Basis (Fin t) (ZMod 2) F) (hb : LowDegree.IsSelfDualBasis b) : Extraction M hm b R δ

Exact field-to-binary conversion of the full extraction witness: the register is relabelled along the binary basis (BipartiteModel.regRelabel). State distance and both valid-answer error sums keep precisely the same bound.

Equations

• w.toBinary b hb = { N := w.N, Φ := (w.N.N.regRelabel (MIPRE.Weyl.binEquiv b).symm).comp w.Φ, state_error := ⋯, X_error := ⋯, Z_error := ⋯ }