structure CommutingRepetition.IsBandFamily {m : ℕ} (B : Fin m → Set ℝ) (t : Fin m → ℝ) : Prop

A band family for the trial construction: m pairwise disjoint measurable subsets of (0, ∞) with positive band values. At consumption these are the retained shifted bins I_j^{θ₀} ∩ [L, H] and their upper endpoints t_j (06_otqcs.tex, eq N1-Z "the finite retained bin set").

• meas (j : Fin m) : MeasurableSet (B j)
• disj : Pairwise (Function.onFun Disjoint B)
• pos (j : Fin m) : B j ⊆ Set.Ioi 0
• tpos (j : Fin m) : 0 < t j

noncomputable def CommutingRepetition.bandZ {m : ℕ} (t : Fin m → ℝ) : ℝ

Z = ∑_{j ∈ J} t_j² (06_otqcs.tex, eq N1-Z).

Equations

• CommutingRepetition.bandZ t = ∑ j : Fin m, t j ^ 2

noncomputable def CommutingRepetition.bandMassA {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 → ℝ) (s : S) : ℝ

Alice's band mass a_s = ∑_j t_j² τ(p_j(h_s)) in finite band form (06_otqcs.tex, eq abcGamma via eq one-trial-probabilities).

Equations

• CommutingRepetition.bandMassA F B t s = ∑ j : Fin m, t j ^ 2 * ((F.dataA s).μ (B j)).toReal

noncomputable def CommutingRepetition.bandMassB {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 → ℝ) (t' : T) : ℝ

Bob's band mass b_t = ∑_j t_j² τ(p_j(k_t)).

Equations

• CommutingRepetition.bandMassB F B t t' = ∑ j : Fin m, t j ^ 2 * ((F.dataB t').μ (B j)).toReal

noncomputable def CommutingRepetition.bandCross {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 → ℝ) (s : S) (t' : T) : ℝ

The joint band mass c_{st} = ∑_j t_j² τ(p_j(h_s) p_j(k_t)), read through the joint spectral coupling (06_otqcs.tex, eqs abcGamma + joint-measure).

Equations

• CommutingRepetition.bandCross F B t s t' = ∑ j : Fin m, t j ^ 2 * ((F.joint s t').ν (B j ×ˢ B j)).toReal

theorem CommutingRepetition.wnorm_core {N : StdTracialAlgebra} {x y : N.H} (dA : SpectralData N x) (dB : SpectralData N y) (Jd : JointSpectralData dA dB) {m : ℕ} (B : Fin m → Set ℝ) (t : Fin m → ℝ) (hB : IsBandFamily B t) : N.τ (star (∑ j : Fin m, ↑(t j) • (dA.proj (B j) * dB.proj (B j) * dB.v)) * ∑ j : Fin m, ↑(t j) • (dA.proj (B j) * dB.proj (B j) * dB.v)) = ↑(∑ j : Fin m, t j ^ 2 * (Jd.ν (B j ×ˢ B j)).toReal)

Core w-norm computation (06_otqcs.tex, eq w-norm): τ(w* w) = ∑_j t_j² τ(p_j(h) p_j(k)) = c, where w = ∑_j t_j p_j(h) p_j(k) v.

noncomputable def CommutingRepetition.trialUnitMat (N : StdTracialAlgebra) (m : ℕ) (t : Fin m → ℝ) : Matrix (Fin (m + 1)) (Fin (m + 1)) N.A

The one-trial resource matrix: √((m+1)/Z) ∑_{j} t_j e_jj ⊗ 1, zero at the distinguished diagonal entry ★★ (06_otqcs.tex, eq omega0, as an element of M_{m+1}(N) before the GNS embedding).

Equations

• CommutingRepetition.trialUnitMat N m t = Matrix.diagonal fun (i : Fin (m + 1)) => Fin.lastCases 0 (fun (j : Fin m) => ↑(√((↑m + 1) / CommutingRepetition.bandZ t) * t j) • 1) i

noncomputable def CommutingRepetition.trialState (N : StdTracialAlgebra) (m : ℕ) (t : Fin m → ℝ) : (N.amplify (m + 1)).H

The one-trial resource vector ω₀ ∈ L²(M_{m+1}(N)) (06_otqcs.tex, eq omega0).

Equations

• CommutingRepetition.trialState N m t = (N.amplify (m + 1)).ι (CommutingRepetition.trialUnitMat N m t)

noncomputable def CommutingRepetition.trialPA (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) : Matrix (Fin (m + 1)) (Fin (m + 1)) N.A

Alice's one-trial success projection P_s = ∑_j e_jj ⊗ p_j(h_s) (06_otqcs.tex, eq PQ).

Equations

• CommutingRepetition.trialPA N F B s = Matrix.diagonal fun (i : Fin (m + 1)) => Fin.lastCases 0 (fun (j : Fin m) => (F.dataA s).proj (B j)) i

noncomputable def CommutingRepetition.trialQB (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) : Matrix (Fin (m + 1)) (Fin (m + 1)) N.A

Bob's one-trial success projection Q_t = ∑_j e_jj ⊗ p_j(k_t) (06_otqcs.tex, eq PQ).

