Pauli mixing in question-dependent coordinate presentations

The number of sampled coordinates and both ancillary spaces can depend on the question. This is the form used after splitting a retained register from its complement. The register's ambient embeddings are not part of this statement.

In a bipartite model (Phase 4 of planning/mipco-track.md) the ancillary state of each question is a model Ξ x, over algebras that may depend on the question too.

theorem MIPRE.Introspection.exists_pauli_mixing_varying {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {X : Type u_2} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] {n : X → ℕ} {𝒞 : X → Type u_4} {𝒜 : X → Type u_5} {ℬ : X → Type u_6} [(x : X) → Ring (𝒞 x)] [(x : X) → StarRing (𝒞 x)] [(x : X) → Algebra ℂ (𝒞 x)] [(x : X) → Ring (𝒜 x)] [(x : X) → StarRing (𝒜 x)] [(x : X) → Algebra ℂ (𝒜 x)] [∀ (x : X), StarModule ℂ (𝒜 x)] [(x : X) → PartialOrder (𝒜 x)] [∀ (x : X), StarOrderedRing (𝒜 x)] [∀ (x : X), StarProper (𝒜 x)] [(x : X) → Ring (ℬ x)] [(x : X) → StarRing (ℬ x)] [(x : X) → Algebra ℂ (ℬ x)] [∀ (x : X), StarModule ℂ (ℬ x)] (D : X → ℝ) (hD0 : ∀ (x : X), 0 ≤ D x) (hD1 : ∑ x : X, D x = 1) (L : (x : X) → (Fin (n x) → F) →ₗ[F] Fin (n x) → F) (Ξ : (x : X) → BipartiteModel (𝒞 x) (𝒜 x) (ℬ x)) (hΞ : ∀ (x : X), ‖(Ξ x).ψ‖ = 1) (M : (x : X) → POVMIn ((Fin (n x) → F) × A) (Matrix (Fin (n x) → F) (Fin (n x) → F) (𝒜 x))) (hM : ∀ (x : X), IsPVMIn (M x).op) {δ : ℝ} (hδ : ∑ x : X, D x * mixingError (L x) (Ξ x) (M x) ≤ δ) : ∃ (Q : (x : X) → (Fin (n x) → F) → POVMIn A (𝒜 x)), ∑ x : X, D x * ∑ p : (Fin (n x) → F) × A, ((Ξ x).reg (Fin (n x) → F)).stateSqNorm ((M x).op p - smulKron ((Q x p.1).op p.2) (Weyl.synOf Weyl.wZ (⇑(L x)) p.1)) ≤ 2 * δ + 4 * √δ

Averaged mixing when the retained register and its complement vary with the question.

theorem MIPRE.Introspection.mixing_error_sqrt_bound {ε : ℝ} (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) : 2 * (18 * ε) + 4 * √(18 * ε) ≤ 56 * √ε

A convenient universal constant for three error hypotheses bounded by ε ≤ 1.

theorem MIPRE.Introspection.exists_pauli_mixing_sqrt {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {X : Type u_2} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] {n : X → ℕ} {𝒞 : X → Type u_4} {𝒜 : X → Type u_5} {ℬ : X → Type u_6} [(x : X) → Ring (𝒞 x)] [(x : X) → StarRing (𝒞 x)] [(x : X) → Algebra ℂ (𝒞 x)] [(x : X) → Ring (𝒜 x)] [(x : X) → StarRing (𝒜 x)] [(x : X) → Algebra ℂ (𝒜 x)] [∀ (x : X), StarModule ℂ (𝒜 x)] [(x : X) → PartialOrder (𝒜 x)] [∀ (x : X), StarOrderedRing (𝒜 x)] [∀ (x : X), StarProper (𝒜 x)] [(x : X) → Ring (ℬ x)] [(x : X) → StarRing (ℬ x)] [(x : X) → Algebra ℂ (ℬ x)] [∀ (x : X), StarModule ℂ (ℬ x)] (D : X → ℝ) (hD0 : ∀ (x : X), 0 ≤ D x) (hD1 : ∑ x : X, D x = 1) (L : (x : X) → (Fin (n x) → F) →ₗ[F] Fin (n x) → F) (Ξ : (x : X) → BipartiteModel (𝒞 x) (𝒜 x) (ℬ x)) (hΞ : ∀ (x : X), ‖(Ξ x).ψ‖ = 1) (M : (x : X) → POVMIn ((Fin (n x) → F) × A) (Matrix (Fin (n x) → F) (Fin (n x) → F) (𝒜 x))) (hM : ∀ (x : X), IsPVMIn (M x).op) {ε : ℝ} (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) (hmarg : ∑ x : X, D x * readoutMarginalError (L x) ((Ξ x).reg (Fin (n x) → F)) (M x).op ≤ ε) (hZ : ∑ x : X, D x * readoutCommutatorError ((Ξ x).reg (Fin (n x) → F)) (M x).op Weyl.wZ LinearMap.id ≤ ε) (hX : ∑ x : X, D x * readoutCommutatorError ((Ξ x).reg (Fin (n x) → F)) (M x).op Weyl.wX (CL.lperp (L x)) ≤ ε) : ∃ (Q : (x : X) → (Fin (n x) → F) → POVMIn A (𝒜 x)), ∑ x : X, D x * ∑ p : (Fin (n x) → F) × A, ((Ξ x).reg (Fin (n x) → F)).stateSqNorm ((M x).op p - smulKron ((Q x p.1).op p.2) (Weyl.synOf Weyl.wZ (⇑(L x)) p.1)) ≤ 56 * √ε

The three readout hypotheses yield a dimension-independent 56 sqrt ε bound.