structure CommutingRepetition.TensorPowerData (N₁ : StdTracialAlgebra) (R : ℕ) : Type (u + 1)

Tensor power in consumed form (06_otqcs.tex, eq amplified-resource): a standard-form algebra N̂ with one unital ∗-embedding per tensor factor, images at distinct factors commuting, and the trace multiplicative over ordered products with one element from each factor. Work package B3b provides the instance (exists_tensorPowerData).

• Nhat : StdTracialAlgebra
• emb : Fin R → N₁.A →⋆ₐ[ℂ] self.Nhat.A
• emb_commute ⦃i j : Fin R⦄ : i ≠ j → ∀ (a b : N₁.A), Commute ((self.emb i) a) ((self.emb j) b)
• trace_prod (f : Fin R → N₁.A) : self.Nhat.τ (List.ofFn fun (j : Fin R) => (self.emb j) (f j)).prod = ∏ j : Fin R, N₁.τ (f j)

theorem CommutingRepetition.exists_tensorPowerData (N₁ : StdTracialAlgebra) (R : ℕ) : Nonempty (TensorPowerData N₁ R)

Existence of tensor powers of a standard tracial algebra (work package B3b; 06_otqcs.tex, thm otqcs item 1 "finitely many normalized matrix amplifications and tensor powers").

noncomputable def CommutingRepetition.tensorState {N₁ : StdTracialAlgebra} {R : ℕ} (D : TensorPowerData N₁ R) (u : N₁.A) : D.Nhat.H

The product state vector: the GNS image of the ordered product of one copy of u per factor — ω^{⊗R} for ω = ι(u) (06_otqcs.tex, eq amplified-resource, Ω = ω₀^{⊗R}).

Equations

• CommutingRepetition.tensorState D u = D.Nhat.ι (List.ofFn fun (j : Fin R) => (D.emb j) u).prod

Algebraic positivity helpers (for the compiled-effect positivity)

theorem CommutingRepetition.isPosElem_of_projection {A : Type u_1} [Ring A] [StarRing A] {a : A} (hsa : star a = a) (hidem : a * a = a) : IsPosElem a

A self-adjoint idempotent is algebraically positive: a = (star a) * a.

theorem CommutingRepetition.IsPosElem.conjug {A : Type u_1} [Ring A] [StarRing A] {x : A} (hx : IsPosElem x) (k : A) : IsPosElem (star k * x * k)

Conjugation preserves algebraic positivity: star k * x * k for positive x.

theorem CommutingRepetition.IsPosElem.conjug' {A : Type u_1} [Ring A] [StarRing A] {x : A} (hx : IsPosElem x) (k : A) : IsPosElem (k * x * star k)

Mirror conjugation k * x * star k for positive x.

theorem CommutingRepetition.IsPosElem.starAlgHom_map {A : Type u_1} {B : Type u_2} [Ring A] [StarRing A] [Algebra ℂ A] [StarModule ℂ A] [Ring B] [StarRing B] [Algebra ℂ B] [StarModule ℂ B] (f : A →⋆ₐ[ℂ] B) {x : A} (hx : IsPosElem x) : IsPosElem (f x)

A ⋆-algebra homomorphism maps positive elements to positive elements.

theorem CommutingRepetition.single_isPosElem {n : Type u_1} [Fintype n] [DecidableEq n] {A : Type u_2} [Ring A] [StarRing A] (i : n) {P : A} (hP : IsPosElem P) : IsPosElem (Matrix.single i i P)

The diagonal matrix corner single i i P of a positive P is positive.

theorem CommutingRepetition.noncommProd_proj {A : Type u_1} [Ring A] [StarRing A] {ι : Type u_2} [DecidableEq ι] (g : ι → A) (hsa : ∀ (i : ι), star (g i) = g i) (hidem : ∀ (i : ι), g i * g i = g i) (hcomm : ∀ (i j : ι), Commute (g i) (g j)) (s : Finset ι) (comm : (↑s).Pairwise (Function.onFun Commute g)) : star (s.noncommProd g comm) = s.noncommProd g comm ∧ s.noncommProd g comm * s.noncommProd g comm = s.noncommProd g comm

noncommProd of a pairwise-commuting family of self-adjoint idempotents is a self-adjoint idempotent.

