Documentation

MIPRE.Foundations.Introspection.HidingBaseOperators

The ideal first hiding family is the full Pauli-X coarsening #

The two statements about a state are made in a bipartite model (Phase 4 of planning/mipco-track.md): an ideal mirror is a vector identity, and the register mirror is BipartiteModel.reg_mirror. The honest register operators stay concrete.

source
theorem MIPRE.Introspection.xSqNorm_eq_stateSqNorm_of_mirror {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) (M P : 𝒜) (Q : ℬ) (hmirror : (Ψ.π (Ψ.πA P)) Ψ.ψ = (Ψ.π (Ψ.πB Q)) Ψ.ψ) :
Ψ.xSqNorm M Q = Ψ.stateSqNorm (P - M)

An ideal mirror identifies same-side replacement error with fine cross-party consistency, before any coarse-graining is performed.

source
noncomputable def MIPRE.Introspection.Honest.pauliXReadout {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] :
Option (ι → F) → Matrix (ι → F) (ι → F) ℂ

The complete Pauli-X family, including zero at the malformed outcome.

Equations
Instances For
    source
    theorem MIPRE.Introspection.Honest.pauliXReadout_isPVM {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] :
    IsPVM pauliXReadout
    source
    @[simp]
    theorem MIPRE.Introspection.Honest.pauliXReadout_none {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] :
    pauliXReadout none = 0
    source
    @[simp]
    theorem MIPRE.Introspection.Honest.pauliXReadout_some {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] (x : ι → F) :
    pauliXReadout (some x) = Weyl.proj Weyl.wX x
    source
    theorem MIPRE.Introspection.Honest.hideLabelCoarse_firstHideAnswer {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (x : ι → F) :
    hideLabelCoarse P 0 (firstHideAnswer P x) = some (firstHideAnswer P x)
    source
    theorem MIPRE.Introspection.Honest.pauliXReadout_firstHide {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (h : P.SupportedOn Finset.univ) (z : Option (HideLabel F ι)) :
    fibSum pauliXReadout (Option.map (firstHideAnswer P)) z = hideCoarseOp P 0 h z

    The ideal full-register first Hide family equals the tested coarsening of ideal Pauli-X, with a complete dummy outcome.

    source
    theorem MIPRE.Introspection.Honest.pauliXReadout_registerState_mirror {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {𝒞 : Type u_3} {𝒜 : Type u_4} {ℬ : Type u_5} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (x : Option (ι → F)) :
    ((Ξ.reg (ι → F)).π ((Ξ.reg (ι → F)).πA (smulKron 1 (pauliXReadout x)))) (Ξ.reg (ι → F)).ψ = ((Ξ.reg (ι → F)).π ((Ξ.reg (ι → F)).πB (smulKron 1 (pauliXReadout x)))) (Ξ.reg (ι → F)).ψ