Documentation

MIPRE.Foundations.Introspection.HidingRigidity

The conditional estimate for the actual adjacent hiding test #

The earlier answer is processed using the question reported in the later answer. This is a conditional measurement, not a single fixed coarse-graining. The resulting estimate is derived from the parsed game and its actual uniform ordered-edge law, including the malformed-answer outcomes.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md).

source
def MIPRE.Introspection.conditionalCoarseDistance {๐’ž : Type u_1} {๐’œ : Type u_2} {โ„ฌ : Type u_3} [Ring ๐’ž] [StarRing ๐’ž] [Algebra โ„‚ ๐’ž] [Ring ๐’œ] [StarRing ๐’œ] [Algebra โ„‚ ๐’œ] [Ring โ„ฌ] [StarRing โ„ฌ] [Algebra โ„‚ โ„ฌ] [PartialOrder ๐’œ] [StarOrderedRing ๐’œ] [PartialOrder โ„ฌ] [StarOrderedRing โ„ฌ] (ฮจ : BipartiteModel ๐’ž ๐’œ โ„ฌ) {A : Type u_4} {B : Type u_5} {Y : Type u_6} {Z : Type u_7} [Fintype A] [Fintype B] [Fintype Y] [DecidableEq Y] [Fintype Z] [DecidableEq Z] (M : POVMIn A ๐’œ) (N : POVMIn B โ„ฌ) (f : Y โ†’ A โ†’ Z) (g : B โ†’ Y ร— Z) :
โ„