theorem CommutingRepetition.noncommProd_isPosElem {A : Type u_1} [Ring A] [StarRing A] {ι : Type u_2} [DecidableEq ι] (g : ι → A) (hsa : ∀ (i : ι), star (g i) = g i) (hidem : ∀ (i : ι), g i * g i = g i) (hcomm : ∀ (i j : ι), Commute (g i) (g j)) (s : Finset ι) (comm : (↑s).Pairwise (Function.onFun Commute g)) : IsPosElem (s.noncommProd g comm)

Hence such a noncommProd is algebraically positive.

theorem CommutingRepetition.noncommProd_prefix_telescope {A : Type u_1} [Ring A] {R : ℕ} (q : Fin R → A) (hcomm : ∀ (i j : Fin R), Commute (q i) (q j)) : ∑ j : Fin R, {ℓ : Fin R | ℓ < j}.noncommProd q ⋯ * (1 - q j) + Finset.univ.noncommProd q ⋯ = 1

First-success telescope for a pairwise-commuting family q (eq first-success-telescope): ∑_j (∏_{ℓ<j} q_ℓ)(1 − q_j) + ∏_ℓ q_ℓ = 1.

theorem CommutingRepetition.ofFn_prod_mul_ofFn_prod {A : Type u_1} [Monoid A] {R : ℕ} (p q : Fin R → A) (h : ∀ (i j : Fin R), i ≠ j → Commute (p i) (q j)) : (List.ofFn p).prod * (List.ofFn q).prod = (List.ofFn fun (j : Fin R) => p j * q j).prod

Ordered products of two families interleave factorwise when the factors at distinct indices commute across the families.

theorem CommutingRepetition.ofFn_prod_star {A : Type u_1} [Monoid A] [StarMul A] {R : ℕ} (p : Fin R → A) (h : ∀ (i j : Fin R), i ≠ j → Commute (p i) (p j)) : star (List.ofFn p).prod = (List.ofFn fun (j : Fin R) => star (p j)).prod

The star of an ordered product of a pairwise-commuting family is the ordered product of the stars (the reversal is absorbed by the commutation).

theorem CommutingRepetition.tensorState_norm {N₁ : StdTracialAlgebra} {R : ℕ} (D : TensorPowerData N₁ R) (u : N₁.A) (hu : ‖N₁.ι u‖ = 1) : ‖tensorState D u‖ = 1

Proof-side helper: the product state of a unit vector is a unit vector, ‖ω^{⊗R}‖² = ∏_j τ(ω*ω) = 1, from trace_prod after interleaving the two ordered products through the cross-factor commutation.

Tensor words and the diagonal branch trace

Proof-side toolkit for the branch decomposition (compile_decomposition): ordered products with one embedded element per tensor factor, the pairing algebra of a standard tracial algebra, and the factorization of a Kraus-branch pairing over the tensor factors (appendix eq common-index-vector).

Ordered products with one entry per index

theorem CommutingRepetition.ofFn_prod_ite_eq {A : Type u_1} [Monoid A] {R : ℕ} (j : Fin R) (f : Fin R → A) : (List.ofFn fun (ℓ : Fin R) => if ℓ = j then f ℓ else 1).prod = f j

A List.ofFn product whose entries are 1 except at j equals the entry at j.

Tensor words

noncomputable def CommutingRepetition.tensorWord {N₁ : StdTracialAlgebra} {R : ℕ} (D : TensorPowerData N₁ R) (g : Fin R → N₁.A) : D.Nhat.A

The ordered product of one embedded element per tensor factor.

Equations

• CommutingRepetition.tensorWord D g = (List.ofFn fun (ℓ : Fin R) => (D.emb ℓ) (g ℓ)).prod

