Mixing on the actual adaptive continuation

The prefix law, next linear map, and remaining coordinates are computed from the CL presentation. Full-carrier errors of prefix-conditioned operators give the weighted hypotheses of mixing exactly. The constructed residual POVM acts on the complement of the next prefix, with the original ancilla.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the full-carrier errors are measured in the register model Ξ.reg (ι → F), and a residual operator at the prefix y is a block matrix over the unvisited register stageRemaining P k y → F with entries in the first player's algebra, whose error is measured in the residual model Ξ.reg (stageRemaining P k y → F). Ambient mixing is applied to the one model Ξ with this prefix-dependent family of registers, weighted by the prefix law. The constructed POVMs are block matrices over the next unvisited register, entering along the split as regSplitHom (stageSplit P hP k y) (smulKron _ _).

@[reducible, inline]

abbrev MIPRE.Introspection.stageRemaining {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (y : ι → F) : Finset ι

The unvisited coordinates at an actual claimed prefix.

Equations

• MIPRE.Introspection.stageRemaining P k y = (MIPRE.Introspection.CLChecks.prefixRegister P k y)ᶜ

theorem MIPRE.Introspection.stageFactor_subset_remaining {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (y : ι → F) : P.factorOfPrefix k y ⊆ stageRemaining P k y

theorem MIPRE.Introspection.stageRemaining_step {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (y : ι → F) : stageRemaining P k y \ P.factorOfPrefix k y = stageRemaining P (k + 1) y

The output support of mixing is precisely the next unvisited register.

noncomputable def MIPRE.Introspection.stageSplit {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (y : ι → F) : (↥(stageRemaining P k y) → F) ≃ (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) × (↥(stageRemaining P k y \ P.factorOfPrefix k y) → F)

Split the actual remaining register into its next factor and its continuation.

Equations

• MIPRE.Introspection.stageSplit P hP k y = MIPRE.Introspection.coordinateSplit (P.factorOfPrefix k y) (MIPRE.Introspection.stageRemaining P k y) ⋯

noncomputable def MIPRE.Introspection.prefixStageMarginalError {ι : Type u_1} {F : Type u_2} {A : Type u_3} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] {ℓ : ℕ} {𝒞 : Type u_4} {𝒜 : Type u_5} {ℬ : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (M : (y : ι → F) → (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) × A → Matrix (↥(stageRemaining P k y) → F) (↥(stageRemaining P k y) → F) 𝒜) : ℝ

Full-carrier marginal error, retaining its actual adaptive prefix projector.

Equations

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

noncomputable def MIPRE.Introspection.prefixStageCommutatorError {ι : Type u_1} {F : Type u_2} {A : Type u_3} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] {ℓ : ℕ} {𝒞 : Type u_4} {𝒜 : Type u_5} {ℬ : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (M : (y : ι → F) → (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) × A → Matrix (↥(stageRemaining P k y) → F) (↥(stageRemaining P k y) → F) 𝒜) (w : (y : ι → F) → (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) → Matrix (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) ℂ) (L : (y : ι → F) → (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) →ₗ[F] Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) : ℝ

Full-carrier commutation error with the actual prefix left in place.

Equations

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

theorem MIPRE.Introspection.prefixStageMarginalError_eq {ι : Type u_1} {F : Type u_2} {A : Type u_3} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {ℓ : ℕ} {𝒞 : Type u_4} {𝒜 : Type u_5} {ℬ : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (M : (y : ι → F) → (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) × A → Matrix (↥(stageRemaining P k y) → F) (↥(stageRemaining P k y) → F) 𝒜) : prefixStageMarginalError P hP k Ξ M = ∑ y : ι → F, prefixWeight P k y * ambientMarginalError (P.factorOfPrefix k y) (stageRemaining P k y) ⋯ (CLChecks.stageLinear P k y) Ξ (M y)

theorem MIPRE.Introspection.prefixStageCommutatorError_eq {ι : Type u_1} {F : Type u_2} {A : Type u_3} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {ℓ : ℕ} {𝒞 : Type u_4} {𝒜 : Type u_5} {ℬ : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (M : (y : ι → F) → (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) × A → Matrix (↥(stageRemaining P k y) → F) (↥(stageRemaining P k y) → F) 𝒜) (w : (y : ι → F) → (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) → Matrix (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) ℂ) (L : (y : ι → F) → (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) →ₗ[F] Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) : prefixStageCommutatorError P hP k Ξ M w L = ∑ y : ι → F, prefixWeight P k y * ambientCommutatorError (P.factorOfPrefix k y) (stageRemaining P k y) ⋯ Ξ (M y) (w y) (L y)

theorem MIPRE.Introspection.exists_adaptive_prefix_mixing {ι : Type u_1} {F : Type u_2} {A : Type u_3} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {ℓ : ℕ} {𝒞 : Type u_4} {𝒜 : Type u_5} {ℬ : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (hΞ : ‖Ξ.ψ‖ = 1) (M : (y : ι → F) → POVMIn ((Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) × A) (Matrix (↥(stageRemaining P k y) → F) (↥(stageRemaining P k y) → F) 𝒜)) (hM : ∀ (y : ι → F), IsPVMIn (M y).op) {ε : ℝ} (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) (hmarg : (prefixStageMarginalError P hP k Ξ fun (y : ι → F) => (M y).op) ≤ ε) (hZ : (prefixStageCommutatorError P hP k Ξ (fun (y : ι → F) => (M y).op) (fun (x : ι → F) => Weyl.wZ) fun (x : ι → F) => LinearMap.id) ≤ ε) (hX : (prefixStageCommutatorError P hP k Ξ (fun (y : ι → F) => (M y).op) (fun (x : ι → F) => Weyl.wX) fun (y : ι → F) => CL.lperp (coordinateLinear (CLChecks.stageLinear P k y))) ≤ ε) : ∃ (Q : (y : ι → F) → (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) → POVMIn A (Matrix (↥(stageRemaining P k y \ P.factorOfPrefix k y) → F) (↥(stageRemaining P k y \ P.factorOfPrefix k y) → F) 𝒜)), ∑ y : ι → F, ∑ p : (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) × A, (Ξ.reg (ι → F)).stateSqNorm (prefixResidualOp P k y ((M y).op p) - prefixResidualOp P k y ((regSplitHom (stageSplit P hP k y)) (smulKron ((Q y p.1).op p.2) (Weyl.synOf Weyl.wZ (⇑(coordinateLinear (CLChecks.stageLinear P k y))) p.1)))) ≤ 56 * √ε

One adaptive extraction step. The three errors are measured on the original EPR-plus-auxiliary state. The theorem constructs the next residual POVMs on the actual next unvisited coordinates; no prefix distribution, support identification, or product-form conclusion is an input.