Documentation

MIPRE.Background.LIDT.Co.Chain.Defs

The model chain, part 1: the canonical-line test in a bipartite model #

The first file of the model chain from the canonical-line theorem to MIPRE.LIDT.Simul.SoundIn, in the port of planning/c6b-plan.md (milestone M14, unit M14-3). It has no vendored counterpart: it restates, over any bipartite model M : MIPRE.BipartiteModel ๐’ž ๐’œ โ„ฌ with the instance set of SoundIn (the two players' algebras star-ordered โ‹†-rings), the vocabulary of the repository's matrix statement MIPRE.LIDT.lowIndividualDegree_soundness (MIPRE/Background/LIDT/Game.lean, Soundness.lean), which stays: it is the tensor instance, and serves soundIn_tensor.

soundLidtIn_tensor checks the statement against the matrix theorem: in the tensor-product model of a state on Fin a ร— Fin b it is lowIndividualDegree_soundness, through BipartiteModel.ProjStrat.toTensor and inconsistency_eq_tensor, exactly as soundIn_tensor reads clSoundness.

Not ported #

Nothing of Game.lean or Soundness.lean is redeclared: the game, its alphabets, lidtError and LowIndDegPoly.eval are classical, imported. The matrix readings pointPOVMA, pointPOVMB and evalPOVM keep their matrix form (they serve the tensor instance), and their model forms here carry the suffix In, as MIPRE.LIDT.Simul.tuplePOVMAIn does for tuplePOVMA.

New here #

The readings of the conclusions #

source
def MIPRE.LIDT.Co.Chain.pointPOVMAIn {๐’ž : Type u_1} {๐’œ : Type u_2} {โ„ฌ : Type u_3} [Ring ๐’ž] [StarRing ๐’ž] [Algebra โ„‚ ๐’ž] [Ring ๐’œ] [StarRing ๐’œ] [Algebra โ„‚ ๐’œ] [Ring โ„ฌ] [StarRing โ„ฌ] [Algebra โ„‚ โ„ฌ] [PartialOrder ๐’œ] [StarOrderedRing ๐’œ] [PartialOrder โ„ฌ] {M : BipartiteModel ๐’ž ๐’œ โ„ฌ} {F : Type u_4} [Field F] [Fintype F] [DecidableEq F] {m d : โ„•} [NeZero m] (S : M.ProjStrat (lidtGame F m d)) (u : Point F m) :
POVMIn F ๐’œ

The first player's point measurements of a projective strategy for the canonical-line test, as POVMs with outcomes in F (the model form of MIPRE.LIDT.pointPOVMA).

Equations
Instances For
    source
    def MIPRE.LIDT.Co.Chain.pointPOVMBIn {๐’ž : Type u_1} {๐’œ : Type u_2} {โ„ฌ : Type u_3} [Ring ๐’ž] [StarRing ๐’ž] [Algebra โ„‚ ๐’ž] [Ring ๐’œ] [StarRing ๐’œ] [Algebra โ„‚ ๐’œ] [Ring โ„ฌ] [StarRing โ„ฌ] [Algebra โ„‚ โ„ฌ] [PartialOrder ๐’œ] [PartialOrder โ„ฌ] [StarOrderedRing โ„ฌ] {M : BipartiteModel ๐’ž ๐’œ โ„ฌ} {F : Type u_4} [Field F] [Fintype F] [DecidableEq F] {m d : โ„•} [NeZero m] (S : M.ProjStrat (lidtGame F m d)) (u : Point F m) :
    POVMIn F โ„ฌ

    The second player's point measurements, as for pointPOVMAIn (the model form of MIPRE.LIDT.pointPOVMB).

    Equations
    Instances For
      source
      def MIPRE.LIDT.Co.Chain.evalPOVMIn {F : Type u_4} [Field F] [Fintype F] [DecidableEq F] {m d : โ„•} {R : Type u_5} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (G : POVMIn LowIndDegPoly R) (u : Point F m) :
      POVMIn F R

      A POVM with outcomes in the polynomials of individual degree d, evaluated at u (the model form of MIPRE.LIDT.evalPOVM): the outcome a gets the sum of the operators of the polynomials g with g(u) = a.

      Equations
      Instances For

        The canonical-line theorem in a model #

        source
        def MIPRE.LIDT.Co.Chain.SoundLidtIn {๐’ž : Type u_1} {๐’œ : Type u_2} {โ„ฌ : Type u_3} [Ring ๐’ž] [StarRing ๐’ž] [Algebra โ„‚ ๐’ž] [Ring ๐’œ] [StarRing ๐’œ] [Algebra โ„‚ ๐’œ] [Ring โ„ฌ] [StarRing โ„ฌ] [Algebra โ„‚ โ„ฌ] [PartialOrder ๐’œ] [StarOrderedRing ๐’œ] [PartialOrder โ„ฌ] [StarOrderedRing โ„ฌ] (M : BipartiteModel ๐’ž ๐’œ โ„ฌ) :
        Prop

        The canonical-line theorem in the bipartite model M (T(M) of reports/lidt-co-audit.md ยง3.2): MIPRE.LIDT.lowIndividualDegree_soundness read in M, with 1 โ‰ค d added. A projective strategy in M passing the (m, q, d)-low individual degree test with probability at least 1 - ฮต admits, for every positive k โ‰ฅ 400 m d, projective measurements GA in the first player's algebra and GB in the second's, with outcomes the polynomials of individual degree d, whose evaluations at a uniform point are consistent with the other player's point measurements, and which are consistent with each other, all with error lidtError m d q k ฮต.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          The tensor-product instance #

          source
          theorem MIPRE.LIDT.Co.Chain.pointPOVMA_toTensor {F : Type u_4} [Field F] [Fintype F] [DecidableEq F] {m d : โ„•} [NeZero m] {a b : โ„•} {ฯˆ : Fin a ร— Fin b โ†’ โ„‚} (S : (BipartiteModel.tensor ฯˆ).ProjStrat (lidtGame F m d)) (u : Point F m) :
          (pointPOVMA S.toTensor u).toIn = pointPOVMAIn S u

          The matrix point measurements of the tensor-product strategy are the model's.

          source
          theorem MIPRE.LIDT.Co.Chain.pointPOVMB_toTensor {F : Type u_4} [Field F] [Fintype F] [DecidableEq F] {m d : โ„•} [NeZero m] {a b : โ„•} {ฯˆ : Fin a ร— Fin b โ†’ โ„‚} (S : (BipartiteModel.tensor ฯˆ).ProjStrat (lidtGame F m d)) (u : Point F m) :
          (pointPOVMB S.toTensor u).toIn = pointPOVMBIn S u

          The matrix point measurements of the tensor-product strategy are the model's.

          source
          theorem MIPRE.LIDT.Co.Chain.evalPOVM_toIn {F : Type u_4} [Field F] [Fintype F] [DecidableEq F] {m d : โ„•} {n : Type u_5} [Fintype n] [DecidableEq n] (G : ProjectiveMeasurement Unit LowIndDegPoly (Matrix n n โ„‚)) (u : Point F m) :
          (evalPOVM G u).toIn = evalPOVMIn (G.toPOVM ()).toIn u

          The matrix evaluation of a projective measurement is the model's evaluation of its POVM.

          source
          theorem MIPRE.LIDT.Co.Chain.soundLidtIn_tensor {a b : โ„•} (ฯˆ : Fin a ร— Fin b โ†’ โ„‚) :
          SoundLidtIn (BipartiteModel.tensor ฯˆ)

          The canonical-line theorem holds in the tensor-product model of every state on Fin a ร— Fin b: lowIndividualDegree_soundness, for the tensor-product strategy the projective strategy is (the hypothesis 1 โ‰ค d is not used).