theorem CommutingRepetition.tensorWord_mul {N₁ : StdTracialAlgebra} {R : ℕ} (D : TensorPowerData N₁ R) (g g' : Fin R → N₁.A) : tensorWord D g * tensorWord D g' = tensorWord D fun (ℓ : Fin R) => g ℓ * g' ℓ

theorem CommutingRepetition.tensorWord_star {N₁ : StdTracialAlgebra} {R : ℕ} (D : TensorPowerData N₁ R) (g : Fin R → N₁.A) : star (tensorWord D g) = tensorWord D fun (ℓ : Fin R) => star (g ℓ)

theorem CommutingRepetition.tensorWord_one {N₁ : StdTracialAlgebra} {R : ℕ} (D : TensorPowerData N₁ R) : (tensorWord D fun (x : Fin R) => 1) = 1

theorem CommutingRepetition.tensorWord_single {N₁ : StdTracialAlgebra} {R : ℕ} (D : TensorPowerData N₁ R) (j : Fin R) (x : N₁.A) : (D.emb j) x = tensorWord D fun (ℓ : Fin R) => if ℓ = j then x else 1

theorem CommutingRepetition.tensorWord_trace {N₁ : StdTracialAlgebra} {R : ℕ} (D : TensorPowerData N₁ R) (g : Fin R → N₁.A) : D.Nhat.τ (tensorWord D g) = ∏ ℓ : Fin R, N₁.τ (g ℓ)

theorem CommutingRepetition.noncommProd_eq_tensorWord {N₁ : StdTracialAlgebra} {R : ℕ} (D : TensorPowerData N₁ R) (s : Finset (Fin R)) (f : Fin R → N₁.A) (comm : (↑s).Pairwise (Function.onFun Commute fun (ℓ : Fin R) => (D.emb ℓ) (f ℓ))) : s.noncommProd (fun (ℓ : Fin R) => (D.emb ℓ) (f ℓ)) comm = tensorWord D fun (ℓ : Fin R) => if ℓ ∈ s then f ℓ else 1

Pairing algebra

theorem CommutingRepetition.StdTracialAlgebra.pairing_add_left (M : StdTracialAlgebra) (σ u₁ u₂ w : M.A) : M.τ (star σ * ((u₁ + u₂) * σ * w)) = M.τ (star σ * (u₁ * σ * w)) + M.τ (star σ * (u₂ * σ * w))

theorem CommutingRepetition.StdTracialAlgebra.pairing_add_right (M : StdTracialAlgebra) (σ u w₁ w₂ : M.A) : M.τ (star σ * (u * σ * (w₁ + w₂))) = M.τ (star σ * (u * σ * w₁)) + M.τ (star σ * (u * σ * w₂))

theorem CommutingRepetition.StdTracialAlgebra.pairing_sum_left (M : StdTracialAlgebra) {ι : Type u_1} (s : Finset ι) (σ : M.A) (u : ι → M.A) (w : M.A) : M.τ (star σ * ((∑ i ∈ s, u i) * σ * w)) = ∑ i ∈ s, M.τ (star σ * (u i * σ * w))

theorem CommutingRepetition.StdTracialAlgebra.pairing_sum_right (M : StdTracialAlgebra) {ι : Type u_1} (s : Finset ι) (σ u : M.A) (w : ι → M.A) : M.τ (star σ * (u * σ * ∑ i ∈ s, w i)) = ∑ i ∈ s, M.τ (star σ * (u * σ * w i))

theorem CommutingRepetition.StdTracialAlgebra.pairing_cyc (M : StdTracialAlgebra) (ω V Wv At Bt : M.A) : M.τ (star ω * (star V * At * V * ω * (Wv * Bt * star Wv))) = M.τ (star (V * (ω * Wv)) * (At * (V * (ω * Wv)) * Bt))

Tracial cyclicity moves the common-branch pairing onto the branch vector ζ = V ω Wv.

theorem CommutingRepetition.StdTracialAlgebra.fail_both_trace (M : StdTracialAlgebra) (ω P Q : M.A) {a b c : ℂ} (h1 : M.τ (star ω * ω) = 1) (hP : M.τ (star ω * (P * ω)) = a) (hQ : M.τ (star ω * (ω * Q)) = b) (hPQ : M.τ (star ω * (P * ω * Q)) = c) : M.τ (star ω * ((1 - P) * ω * (1 - Q))) = 1 - a - b + c

The joint-failure pairing from the one-trial success traces (appendix eq one-trial-branch-norms, first line).

theorem CommutingRepetition.one_sub_mul_one_sub_of_idem {A : Type u_1} [Ring A] {p : A} (hp : p * p = p) : (1 - p) * (1 - p) = 1 - p

1 - p is idempotent when p is.

theorem CommutingRepetition.prod_ite_lt_eq_pow_mul {R : ℕ} (j : Fin R) (x T : ℂ) : (∏ ℓ : Fin R, if ℓ < j then x else if ℓ = j then T else 1) = x ^ ↑j * T

The x^j bookkeeping: a product over Fin R that is x before j, T at j and 1 after j.

theorem CommutingRepetition.diag_term_trace {M₁ : StdTracialAlgebra} {R : ℕ} (D : TensorPowerData M₁ R) (ω P Q V Wv At Bt : M₁.A) (hPsa : star P = P) (hPid : P * P = P) (hQsa : star Q = Q) (hQid : Q * Q = Q) {x T : ℂ} (h1 : M₁.τ (star ω * ω) = 1) (hx : M₁.τ (star ω * ((1 - P) * ω * (1 - Q))) = x) (hT : M₁.τ (star ω * (star V * At * V * ω * (Wv * Bt * star Wv))) = T) (j : Fin R) (commP : (↑{ℓ : Fin R | ℓ < j}).Pairwise (Function.onFun Commute fun (ℓ : Fin R) => (D.emb ℓ) (1 - P))) (commQ : (↑{ℓ : Fin R | ℓ < j}).Pairwise (Function.onFun Commute fun (ℓ : Fin R) => (D.emb ℓ) (1 - Q))) : D.Nhat.τ (star (tensorWord D fun (x : Fin R) => ω) * ((star ((D.emb j) V * {ℓ : Fin R | ℓ < j}.noncommProd (fun (ℓ : Fin R) => (D.emb ℓ) (1 - P)) commP) * (D.emb j) At * ((D.emb j) V * {ℓ : Fin R | ℓ < j}.noncommProd (fun (ℓ : Fin R) => (D.emb ℓ) (1 - P)) commP) * tensorWord D fun (x : Fin R) => ω) * ({ℓ : Fin R | ℓ < j}.noncommProd (fun (ℓ : Fin R) => (D.emb ℓ) (1 - Q)) commQ * (D.emb j) Wv * (D.emb j) Bt * star ({ℓ : Fin R | ℓ < j}.noncommProd (fun (ℓ : Fin R) => (D.emb ℓ) (1 - Q)) commQ * (D.emb j) Wv)))) = x ^ ↑j * T

Diagonal branch trace: for a common first-success index j, the pairing of the two compiled Kraus branches on the product state factorizes over the tensor factors — joint failure (x) before j, the erased common branch (T) at j, the untouched unit resource after j (appendix eq common-index-vector).

noncomputable def CommutingRepetition.tildeA {N : StdTracialAlgebra} {S : Type v} {m : ℕ} {Aa : Type u_1} (E : S → Aa → N.A) (a₀ : Aa) (s : S) (a : Aa) : Matrix (Fin (m + 1)) (Fin (m + 1)) N.A

Alice's extended target effect Ã_s^a = e_{★★} ⊗ A_s^a + 1_{a=a₀} (1 − e_{★★} ⊗ 1) (06_otqcs.tex, eq Atilde).

Equations

• CommutingRepetition.tildeA E a₀ s a = Matrix.single (Fin.last m) (Fin.last m) (E s a) + if a = a₀ then 1 - Matrix.single (Fin.last m) (Fin.last m) 1 else 0

noncomputable def CommutingRepetition.tildeB {N : StdTracialAlgebra} {T : Type w} {m : ℕ} {Bb : Type u_2} (G : T → Bb → N.A) (b₀ : Bb) (t' : T) (b : Bb) : Matrix (Fin (m + 1)) (Fin (m + 1)) N.A

Bob's extended target effect B̃_t^b = e_{★★} ⊗ B_t^b + 1_{b=b₀} (1 − e_{★★} ⊗ 1) (06_otqcs.tex, eq Btilde).

Equations

• CommutingRepetition.tildeB G b₀ t' b = Matrix.single (Fin.last m) (Fin.last m) (G t' b) + if b = b₀ then 1 - Matrix.single (Fin.last m) (Fin.last m) 1 else 0

noncomputable def CommutingRepetition.krausA {N : StdTracialAlgebra} {S : Type v} {T : Type w} {x : S → N.H} {y : T → N.H} (F : ModulusFamily N x y) {m : ℕ} (B : Fin m → Set ℝ) {R : ℕ} (D : TensorPowerData (N.amplify (m + 1)) R) (s : S) (j : Fin R) : D.Nhat.A

Alice's first-success Kraus element K^A_{s,j} = V_{s,j} ∏_{ℓ<j} (1 − P_{s,ℓ}) (06_otqcs.tex, eq first-success-Kraus).

Equations

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

noncomputable def CommutingRepetition.krausB {N : StdTracialAlgebra} {S : Type v} {T : Type w} {x : S → N.H} {y : T → N.H} (F : ModulusFamily N x y) {m : ℕ} (B : Fin m → Set ℝ) {R : ℕ} (D : TensorPowerData (N.amplify (m + 1)) R) (t' : T) (j : Fin R) : D.Nhat.A

Bob's first-success Kraus element K^B_{t,j} = (∏_{ℓ<j} (1 − Q_{t,ℓ})) W_{t,j} v̄_{t,j} (06_otqcs.tex, eq first-success-Kraus).

Equations

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

noncomputable def CommutingRepetition.allFailA {N : StdTracialAlgebra} {S : Type v} {T : Type w} {x : S → N.H} {y : T → N.H} (F : ModulusFamily N x y) {m : ℕ} (B : Fin m → Set ℝ) {R : ℕ} (D : TensorPowerData (N.amplify (m + 1)) R) (s : S) : D.Nhat.A

Alice's all-fail projection F_s^A = ∏_{j} (1 − P_{s,j}) (06_otqcs.tex, eq all-fail).

Equations

• CommutingRepetition.allFailA F B D s = Finset.univ.noncommProd (fun (ℓ : Fin R) => (D.emb ℓ) (1 - CommutingRepetition.trialPA N F B s)) ⋯

noncomputable def CommutingRepetition.allFailB {N : StdTracialAlgebra} {S : Type v} {T : Type w} {x : S → N.H} {y : T → N.H} (F : ModulusFamily N x y) {m : ℕ} (B : Fin m → Set ℝ) {R : ℕ} (D : TensorPowerData (N.amplify (m + 1)) R) (t' : T) : D.Nhat.A

Bob's all-fail projection F_t^B = ∏_{j} (1 − Q_{t,j}) (06_otqcs.tex, eq all-fail).

Equations

• CommutingRepetition.allFailB F B D t' = Finset.univ.noncommProd (fun (ℓ : Fin R) => (D.emb ℓ) (1 - CommutingRepetition.trialQB N F B t')) ⋯

noncomputable def CommutingRepetition.hatA {N : StdTracialAlgebra} {S : Type v} {T : Type w} {x : S → N.H} {y : T → N.H} (F : ModulusFamily N x y) {m : ℕ} (B : Fin m → Set ℝ) {R : ℕ} (D : TensorPowerData (N.amplify (m + 1)) R) {Aa : Type u_1} (E : S → Aa → N.A) (a₀ : Aa) (s : S) (a : Aa) : D.Nhat.A

Alice's compiled effect Â_s^a = ∑_j (K^A_{s,j})* Ã_{s,j}^a K^A_{s,j} + 1_{a=a₀} F_s^A (06_otqcs.tex, eq Ahat).

Equations

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

noncomputable def CommutingRepetition.hatB {N : StdTracialAlgebra} {S : Type v} {T : Type w} {x : S → N.H} {y : T → N.H} (F : ModulusFamily N x y) {m : ℕ} (B : Fin m → Set ℝ) {R : ℕ} (D : TensorPowerData (N.amplify (m + 1)) R) {Bb : Type u_2} (G : T → Bb → N.A) (b₀ : Bb) (t' : T) (b : Bb) : D.Nhat.A

Bob's compiled effect B̂_t^b = ∑_j K^B_{t,j} B̃_{t,j}^b (K^B_{t,j})* + 1_{b=b₀} F_t^B (06_otqcs.tex, eq Bhat) — note the mirrored pullback orientation (appendix eq right-pullback).

Equations

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

theorem CommutingRepetition.trialPA_sa {N : StdTracialAlgebra} {S : Type v} {T : Type w} {x : S → N.H} {y : T → N.H} (F : ModulusFamily N x y) {m : ℕ} (B : Fin m → Set ℝ) (s : S) : star (trialPA N F B s) = trialPA N F B s

P_s is self-adjoint (its band spectral projections are self-adjoint).

theorem CommutingRepetition.trialPA_idem {N : StdTracialAlgebra} {S : Type v} {T : Type w} {x : S → N.H} {y : T → N.H} (F : ModulusFamily N x y) {m : ℕ} (B : Fin m → Set ℝ) (t : Fin m → ℝ) (hB : IsBandFamily B t) (s : S) : trialPA N F B s * trialPA N F B s = trialPA N F B s

P_s is idempotent (the band spectral projections are, given measurability).

theorem CommutingRepetition.trialQB_sa {N : StdTracialAlgebra} {S : Type v} {T : Type w} {x : S → N.H} {y : T → N.H} (F : ModulusFamily N x y) {m : ℕ} (B : Fin m → Set ℝ) (t' : T) : star (trialQB N F B t') = trialQB N F B t'

Q_t is self-adjoint.

theorem CommutingRepetition.trialQB_idem {N : StdTracialAlgebra} {S : Type v} {T : Type w} {x : S → N.H} {y : T → N.H} (F : ModulusFamily N x y) {m : ℕ} (B : Fin m → Set ℝ) (t : Fin m → ℝ) (hB : IsBandFamily B t) (t' : T) : trialQB N F B t' * trialQB N F B t' = trialQB N F B t'

Q_t is idempotent.

theorem CommutingRepetition.emb_one_sub_proj {N₁ : StdTracialAlgebra} {R : ℕ} (D : TensorPowerData N₁ R) (i : Fin R) (p : N₁.A) (hsa : star p = p) (hidem : p * p = p) : star ((D.emb i) (1 - p)) = (D.emb i) (1 - p) ∧ (D.emb i) (1 - p) * (D.emb i) (1 - p) = (D.emb i) (1 - p)

For a ∗-embedding emb i and a self-adjoint idempotent p, the image emb i (1 − p) is a self-adjoint idempotent (the "bin ℓ failed" projection).

theorem CommutingRepetition.tildeA_mul_single {N : StdTracialAlgebra} {S : Type v} {m : ℕ} {Aa : Type u_1} (E : S → Aa → N.A) (a₀ : Aa) (s : S) (a : Aa) (z : N.A) : tildeA E a₀ s a * Matrix.single (Fin.last m) (Fin.last m) z = Matrix.single (Fin.last m) (Fin.last m) (E s a * z)

Ã_s^a · e_{★★}⊗y = e_{★★} ⊗ (A_s^a y): the fallback part of Ã kills the corner.

theorem CommutingRepetition.single_mul_tildeB {N : StdTracialAlgebra} {T : Type w} {m : ℕ} {Bb : Type u_2} (G : T → Bb → N.A) (b₀ : Bb) (t' : T) (b : Bb) (z : N.A) : Matrix.single (Fin.last m) (Fin.last m) z * tildeB G b₀ t' b = Matrix.single (Fin.last m) (Fin.last m) (z * G t' b)

e_{★★}⊗y · B̃_t^b = e_{★★} ⊗ (y B_t^b).

theorem CommutingRepetition.tildeA_isPosElem {N : StdTracialAlgebra} {S : Type v} {m : ℕ} {Aa : Type u_1} (E : S → Aa → N.A) (a₀ : Aa) (s : S) (hE : ∀ (s : S) (a : Aa), IsPosElem (E s a)) (a : Aa) : IsPosElem (tildeA E a₀ s a)

The extended target effects are algebraically positive.

theorem CommutingRepetition.tildeB_isPosElem {N : StdTracialAlgebra} {T : Type w} {m : ℕ} {Bb : Type u_2} (G : T → Bb → N.A) (b₀ : Bb) (t' : T) (hG : ∀ (t' : T) (b : Bb), IsPosElem (G t' b)) (b : Bb) : IsPosElem (tildeB G b₀ t' b)

theorem CommutingRepetition.allFailA_isPosElem {N : StdTracialAlgebra} {S : Type v} {T : Type w} {x : S → N.H} {y : T → N.H} (F : ModulusFamily N x y) {m : ℕ} (B : Fin m → Set ℝ) (t : Fin m → ℝ) {R : ℕ} (D : TensorPowerData (N.amplify (m + 1)) R) (hB : IsBandFamily B t) (s : S) : IsPosElem (allFailA F B D s)

The all-fail projections are algebraically positive.

theorem CommutingRepetition.allFailB_isPosElem {N : StdTracialAlgebra} {S : Type v} {T : Type w} {x : S → N.H} {y : T → N.H} (F : ModulusFamily N x y) {m : ℕ} (B : Fin m → Set ℝ) (t : Fin m → ℝ) {R : ℕ} (D : TensorPowerData (N.amplify (m + 1)) R) (hB : IsBandFamily B t) (t' : T) : IsPosElem (allFailB F B D t')

theorem CommutingRepetition.corner_pairing {N : StdTracialAlgebra} {S : Type v} {T : Type w} {x : S → N.H} {y : T → N.H} (F : ModulusFamily N x y) {m : ℕ} (B : Fin m → Set ℝ) (t : Fin m → ℝ) {Aa : Type u_1} {Bb : Type u_2} (E : S → Aa → N.A) (G : T → Bb → N.A) (s : S) (t' : T) (a₀ a : Aa) (b₀ b : Bb) : (N.amplify (m + 1)).τ (star (trialVA N F B s * (trialUnitMat N m t * (trialWB N F B t' * trialVbar N F t'))) * (tildeA E a₀ s a * (trialVA N F B s * (trialUnitMat N m t * (trialWB N F B t' * trialVbar N F t'))) * tildeB G b₀ t' b)) = (↑(bandZ t))⁻¹ * N.τ (star (selWord (F.dataA s) (F.dataB t') B t) * (E s a * selWord (F.dataA s) (F.dataB t') B t * G t' b))

The ★★-corner pairing: on the erased common branch ζ = V ω₀ (W v̄) = e_{★★} ⊗ √((m+1)/Z) w_{st}, the extended effects act through the corner only: τ₁(ζ* Ã ζ B̃) = Z⁻¹ τ(w* A w B) (appendix eqs left-pullback and right-pullback with the normalized corner identification).

theorem CommutingRepetition.hatA_isPosElem {N : StdTracialAlgebra} {S : Type v} {T : Type w} {x : S → N.H} {y : T → N.H} (F : ModulusFamily N x y) {m : ℕ} (B : Fin m → Set ℝ) (t : Fin m → ℝ) {R : ℕ} (D : TensorPowerData (N.amplify (m + 1)) R) {Aa : Type u_1} (E : S → Aa → N.A) [Fintype Aa] (a₀ : Aa) (s : S) (hB : IsBandFamily B t) (hE : ∀ (s : S) (a : Aa), IsPosElem (E s a)) (a : Aa) : IsPosElem (hatA F B D E a₀ s a)

The compiled Alice effects are algebraically positive (06_otqcs.tex, "All effects in eqs Ahat–Bhat are positive").

theorem CommutingRepetition.hatB_isPosElem {N : StdTracialAlgebra} {S : Type v} {T : Type w} {x : S → N.H} {y : T → N.H} (F : ModulusFamily N x y) {m : ℕ} (B : Fin m → Set ℝ) (t : Fin m → ℝ) {R : ℕ} (D : TensorPowerData (N.amplify (m + 1)) R) {Bb : Type u_2} (G : T → Bb → N.A) [Fintype Bb] (b₀ : Bb) (t' : T) (hB : IsBandFamily B t) (hG : ∀ (t' : T) (b : Bb), IsPosElem (G t' b)) (b : Bb) : IsPosElem (hatB F B D G b₀ t' b)

The compiled Bob effects are algebraically positive.

theorem CommutingRepetition.hatA_sum {N : StdTracialAlgebra} {S : Type v} {T : Type w} {x : S → N.H} {y : T → N.H} (F : ModulusFamily N x y) {m : ℕ} (B : Fin m → Set ℝ) (t : Fin m → ℝ) {R : ℕ} (D : TensorPowerData (N.amplify (m + 1)) R) {Aa : Type u_1} (E : S → Aa → N.A) [Fintype Aa] (a₀ : Aa) (s : S) (hB : IsBandFamily B t) (hE1 : ∑ a : Aa, E s a = 1) : ∑ a : Aa, hatA F B D E a₀ s a = 1

Alice's compiled family is a full POVM: the first-success telescope (06_otqcs.tex, eq first-success-telescope, via V* V = P).

theorem CommutingRepetition.hatB_sum {N : StdTracialAlgebra} {S : Type v} {T : Type w} {x : S → N.H} {y : T → N.H} (F : ModulusFamily N x y) {m : ℕ} (B : Fin m → Set ℝ) (t : Fin m → ℝ) {R : ℕ} (D : TensorPowerData (N.amplify (m + 1)) R) {Bb : Type u_2} (G : T → Bb → N.A) [Fintype Bb] (b₀ : Bb) (t' : T) (hB : IsBandFamily B t) (hG1 : ∑ b : Bb, G t' b = 1) : ∑ b : Bb, hatB F B D G b₀ t' b = 1

Bob's compiled family is a full POVM (mirror telescope via W W* = Q).

noncomputable def CommutingRepetition.commonMass (a b c Z : ℝ) (R : ℕ) : ℝ

Total mass of the common-index branches with R retained trials: ∑_{j=1}^{R} (1 − (a+b−c)/Z)^{j−1} (c/Z) (06_otqcs.tex, eq common-index-mass, summed).

Equations

• CommutingRepetition.commonMass a b c Z R = ∑ j ∈ Finset.range R, (1 - (a + b - c) / Z) ^ j * (c / Z)

theorem CommutingRepetition.finite_bad_bound (a b c Z : ℝ) (R : ℕ) (hZ : 0 < Z) (ha : 1 / 2 ≤ a) (hb : 1 / 2 ≤ b) (hc : 0 ≤ c) (hca : c ≤ a) (hcb : c ≤ b) (hle : a + b - c ≤ Z) : 1 - commonMass a b c Z R ≤ 2 * (a + b - 2 * c) + 2 * Real.exp (-↑R / (2 * Z))

Finite bad-event bound (node 1.3.6; 06_otqcs.tex, eq finite-bad): outside the common-index branches — mismatched indices or exhaustion — the total mass is at most 2Γ + 2 e^{−R/(2Z)} when a, b ≥ 1/2 and c ≤ min{a,b}.

theorem CommutingRepetition.compile_decomposition {N : StdTracialAlgebra} {S T Aa Bb : Type} [Fintype Aa] [Fintype Bb] {x : S → N.H} {y : T → N.H} (F : ModulusFamily N x y) {m : ℕ} (B : Fin m → Set ℝ) (t : Fin m → ℝ) {R : ℕ} (D : TensorPowerData (N.amplify (m + 1)) R) (E : S → Aa → N.A) (G : T → Bb → N.A) (a₀ : Aa) (b₀ : Bb) (hB : IsBandFamily B t) (hZ : 0 < bandZ t) (hE_pos : ∀ (s : S) (a : Aa), IsPosElem (E s a)) (hG_pos : ∀ (t' : T) (b : Bb), IsPosElem (G t' b)) (hE_sum : ∀ (s : S), ∑ a : Aa, E s a = 1) (hG_sum : ∀ (t' : T), ∑ b : Bb, G t' b = 1) (s : S) (t' : T) : ∃ (r : Aa → Bb → ℝ), (∀ (a : Aa) (b : Bb), 0 ≤ r a b) ∧ ∑ a : Aa, ∑ b : Bb, r a b = 1 - commonMass (bandMassA F B t s) (bandMassB F B t t') (bandCross F B t s t') (bandZ t) R ∧ ∀ (a : Aa) (b : Bb), tracialPairLaw D.Nhat (fun (x : S) (x_1 : T) => tensorState D (trialUnitMat N m t)) (fun (s : S) (a : Aa) => hatA F B D E a₀ s a) (fun (t' : T) (b : Bb) => hatB F B D G b₀ t' b) s t' a b = commonMass (bandMassA F B t s) (bandMassB F B t t') (bandCross F B t s t') (bandZ t) R * tracialPairLaw N (fun (s : S) (t'' : T) => selState (F.dataA s) (F.dataB t'') (F.joint s t'') B t) E G s t' a b + r a b

Branch decomposition of the compiled answer law (node 1.3.8; 06_otqcs.tex, eqs Ahat + Bhat realizing eq common-index-mass; appendix_otqcs.tex, eqs one-trial-branch-norms, common-index-vector, left-pullback, right-pullback): on each pair (s,t), the compiled resource's answer law equals commonMass times the answer law of the selected state z_{st} under the original POVMs, plus a nonnegative remainder — the mismatched-index, one-sided-success, exhaustion, and fallback-corner branches — of total mass 1 − commonMass. Stated at universe 0 with the signed tracialPairLaw.