Documentation

MIPRE.Foundations.Introspection.PrefixConditioning

Concrete adaptive prefix conditioning #

The used and remaining coordinates are those selected by the actual CL prefix. A residual operator is embedded with the concrete prefix projector. Its ambient squared error is exactly the actual prefix weight times its error on the remaining EPR register and the original auxiliary state.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): a residual operator is a block matrix over the remaining register with entries in any algebra, the prefix projector enters as smulKron M (prefixProjector P k y), and the split is regSplitHom (ambientSplit _); the exact error identity is the local isometry regSplit followed by stateSqNorm_expand_smulKron.

source
theorem MIPRE.Introspection.registerParty_kron_one {I : Type u_1} {J : Type u_2} {R : Type u_3} {๐’œ : Type u_4} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype R] [DecidableEq R] [Ring ๐’œ] [StarRing ๐’œ] [Algebra โ„‚ ๐’œ] (e : I โ‰ƒ J ร— R) (Q : Matrix J J โ„‚) :
(regSplitHom e) (smulKron 1 Q) = smulKron 1 (registerOp e (Matrix.kroneckerMap (fun (x1 x2 : โ„‚) => x1 * x2) Q 1))

The honest identity on the remaining register and the auxiliary algebra, split off a register operator Q, is Q โŠ— 1 read along the split.

source
theorem MIPRE.Introspection.prefixProjector_weight {F : Type u_1} {ฮน : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ฮน] [DecidableEq ฮน] {โ„“ : โ„•} (P : CL.CLFun F ฮน โ„“) (hP : P.SupportedOn Finset.univ) (k : โ„•) (y : ฮน โ†’ F) :
stateSqNorm (registerEPR (โ†ฅ(CLChecks.prefixRegister P k y) โ†’ F)) (Honest.prefixProjector P k y) = prefixWeight P k y

The probability of the local used-register projector is precisely the uniform CL prefix probability, with no conditional normalization premise.

source
def MIPRE.Introspection.prefixResidualOp {F : Type u_1} {ฮน : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Fintype ฮน] [DecidableEq ฮน] {โ„“ : โ„•} {๐’œ : Type u_3} [Ring ๐’œ] [StarRing ๐’œ] [Algebra โ„‚ ๐’œ] (P : CL.CLFun F ฮน โ„“) (k : โ„•) (y : ฮน โ†’ F) (M : Matrix (โ†ฅ(CLChecks.prefixRegister P k y)แถœ โ†’ F) (โ†ฅ(CLChecks.prefixRegister P k y)แถœ โ†’ F) ๐’œ) :
Matrix (ฮน โ†’ F) (ฮน โ†’ F) ๐’œ