Equations

• CommutingRepetition.trialQB N F B t' = Matrix.diagonal fun (i : Fin (m + 1)) => Fin.lastCases 0 (fun (j : Fin m) => (F.dataB t').proj (B j)) i

noncomputable def CommutingRepetition.trialVA (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) : Matrix (Fin (m + 1)) (Fin (m + 1)) N.A

Alice's bin-erasing partial isometry V_s = ∑_j e_{★j} ⊗ p_j(h_s) (06_otqcs.tex, eq erasers).

Equations

• CommutingRepetition.trialVA N F B s = Matrix.of fun (i i' : Fin (m + 1)) => if i = Fin.last m then Fin.lastCases 0 (fun (j : Fin m) => (F.dataA s).proj (B j)) i' else 0

noncomputable def CommutingRepetition.trialWB (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) : Matrix (Fin (m + 1)) (Fin (m + 1)) N.A

Bob's bin-erasing partial isometry W_t = ∑_j e_{j★} ⊗ p_j(k_t) (06_otqcs.tex, eq erasers).

Equations

• CommutingRepetition.trialWB N F B t' = Matrix.of fun (i i' : Fin (m + 1)) => if i' = Fin.last m then Fin.lastCases 0 (fun (j : Fin m) => (F.dataB t').proj (B j)) i else 0

noncomputable def CommutingRepetition.trialVbar (N : StdTracialAlgebra) {S : Type v} {T : Type w} {x : S → N.H} {y : T → N.H} (F : ModulusFamily N x y) {m : ℕ} (t' : T) : Matrix (Fin (m + 1)) (Fin (m + 1)) N.A

The polar corrector v̄_t = e_{★★} ⊗ v_t (06_otqcs.tex, above eq polar-initial).

Equations

• CommutingRepetition.trialVbar N F t' = Matrix.single (Fin.last m) (Fin.last m) (F.dataB t').v

noncomputable def CommutingRepetition.trialZeta (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 → ℝ) (s : S) (t' : T) : (N.amplify (m + 1)).H

The erased, polar-corrected common branch ζ_{st} = V_s ω₀ W_t v̄_t — Alice's eraser on the left, Bob's on the right (06_otqcs.tex, eq common-branch).

Equations

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

theorem CommutingRepetition.trialState_norm (N : StdTracialAlgebra) (m : ℕ) (t : Fin m → ℝ) (hZ : 0 < bandZ t) : ‖trialState N m t‖ = 1

The one-trial resource is a unit vector (06_otqcs.tex, below eq omega0).

theorem CommutingRepetition.trial_success_A (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) : inner ℂ (trialState N m t) (((N.amplify (m + 1)).L (trialPA N F B s)) (trialState N m t)) = ↑(bandMassA F B t s / bandZ t)

Alice's one-trial success probability is a_s / Z (06_otqcs.tex, eq one-trial-probabilities, first entry).

theorem CommutingRepetition.trial_success_B (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) : inner ℂ (trialState N m t) (((N.amplify (m + 1)).Rop (trialQB N F B t')) (trialState N m t)) = ↑(bandMassB F B t t' / bandZ t)

Bob's one-trial success probability is b_t / Z (06_otqcs.tex, eq one-trial-probabilities, second entry).

theorem CommutingRepetition.trial_success_joint (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) (t' : T) : inner ℂ (trialState N m t) (((N.amplify (m + 1)).L (trialPA N F B s)) (((N.amplify (m + 1)).Rop (trialQB N F B t')) (trialState N m t))) = ↑(bandCross F B t s t' / bandZ t)

The joint one-trial success probability is c_{st} / Z (06_otqcs.tex, eq one-trial-probabilities, third entry).

theorem CommutingRepetition.trialVA_star_mul (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) : star (trialVA N F B s) * trialVA N F B s = trialPA N F B s

V_s* V_s = P_s (06_otqcs.tex, below eq erasers).

theorem CommutingRepetition.trialWB_mul_star (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) : trialWB N F B t' * star (trialWB N F B t') = trialQB N F B t'

W_t W_t* = Q_t (06_otqcs.tex, below eq erasers).

theorem CommutingRepetition.trialWB_vbar_initial (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) : trialWB N F B t' * trialVbar N F t' * star (trialVbar N F t') * star (trialWB N F B t') = trialQB N F B t'

W_t v̄_t v̄_t* W_t* = Q_t: every retained spectral projection of k_t lies below the left support v_t v_t* (06_otqcs.tex, eq polar-initial).

