Documentation

MIPRE.Foundations.Introspection.SamplingRegister

The actual sampling outcomes and their ideal prefix readouts #

All maps retain a dummy outcome for malformed answers. Coarse-graining the ideal computational-basis measurement gives exactly the prefix measurement used by the hiding induction, on the full ambient outcome alphabet.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): nothing here involves a state, so the translation is of the operators. A measurement is a POVM in any ordered ⋆-ring (a player's algebra; in the register model Ξ.reg (ι → F), the matrices over ι → F with entries in Ξ's algebras), coarse-graining is fibSumIn, and the ideal Z readout and the hiding prefix, honest register operators over ℂ, stay concrete and enter the matrices over any algebra as smulKron 1, through which coarse-graining passes (fibSumIn_smulKron_one). The coarse-graining of a readout (fibSum_readout) is an identity of complex register matrices and is unchanged.

source
theorem MIPRE.Introspection.fibSum_readout {I : Type u_1} {Y : Type u_2} {Z : Type u_3} [Fintype I] [DecidableEq I] [Fintype Y] [DecidableEq Y] [Fintype Z] [DecidableEq Z] (f : I → Y) (g : Y → Z) (z : Z) :
fibSum (readout f) g z = readout (g ∘ f) z

Coarse-graining a computational readout reads the composite function.

source
def MIPRE.Introspection.TypedEstimates.sampleSeed {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {A : Type u_5} :
ParsedAnswer (ι → F) A PauliAnswer → Option (ι → F)

The seed reported by a Sample answer.

Equations
Instances For
    source
    def MIPRE.Introspection.TypedEstimates.sampledQuestionPrefix {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {A : Type u_5} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (j : ℕ) (a : ParsedAnswer (ι → F) A PauliAnswer) :
    Option (ι → F)

    The actual sampled question prefix, rather than the reported Introspect prefix.

    Equations
    Instances For
      source
      theorem MIPRE.Introspection.TypedEstimates.check_sample_pauliZ_seed {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {A : Type u_5} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (X Z : PauliType) (projectPauli : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : PauliType → PauliType → PauliAnswer → PauliAnswer → Bool) (w : Bool) {a b : ParsedAnswer (ι → F) A PauliAnswer} (h : TypedPredicate.check L X Z projectPauli D DP (QuestionType.sample w) (QuestionType.pauli Z) a b = true) :
      sampleSeed a = pauliProjection projectPauli b

      The actual reversed Z/Sample edge compares the sampled seed with Bob's projected Pauli answer; wrong constructors cannot be accepted.

      source
      theorem MIPRE.Introspection.TypedEstimates.check_sample_introspect_prefix {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {A : Type u_5} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (X Z : PauliType) (projectPauli : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : PauliType → PauliType → PauliAnswer → PauliAnswer → Bool) (w : Bool) (hL : (L w).SupportedOn Finset.univ) (j : ℕ) {a b : ParsedAnswer (ι → F) A PauliAnswer} (h : TypedPredicate.check L X Z projectPauli D DP (QuestionType.sample w) (QuestionType.introspect w) a b = true) :
      sampledQuestionPrefix (L w) j a = reportedPrefix (L w) j AuxType.introspect b

      The actual Sample/Introspect edge preserves every CL prefix, with no assumption that the claimed question is already in the CL image.

      source
      theorem MIPRE.Introspection.TypedEstimates.sampledQuestionPrefix_mapped {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {A : Type u_5} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} [Fintype F] [DecidableEq F] [Fintype A] [Fintype PauliAnswer] (P : CL.CLFun F ι ℓ) (j : ℕ) {R : Type u_6} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (M : POVMIn (ParsedAnswer (ι → F) A PauliAnswer) R) (y : Option (ι → F)) :
      fibSumIn (POVMIn.map sampleSeed M).op (Option.map (CL.CLFun.truncate j P).eval) y = (POVMIn.map (sampledQuestionPrefix P j) M).op y

      Processing the actual sampled seed produces the actual sampled-prefix POVM, for a POVM in any ordered ⋆-ring.

      source
      theorem MIPRE.Introspection.TypedEstimates.idealZ_prefix_fibSum {F : Type u_3} {ι : Type u_4} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} [Fintype F] [DecidableEq F] {R : Type u_6} [Ring R] [Algebra ℂ R] (P : CL.CLFun F ι ℓ) (j : ℕ) (y : Option (ι → F)) :
      fibSumIn (fun (z : Option (ι → F)) => smulKron 1 (readout some z)) (Option.map (CL.CLFun.truncate j P).eval) y = smulKron 1 (Honest.hidingPrefixOp P j y)

      The same processing of ideal Z projectors is precisely the hiding prefix, including its zero malformed outcome and every impossible ambient prefix. Both are honest register operators, embedded as smulKron 1 in the matrices over any algebra.