Reinsert a residual operator behind its actual adaptive prefix projector.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem MIPRE.Introspection.prefixResidualOp_one {F : Type u_1} {ฮน : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ฮน] [DecidableEq ฮน] {โ„“ : โ„•} {๐’œ : Type u_3} [Ring ๐’œ] [StarRing ๐’œ] [Algebra โ„‚ ๐’œ] (P : CL.CLFun F ฮน โ„“) (hP : P.SupportedOn Finset.univ) (k : โ„•) (y : ฮน โ†’ F) :
    prefixResidualOp P k y 1 = smulKron 1 (Honest.hidingPrefixOp P k (some y))

    The normalizer of the reinserted residual family is exactly the ambient honest prefix projector.

    source
    theorem MIPRE.Introspection.prefixProjector_eq_zero {F : Type u_1} {ฮน : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ฮน] [DecidableEq ฮน] {โ„“ : โ„•} (P : CL.CLFun F ฮน โ„“) (k : โ„•) (y : ฮน โ†’ F) (hy : y โˆ‰ prefixOutcomes P k) :
    Honest.prefixProjector P k y = 0
    source
    theorem MIPRE.Introspection.prefixResidualOp_eq_zero {F : Type u_1} {ฮน : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ฮน] [DecidableEq ฮน] {โ„“ : โ„•} {๐’œ : Type u_3} [Ring ๐’œ] [StarRing ๐’œ] [Algebra โ„‚ ๐’œ] (P : CL.CLFun F ฮน โ„“) (k : โ„•) (y : ฮน โ†’ F) (hy : y โˆ‰ prefixOutcomes P k) (M : Matrix (โ†ฅ(CLChecks.prefixRegister P k y)แถœ โ†’ F) (โ†ฅ(CLChecks.prefixRegister P k y)แถœ โ†’ F) ๐’œ) :
    prefixResidualOp P k y M = 0
    source
    theorem MIPRE.Introspection.prefixResidualOp_sum {F : Type u_1} {ฮน : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ฮน] [DecidableEq ฮน] {โ„“ : โ„•} {๐’œ : Type u_3} [Ring ๐’œ] [StarRing ๐’œ] [Algebra โ„‚ ๐’œ] (P : CL.CLFun F ฮน โ„“) (k : โ„•) (y : ฮน โ†’ F) {A : Type u_4} [Fintype A] (M : A โ†’ Matrix (โ†ฅ(CLChecks.prefixRegister P k y)แถœ โ†’ F) (โ†ฅ(CLChecks.prefixRegister P k y)แถœ โ†’ F) ๐’œ) :
    prefixResidualOp P k y (โˆ‘ a : A, M a) = โˆ‘ a : A, prefixResidualOp P k y (M a)
    source
    theorem MIPRE.Introspection.prefixResidualOp_sub {F : Type u_1} {ฮน : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ฮน] [DecidableEq ฮน] {โ„“ : โ„•} {๐’œ : Type u_3} [Ring ๐’œ] [StarRing ๐’œ] [Algebra โ„‚ ๐’œ] (P : CL.CLFun F ฮน โ„“) (k : โ„•) (y : ฮน โ†’ F) (M N : Matrix (โ†ฅ(CLChecks.prefixRegister P k y)แถœ โ†’ F) (โ†ฅ(CLChecks.prefixRegister P k y)แถœ โ†’ F) ๐’œ) :
    prefixResidualOp P k y (M - N) = prefixResidualOp P k y M - prefixResidualOp P k y N
    source
    theorem MIPRE.Introspection.prefixResidualOp_mul {F : Type u_1} {ฮน : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ฮน] [DecidableEq ฮน] {โ„“ : โ„•} {๐’œ : Type u_3} [Ring ๐’œ] [StarRing ๐’œ] [Algebra โ„‚ ๐’œ] (P : CL.CLFun F ฮน โ„“) (k : โ„•) (y : ฮน โ†’ F) (M N : Matrix (โ†ฅ(CLChecks.prefixRegister P k y)แถœ โ†’ F) (โ†ฅ(CLChecks.prefixRegister P k y)แถœ โ†’ F) ๐’œ) :
    prefixResidualOp P k y (M * N) = prefixResidualOp P k y M * prefixResidualOp P k y N
    source
    theorem MIPRE.Introspection.stateSqNorm_prefixResidualOp {F : Type u_1} {ฮน : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ฮน] [DecidableEq ฮน] {โ„“ : โ„•} {๐’œ : Type u_3} [Ring ๐’œ] [StarRing ๐’œ] [Algebra โ„‚ ๐’œ] {๐’ž : Type u_4} {โ„ฌ : Type u_5} [Ring ๐’ž] [StarRing ๐’ž] [Algebra โ„‚ ๐’ž] [StarModule โ„‚ ๐’œ] [Ring โ„ฌ] [StarRing โ„ฌ] [Algebra โ„‚ โ„ฌ] (ฮž : BipartiteModel ๐’ž ๐’œ โ„ฌ) (P : CL.CLFun F ฮน โ„“) (hP : P.SupportedOn Finset.univ) (k : โ„•) (y : ฮน โ†’ F) (M : Matrix (โ†ฅ(CLChecks.prefixRegister P k y)แถœ โ†’ F) (โ†ฅ(CLChecks.prefixRegister P k y)แถœ โ†’ F) ๐’œ) :
    (ฮž.reg (ฮน โ†’ F)).stateSqNorm (prefixResidualOp P k y M) = prefixWeight P k y * (ฮž.reg (โ†ฅ(CLChecks.prefixRegister P k y)แถœ โ†’ F)).stateSqNorm M

    Exact conditional error, on the concrete complement of the used prefix register. It holds for every prefix, including impossible ones of weight zero.

    source
    theorem MIPRE.Introspection.hidingPrefixOp_registerState_weight {F : Type u_1} {ฮน : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ฮน] [DecidableEq ฮน] {โ„“ : โ„•} {๐’œ : Type u_3} [Ring ๐’œ] [StarRing ๐’œ] [Algebra โ„‚ ๐’œ] {๐’ž : Type u_4} {โ„ฌ : Type u_5} [Ring ๐’ž] [StarRing ๐’ž] [Algebra โ„‚ ๐’ž] [StarModule โ„‚ ๐’œ] [Ring โ„ฌ] [StarRing โ„ฌ] [Algebra โ„‚ โ„ฌ] (ฮž : BipartiteModel ๐’ž ๐’œ โ„ฌ) (P : CL.CLFun F ฮน โ„“) (hP : P.SupportedOn Finset.univ) (k : โ„•) (y : ฮน โ†’ F) (hฮž : โ€–ฮž.ฯˆโ€– = 1) :
    (ฮž.reg (ฮน โ†’ F)).stateSqNorm (smulKron 1 (Honest.hidingPrefixOp P k (some y))) = prefixWeight P k y

    Auxiliary registers do not change the prefix distribution.

    source
    theorem MIPRE.Introspection.prefixResidual_distance {F : Type u_1} {ฮน : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ฮน] [DecidableEq ฮน] {โ„“ : โ„•} {๐’œ : Type u_3} [Ring ๐’œ] [StarRing ๐’œ] [Algebra โ„‚ ๐’œ] {๐’ž : Type u_4} {โ„ฌ : Type u_5} [Ring ๐’ž] [StarRing ๐’ž] [Algebra โ„‚ ๐’ž] [StarModule โ„‚ ๐’œ] [Ring โ„ฌ] [StarRing โ„ฌ] [Algebra โ„‚ โ„ฌ] (ฮž : BipartiteModel ๐’ž ๐’œ โ„ฌ) (P : CL.CLFun F ฮน โ„“) (hP : P.SupportedOn Finset.univ) (k : โ„•) (y : ฮน โ†’ F) (M N : Matrix (โ†ฅ(CLChecks.prefixRegister P k y)แถœ โ†’ F) (โ†ฅ(CLChecks.prefixRegister P k y)แถœ โ†’ F) ๐’œ) :
    (ฮž.reg (ฮน โ†’ F)).stateSqNorm (prefixResidualOp P k y M - prefixResidualOp P k y N) = prefixWeight P k y * (ฮž.reg (โ†ฅ(CLChecks.prefixRegister P k y)แถœ โ†’ F)).stateSqNorm (M - N)
    source
    theorem MIPRE.Introspection.prefixResidual_commutator {F : Type u_1} {ฮน : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ฮน] [DecidableEq ฮน] {โ„“ : โ„•} {๐’œ : Type u_3} [Ring ๐’œ] [StarRing ๐’œ] [Algebra โ„‚ ๐’œ] {๐’ž : Type u_4} {โ„ฌ : Type u_5} [Ring ๐’ž] [StarRing ๐’ž] [Algebra โ„‚ ๐’ž] [StarModule โ„‚ ๐’œ] [Ring โ„ฌ] [StarRing โ„ฌ] [Algebra โ„‚ โ„ฌ] (ฮž : BipartiteModel ๐’ž ๐’œ โ„ฌ) (P : CL.CLFun F ฮน โ„“) (hP : P.SupportedOn Finset.univ) (k : โ„•) (y : ฮน โ†’ F) (M N : Matrix (โ†ฅ(CLChecks.prefixRegister P k y)แถœ โ†’ F) (โ†ฅ(CLChecks.prefixRegister P k y)แถœ โ†’ F) ๐’œ) :
    (ฮž.reg (ฮน โ†’ F)).stateSqNorm (prefixResidualOp P k y M * prefixResidualOp P k y N - prefixResidualOp P k y N * prefixResidualOp P k y M) = prefixWeight P k y * (ฮž.reg (โ†ฅ(CLChecks.prefixRegister P k y)แถœ โ†’ F)).stateSqNorm (M * N - N * M)
    source
    theorem MIPRE.Introspection.prefixResidual_distance_sum {F : Type u_1} {ฮน : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ฮน] [DecidableEq ฮน] {โ„“ : โ„•} {๐’œ : Type u_3} [Ring ๐’œ] [StarRing ๐’œ] [Algebra โ„‚ ๐’œ] {๐’ž : Type u_4} {โ„ฌ : Type u_5} [Ring ๐’ž] [StarRing ๐’ž] [Algebra โ„‚ ๐’ž] [StarModule โ„‚ ๐’œ] [Ring โ„ฌ] [StarRing โ„ฌ] [Algebra โ„‚ โ„ฌ] (ฮž : BipartiteModel ๐’ž ๐’œ โ„ฌ) (P : CL.CLFun F ฮน โ„“) (hP : P.SupportedOn Finset.univ) (k : โ„•) {A : (ฮน โ†’ F) โ†’ Type u_6} [(y : ฮน โ†’ F) โ†’ Fintype (A y)] (M N : (y : ฮน โ†’ F) โ†’ A y โ†’ Matrix (โ†ฅ(CLChecks.prefixRegister P k y)แถœ โ†’ F) (โ†ฅ(CLChecks.prefixRegister P k y)แถœ โ†’ F) ๐’œ) :
    โˆ‘ y : ฮน โ†’ F, โˆ‘ a : A y, (ฮž.reg (ฮน โ†’ F)).stateSqNorm (prefixResidualOp P k y (M y a) - prefixResidualOp P k y (N y a)) = โˆ‘ y : ฮน โ†’ F, prefixWeight P k y * โˆ‘ a : A y, (ฮž.reg (โ†ฅ(CLChecks.prefixRegister P k y)แถœ โ†’ F)).stateSqNorm (M y a - N y a)

    Full-carrier errors are exactly weighted residual errors under the actual CL prefix law. The residual outcome alphabet may itself depend on the prefix.

    source
    theorem MIPRE.Introspection.prefixResidual_commutator_sum {F : Type u_1} {ฮน : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ฮน] [DecidableEq ฮน] {โ„“ : โ„•} {๐’œ : Type u_3} [Ring ๐’œ] [StarRing ๐’œ] [Algebra โ„‚ ๐’œ] {๐’ž : Type u_4} {โ„ฌ : Type u_5} [Ring ๐’ž] [StarRing ๐’ž] [Algebra โ„‚ ๐’ž] [StarModule โ„‚ ๐’œ] [Ring โ„ฌ] [StarRing โ„ฌ] [Algebra โ„‚ โ„ฌ] (ฮž : BipartiteModel ๐’ž ๐’œ โ„ฌ) (P : CL.CLFun F ฮน โ„“) (hP : P.SupportedOn Finset.univ) (k : โ„•) {A : (ฮน โ†’ F) โ†’ Type u_6} {B : (ฮน โ†’ F) โ†’ Type u_7} [(y : ฮน โ†’ F) โ†’ Fintype (A y)] [(y : ฮน โ†’ F) โ†’ Fintype (B y)] (M : (y : ฮน โ†’ F) โ†’ A y โ†’ Matrix (โ†ฅ(CLChecks.prefixRegister P k y)แถœ โ†’ F) (โ†ฅ(CLChecks.prefixRegister P k y)แถœ โ†’ F) ๐’œ) (N : (y : ฮน โ†’ F) โ†’ B y โ†’ Matrix (โ†ฅ(CLChecks.prefixRegister P k y)แถœ โ†’ F) (โ†ฅ(CLChecks.prefixRegister P k y)แถœ โ†’ F) ๐’œ) :
    โˆ‘ y : ฮน โ†’ F, โˆ‘ a : A y, โˆ‘ b : B y, (ฮž.reg (ฮน โ†’ F)).stateSqNorm (prefixResidualOp P k y (M y a) * prefixResidualOp P k y (N y b) - prefixResidualOp P k y (N y b) * prefixResidualOp P k y (M y a)) = โˆ‘ y : ฮน โ†’ F, prefixWeight P k y * โˆ‘ a : A y, โˆ‘ b : B y, (ฮž.reg (โ†ฅ(CLChecks.prefixRegister P k y)แถœ โ†’ F)).stateSqNorm (M y a * N y b - N y b * M y a)