Squared error of the conditional coarse comparison, retaining Bob's conditioning index and summing every coarse outcome.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem MIPRE.Introspection.conditional_bornProb_map {๐’ž : Type u_1} {๐’œ : Type u_2} {โ„ฌ : Type u_3} [Ring ๐’ž] [StarRing ๐’ž] [Algebra โ„‚ ๐’ž] [Ring ๐’œ] [StarRing ๐’œ] [Algebra โ„‚ ๐’œ] [Ring โ„ฌ] [StarRing โ„ฌ] [Algebra โ„‚ โ„ฌ] [PartialOrder ๐’œ] [StarOrderedRing ๐’œ] [PartialOrder โ„ฌ] [StarOrderedRing โ„ฌ] (ฮจ : BipartiteModel ๐’ž ๐’œ โ„ฌ) {A : Type u_4} {B : Type u_5} {Y : Type u_6} {Z : Type u_7} [Fintype A] [Fintype B] [DecidableEq B] [Fintype Y] [DecidableEq Y] [Fintype Z] [DecidableEq Z] (M : POVMIn A ๐’œ) (N : POVMIn B โ„ฌ) (f : Y โ†’ A โ†’ Z) (g : B โ†’ Y ร— Z) :
    โˆ‘ p : Y ร— Z, ฮจ.bornProb ((POVMIn.map (f p.1) M).op p.2) ((POVMIn.map g N).op p) = โˆ‘ b : B, โˆ‘ a : A, (if f (g b).1 a = (g b).2 then 1 else 0) * ฮจ.bornProb (M.op a) (N.op b)

    Data processing when Alice's outcome map depends on a retained part of Bob's outcome. The dependency remains inside the Born sum.

    source
    theorem MIPRE.Introspection.conditional_coarse_consistency {๐’ž : Type u_1} {๐’œ : Type u_2} {โ„ฌ : Type u_3} [Ring ๐’ž] [StarRing ๐’ž] [Algebra โ„‚ ๐’ž] [Ring ๐’œ] [StarRing ๐’œ] [Algebra โ„‚ ๐’œ] [Ring โ„ฌ] [StarRing โ„ฌ] [Algebra โ„‚ โ„ฌ] [PartialOrder ๐’œ] [StarOrderedRing ๐’œ] [PartialOrder โ„ฌ] [StarOrderedRing โ„ฌ] (ฮจ : BipartiteModel ๐’ž ๐’œ โ„ฌ) {A : Type u_4} {B : Type u_5} {Y : Type u_6} {Z : Type u_7} [Fintype A] [Fintype B] [DecidableEq B] [Fintype Y] [DecidableEq Y] [Fintype Z] [DecidableEq Z] (hฮจ : โ€–ฮจ.ฯˆโ€– = 1) (M : POVMIn A ๐’œ) (N : POVMIn B โ„ฌ) (hN : IsPVMIn N.op) (f : Y โ†’ A โ†’ Z) (g : B โ†’ Y ร— Z) (test : A โ†’ B โ†’ Bool) {ฮด : โ„} (hwin : 1 - ฮด โ‰ค โˆ‘ a : A, โˆ‘ b : B, (if test a b = true then 1 else 0) * ฮจ.bornProb (M.op a) (N.op b)) (hcheck : โˆ€ (a : A) (b : B), test a b = true โ†’ f (g b).1 a = (g b).2) :
    conditionalCoarseDistance ฮจ M N f g โ‰ค 2 * ฮด

    Conditional consistency for an actual pair of measurements and explicit outcome maps. The acceptance premise is solely a scalar tested probability.

    source
    theorem MIPRE.Introspection.CLChecks.proj_outputPrefix_cons {F : Type u_1} {ฮน : Type u_2} [Field F] [Fintype ฮน] [DecidableEq ฮน] {โ„“ : โ„•} {S T : Finset ฮน} {L : CL.RegLinear F S} {next : (ฮน โ†’ F) โ†’ CL.CLFun F ฮน โ„“} (hP : (CL.CLFun.cons S L next).SupportedOn T) (k : โ„•) (y : ฮน โ†’ F) :
    (CL.proj S) ((CL.CLFun.cons S L next).outputPrefix (k + 1) y) = (CL.proj S) y โˆง (CL.proj Sแถœ) ((CL.CLFun.cons S L next).outputPrefix (k + 1) y) = (next ((CL.proj S) y)).outputPrefix k ((CL.proj Sแถœ) y)

    Projecting an arbitrary claimed prefix recovers its first branch and the remaining claimed prefix. No image-membership hypothesis is needed.

    source
    theorem MIPRE.Introspection.CLChecks.prefixRegister_outputPrefix_succ {F : Type u_1} {ฮน : Type u_2} [Field F] [Fintype ฮน] [DecidableEq ฮน] {โ„“ : โ„•} {P : CL.CLFun F ฮน โ„“} {T : Finset ฮน} (hP : P.SupportedOn T) (k : โ„•) (y : ฮน โ†’ F) :
    prefixRegister P (k + 1) (P.outputPrefix k y) = prefixRegister P (k + 1) y

    The register of the next stage is already fixed by the reported prefix.

    source
    theorem MIPRE.Introspection.CLChecks.dualReadout_outputPrefix {F : Type u_1} {ฮน : Type u_2} [Field F] [Fintype ฮน] [DecidableEq ฮน] {โ„“ : โ„•} {P : CL.CLFun F ฮน โ„“} {T : Finset ฮน} (hP : P.SupportedOn T) (k : โ„•) (y x : ฮน โ†’ F) :
    dualReadout P k (P.outputPrefix k y) x = dualReadout P k y x

    The next dual readout depends only on the preceding reported prefix.

    source
    def MIPRE.Introspection.TypedEstimates.hidingNextCondition {PauliAnswer : Type u_2} {F : Type u_3} {ฮน : Type u_4} {A : Type u_6} [Field F] [Fintype ฮน] [DecidableEq ฮน] {โ„“ : โ„•} (P : CL.CLFun F ฮน โ„“) (k : โ„•) :
    ParsedAnswer (ฮน โ†’ F) A PauliAnswer โ†’ Option (ฮน โ†’ F)

    Retain exactly the later hiding answer's preceding question prefix as the conditioning index. Malformed answers retain a separate index.

    Equations
    Instances For
      source
      noncomputable def MIPRE.Introspection.TypedEstimates.hidingNextEarlier {PauliAnswer : Type u_2} {F : Type u_3} {ฮน : Type u_4} {A : Type u_6} [Field F] [Fintype ฮน] [DecidableEq ฮน] {โ„“ : โ„•} (P : CL.CLFun F ฮน โ„“) (k : โ„•) (v : Option (ฮน โ†’ F)) :
      ParsedAnswer (ฮน โ†’ F) A PauliAnswer โ†’ Option ((ฮน โ†’ F) ร— (ฮน โ†’ F) ร— (ฮน โ†’ F))

      Process the earlier answer using the later reported question. The output retains the earlier prefix, the new dual readout, and the untouched tail.

      Equations
      Instances For
        source
        def MIPRE.Introspection.TypedEstimates.hidingNextLater {PauliAnswer : Type u_2} {F : Type u_3} {ฮน : Type u_4} {A : Type u_6} [Field F] [Fintype ฮน] [DecidableEq ฮน] {โ„“ : โ„•} (P : CL.CLFun F ฮน โ„“) (k : โ„•) (a : ParsedAnswer (ฮน โ†’ F) A PauliAnswer) :
        Option (ฮน โ†’ F) ร— Option ((ฮน โ†’ F) ร— (ฮน โ†’ F) ร— (ฮน โ†’ F))

        The actual coarse later answer. Both the factor for the new dual output and the tail projector use that answer's own reported question.

        Equations
        Instances For
          source
          theorem MIPRE.Introspection.TypedEstimates.hiding_next_accepts_conditional {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ฮน : Type u_4} {A : Type u_6} [Fintype PauliType] [DecidableEq PauliType] [Fintype PauliAnswer] [Field F] [Fintype F] [DecidableEq F] [Fintype ฮน] [DecidableEq ฮน] [Fintype A] {โ„“ : โ„•} (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) (k j : Fin โ„“) (hk : โ†‘k + 1 = โ†‘j) (hL : (L w).SupportedOn Finset.univ) {a b : ParsedAnswer (ฮน โ†’ F) A PauliAnswer} (h : TypedPredicate.check L X Z projectPauli D DP (QuestionType.hide w k) (QuestionType.hide w j) a b = true) :
          hidingNextEarlier (L w) (โ†‘k) (hidingNextLater (L w) (โ†‘k) b).1 a = (hidingNextLater (L w) (โ†‘k) b).2

          The parsed adjacent-hiding check supplies the conditional accepted-answer relation; no condition on honestly sampled or in-image answers is imposed.

          source
          theorem MIPRE.Introspection.TypedEstimates.hiding_next_conditional_estimate {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ฮน : Type u_4} {ฮบ : Type u_5} {A : Type u_6} [Fintype PauliType] [DecidableEq PauliType] [Fintype PauliAnswer] [Field F] [Fintype F] [DecidableEq F] [Fintype ฮน] [DecidableEq ฮน] [Fintype ฮบ] [DecidableEq ฮบ] [Fintype A] {โ„“ : โ„•} {๐’ž : Type u_7} {๐’œ : Type u_8} {โ„ฌ : Type u_9} [Ring ๐’ž] [StarRing ๐’ž] [Algebra โ„‚ ๐’ž] [Ring ๐’œ] [StarRing ๐’œ] [Algebra โ„‚ ๐’œ] [Ring โ„ฌ] [StarRing โ„ฌ] [Algebra โ„‚ โ„ฌ] [PartialOrder ๐’œ] [StarOrderedRing ๐’œ] [PartialOrder โ„ฌ] [StarOrderedRing โ„ฌ] (E : PauliType โ†’ PauliType โ†’ Bool) (X Z : PauliType) (P : PauliType โ†’ CL.CLFun (ZMod 2) ฮบ 3) (L : Bool โ†’ CL.CLFun F ฮน โ„“) (projectPauli : PauliAnswer โ†’ ฮน โ†’ F) (D : (ฮน โ†’ F) โ†’ (ฮน โ†’ F) โ†’ A โ†’ A โ†’ Bool) (DP : PauliType โ†’ PauliType โ†’ (ฮบ โ†’ ZMod 2) โ†’ (ฮบ โ†’ ZMod 2) โ†’ PauliAnswer โ†’ PauliAnswer โ†’ Bool) (ฮจ : BipartiteModel ๐’ž ๐’œ โ„ฌ) (hฮจ : โ€–ฮจ.ฯˆโ€– = 1) (MA : CL.Detyping.Question (QuestionType PauliType โ„“) ฮบ โ†’ POVMIn (ParsedAnswer (ฮน โ†’ F) A PauliAnswer) ๐’œ) (MB : CL.Detyping.Question (QuestionType PauliType โ„“) ฮบ โ†’ POVMIn (ParsedAnswer (ฮน โ†’ F) A PauliAnswer) โ„ฌ) {ฮต : โ„} (hfail : 1 - ฮจ.povmValue (parsedGame E X Z P L projectPauli D DP) MA MB โ‰ค ฮต) (w : Bool) (k j : Fin โ„“) (hk : โ†‘k + 1 = โ†‘j) (hL : (L w).SupportedOn Finset.univ) (hMB : IsPVMIn (MB (QuestionType.hide w j, 0)).op) :
          conditionalCoarseDistance ฮจ (MA (QuestionType.hide w k, 0)) (MB (QuestionType.hide w j, 0)) (hidingNextEarlier (L w) โ†‘k) (hidingNextLater (L w) โ†‘k) โ‰ค 2 * โ†‘(TypeGraph.edges E X Z โ„“).card * ฮต

          Actual adjacent-hiding conditional estimate. The source induction's first step follows from the parsed verifier with error 2 |E| ฮต. Alice's coarse measurement depends on Bob's retained question; Bob's marginal is the sum over all tested coarse answers. This is not an unconditional marginal distance and does not assume the later ideal hiding form.