theorem CommutingRepetition.trialVA_mul_state_mul_WVbar (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 → ℝ) (s : S) (t' : T) : trialVA N F B s * (trialUnitMat N m t * (trialWB N F B t' * trialVbar N F t')) = Matrix.single (Fin.last m) (Fin.last m) (↑√((↑m + 1) / bandZ t) • ∑ j : Fin m, ↑(t j) • ((F.dataA s).proj (B j) * (F.dataB t').proj (B j) * (F.dataB t').v))

The erased, polar-corrected common branch as a matrix (eq common-branch before the GNS map): V_s ω₀ (W_t v̄_t) = e_{★★} ⊗ √((m+1)/Z) w_{st}.

theorem CommutingRepetition.trialZeta_eq (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) (t' : T) : trialZeta N F B t s t' = (N.amplify (m + 1)).ι (Matrix.single (Fin.last m) (Fin.last m) (↑√((↑m + 1) / bandZ t) • ∑ j : Fin m, ↑(t j) • ((F.dataA s).proj (B j) * (F.dataB t').proj (B j) * (F.dataB t').v)))

The common branch in closed form: ζ_{st} = √((m+1)/Z) · ι(e_{★★} ⊗ ∑_j t_j p_j(h_s) p_j(k_t) v_t) (06_otqcs.tex, eq common-branch, second line).

theorem CommutingRepetition.trialZeta_normSq (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) (t' : T) : ‖trialZeta N F B t s t'‖ ^ 2 = bandCross F B t s t' / bandZ t

‖ζ_{st}‖² = c_{st} / Z (06_otqcs.tex, below eq common-branch).

One-trial traces and the corner trace (proof-side helpers for OTQCS/Compile)

theorem CommutingRepetition.trialUnitMat_trace_one (N : StdTracialAlgebra) {m : ℕ} (t : Fin m → ℝ) (hZ : 0 < bandZ t) : (N.amplify (m + 1)).τ (star (trialUnitMat N m t) * trialUnitMat N m t) = 1

τ₁(ω₀* ω₀) = 1 (the unit-norm resource, in trace form).

theorem CommutingRepetition.trialUnitMat_trace_PA (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) : (N.amplify (m + 1)).τ (star (trialUnitMat N m t) * (trialPA N F B s * trialUnitMat N m t)) = ↑(bandMassA F B t s / bandZ t)

τ₁(ω₀* P_s ω₀) = a_s/Z (eq one-trial-probabilities, trace form).

theorem CommutingRepetition.trialUnitMat_trace_QB (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) : (N.amplify (m + 1)).τ (star (trialUnitMat N m t) * (trialUnitMat N m t * trialQB N F B t')) = ↑(bandMassB F B t t' / bandZ t)

τ₁(ω₀* ω₀ Q_t) = b_t/Z.

theorem CommutingRepetition.trialUnitMat_trace_joint (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) (t' : T) : (N.amplify (m + 1)).τ (star (trialUnitMat N m t) * (trialPA N F B s * trialUnitMat N m t * trialQB N F B t')) = ↑(bandCross F B t s t' / bandZ t)

τ₁(ω₀* P_s ω₀ Q_t) = c_{st}/Z.

theorem CommutingRepetition.ampτ_single (N : StdTracialAlgebra) {m : ℕ} (z : N.A) : (N.amplify (m + 1)).τ (Matrix.single (Fin.last m) (Fin.last m) z) = (↑m + 1)⁻¹ * N.τ z

The normalized matrix trace of a ★★-corner matrix.

First-success arithmetic (node 1.3.6)

Scalar consumed form of lem otqcs-first-success: the per-trial success probabilities are a/Z, b/Z, c/Z (eq one-trial-probabilities), and independence across trials reduces the first-success analysis to the three scalar facts below (exact geometric mass of the equal-index event, the mismatch bound, and the exhaustion tail).

theorem CommutingRepetition.equal_index_probability (a b c Z : ℝ) (hZ : 0 < Z) (hw : 0 < a + b - c) (hle : a + b - c ≤ Z) : ∑' (j : ℕ), (1 - (a + b - c) / Z) ^ j * (c / Z) = c / (a + b - c)

Exact equal-index probability (06_otqcs.tex, proof of lem otqcs-first-success, the geometric sum): with per-trial progress w = (a + b − c)/Z, the total mass of "both first successes at the same trial" is ∑_{j≥0} (1 − w)^j (c/Z) = c/(a + b − c).

theorem CommutingRepetition.first_success_mismatch (a b c : ℝ) (ha : 1 / 2 ≤ a) (hb : 1 / 2 ≤ b) (hc : 0 ≤ c) (hca : c ≤ a) (hcb : c ≤ b) : (a + b - 2 * c) / (a + b - c) ≤ 2 * (a + b - 2 * c)

First-success mismatch (node 1.3.6; 06_otqcs.tex, eq first-index-mismatch): when a, b ≥ 1/2 (eq ab-mass under the standing condition ρ + L² ≤ 1/4) and c ≤ min{a, b} (eq c-min), the index-mismatch probability (a + b − 2c)/(a + b − c) is at most 2 Γ = 2 (a + b − 2c).

theorem CommutingRepetition.all_fail_bound (a Z : ℝ) (R : ℕ) (hZ : 0 < Z) (ha : 1 / 2 ≤ a) (haZ : a ≤ Z) : (1 - a / Z) ^ R ≤ Real.exp (-↑R / (2 * Z))

Exhaustion tail (06_otqcs.tex, eq finite-bad): a player with per-trial success probability a/Z ≥ 1/(2Z) fails all R retained trials with probability at most e^{−R/(2Z)}.