noncomputable def CommutingRepetition.pairMassA {N : StdTracialAlgebra} {x : N.H} (dA : SpectralData N x) {m : ℕ} (B : Fin m → Set ℝ) (t : Fin m → ℝ) : ℝ

Alice's band mass a = ∑_j t_j² μ_A(B_j) for one pair of packages (the bandMassA of OTQCS/Trial.lean, without the family wrapper).

Equations

• CommutingRepetition.pairMassA dA B t = ∑ j : Fin m, t j ^ 2 * (dA.μ (B j)).toReal

noncomputable def CommutingRepetition.pairMassB {N : StdTracialAlgebra} {y : N.H} (dB : SpectralData N y) {m : ℕ} (B : Fin m → Set ℝ) (t : Fin m → ℝ) : ℝ

Bob's band mass b = ∑_j t_j² μ_B(B_j).

Equations

• CommutingRepetition.pairMassB dB B t = ∑ j : Fin m, t j ^ 2 * (dB.μ (B j)).toReal

noncomputable def CommutingRepetition.pairCross {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 → ℝ) : ℝ

The joint band mass c = ∑_j t_j² ν(B_j × B_j).

Equations

• CommutingRepetition.pairCross dA dB Jd B t = ∑ j : Fin m, t j ^ 2 * (Jd.ν (B j ×ˢ B j)).toReal

noncomputable def CommutingRepetition.selWord {N : StdTracialAlgebra} {x y : N.H} (dA : SpectralData N x) (dB : SpectralData N y) {m : ℕ} (B : Fin m → Set ℝ) (t : Fin m → ℝ) : N.A

The unnormalized selected word w_{st} = ∑_j t_j p_j(h_s) p_j(k_t) v_t — an algebra element (06_otqcs.tex, eq wst).

Equations

• CommutingRepetition.selWord dA dB B t = ∑ j : Fin m, ↑(t j) • (dA.proj (B j) * dB.proj (B j) * dB.v)

noncomputable def CommutingRepetition.selVec {N : StdTracialAlgebra} {x y : N.H} (dA : SpectralData N x) (dB : SpectralData N y) {m : ℕ} (B : Fin m → Set ℝ) (t : Fin m → ℝ) : N.H

The selected vector ι(w_{st}) ∈ L² (06_otqcs.tex, eq wst).

Equations

• CommutingRepetition.selVec dA dB B t = N.ι (CommutingRepetition.selWord dA dB B t)

noncomputable def CommutingRepetition.selState {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 → ℝ) : N.H

The selected state z_{st}: the normalized selected vector when the common mass is positive, the trace vector (a fixed unit default) when it vanishes (06_otqcs.tex, eqs zst + c-zero; the default is never passed to a physical branch — eq common-index-mass gives such branches zero mass).

Equations

• CommutingRepetition.selState dA dB Jd B t = if CommutingRepetition.pairCross dA dB Jd B t = 0 then N.ι 1 else ↑‖CommutingRepetition.selVec dA dB B t‖⁻¹ • CommutingRepetition.selVec dA dB B t

noncomputable def CommutingRepetition.selSharp {N : StdTracialAlgebra} {y : N.H} (dB : SpectralData N y) {m : ℕ} (B : Fin m → Set ℝ) (t : Fin m → ℝ) : N.A

The rounded modulus k_t^♯ = ∑_j t_j p_j(k_t) — a bounded algebra element (06_otqcs.tex, eq rounded-y).

Equations

• CommutingRepetition.selSharp dB B t = ∑ j : Fin m, ↑(t j) • dB.proj (B j)

noncomputable def CommutingRepetition.selYTilde {N : StdTracialAlgebra} {y : N.H} (dB : SpectralData N y) {m : ℕ} (B : Fin m → Set ℝ) (t : Fin m → ℝ) : N.H

The rounded polar vector ỹ_t = b_t^{−1/2} k_t^♯ v_t (06_otqcs.tex, eq rounded-y).

Equations

• CommutingRepetition.selYTilde dB B t = ↑(√(CommutingRepetition.pairMassB dB B t))⁻¹ • N.ι (CommutingRepetition.selSharp dB B t * dB.v)

noncomputable def CommutingRepetition.selCutVec {N : StdTracialAlgebra} {y : N.H} (dB : SpectralData N y) {m : ℕ} (B : Fin m → Set ℝ) : N.H

The cut modulus k_t^{cut} = k_t 1_{∪_j B_j}(k_t) as an L² vector (06_otqcs.tex, above eq rounding-tails, with the retained window realized by the band union).

Equations

• CommutingRepetition.selCutVec dB B = (N.Rop (dB.proj (⋃ (j : Fin m), B j))) dB.hvec

theorem CommutingRepetition.selVec_normSq {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) : ‖selVec dA dB B t‖ ^ 2 = pairCross dA dB Jd B t

‖w_{st}‖₂² = c_{st} (06_otqcs.tex, eq w-norm): orthogonality of the spectral projections, tracial cyclicity, and p_j(k_t) ≤ v_t v_t*.

theorem CommutingRepetition.selState_sub_yTilde {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) (ha : 1 / 2 ≤ pairMassA dA B t) (hb : 1 / 2 ≤ pairMassB dB B t) : ‖selState dA dB Jd B t - selYTilde dB B t‖ ^ 2 ≤ 4 * (pairMassA dA B t + pairMassB dB B t - 2 * pairCross dA dB Jd B t)

‖z_{st} − ỹ_t‖₂² ≤ 4 Γ_{st} (06_otqcs.tex, eqs z-rounded-y + c-zero): at positive common mass via 2 − 2√(c/b) ≤ 2(b−c)/b ≤ 4(b−c) ≤ 4Γ, and at zero common mass via Γ = a + b ≥ 1 against the crude bound ‖z − ỹ‖² ≤ 4; the constant 4 covers both branches.

theorem CommutingRepetition.selCutVec_sub {N : StdTracialAlgebra} {y : N.H} (dB : SpectralData N y) {m : ℕ} (B : Fin m → Set ℝ) (t : Fin m → ℝ) (hB : IsBandFamily B t) : ‖dB.hvec - selCutVec dB B‖ ^ 2 = ∫ (b : ℝ), b ^ 2 ∂dB.μ - ∫ (b : ℝ) in ⋃ (j : Fin m), B j, b ^ 2 ∂dB.μ

Omitted-tail identity (06_otqcs.tex, eq rounding-tails, second bound, in exact form): the cut loss is the off-window second moment, ‖k_t − k_t^{cut}‖₂² = ∫ b² dμ − ∫_{∪_j B_j} b² dμ (bounded by ρ + L² at consumption, where the omitted region is the union of the low window and the high tail).

theorem CommutingRepetition.selSharp_round {N : StdTracialAlgebra} {y : N.H} (dB : SpectralData N y) {m : ℕ} (B : Fin m → Set ℝ) (t : Fin m → ℝ) (hB : IsBandFamily B t) (r : ℝ) (hr : 1 ≤ r) (hband : ∀ (j : Fin m), B j ⊆ Set.Icc (t j / r) (t j)) : ‖N.ι (selSharp dB B t) - selCutVec dB B‖ ^ 2 ≤ (r - 1) ^ 2 * ‖y‖ ^ 2

Upward-rounding cost (06_otqcs.tex, eq rounding-tails, first bound): when every band sits inside [t_j / r, t_j] — the shifted-bin geometry at ratio r — the rounded modulus is (r−1)-close to the cut modulus in L², relative to the second moment: ‖k^♯ − k^{cut}‖₂² ≤ (r − 1)² ‖y‖₂² (at r = 1 + α this is ≤ α²).

theorem CommutingRepetition.Rop_v_norm {N : StdTracialAlgebra} {y : N.H} (dB : SpectralData N y) {m : ℕ} (B : Fin m → Set ℝ) (t : Fin m → ℝ) (hB : IsBandFamily B t) (c₁ c₂ : ℂ) : ‖(N.Rop dB.v) (c₁ • N.ι (selSharp dB B t) + c₂ • dB.hvec)‖ = ‖c₁ • N.ι (selSharp dB B t) + c₂ • dB.hvec‖

Right multiplication by the polar isometry preserves the norms of the rounded and exact moduli and their combinations (06_otqcs.tex, display below eq normalization-inequality: "right multiplication by v_t preserves the norms needed here"): the supports of k_t and k_t^♯ lie below s(k_t) = v_t v_t*.

Proof-side helpers (not manuscript statements)

theorem CommutingRepetition.selState_norm {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) : ‖selState dA dB Jd B t‖ = 1

The selected state is a unit vector in both branches of its definition: the trace vector at zero common mass, the normalized selected vector otherwise (using ‖w_{st}‖² = c_{st} ≠ 0). Consumed by the ∑ r conjunct of compile_decomposition (OTQCS/Compile).

theorem CommutingRepetition.selState_pairing {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) (A B' : N.A) : pairCross dA dB Jd B t * (inner ℂ (selState dA dB Jd B t) ((N.L A) ((N.Rop B') (selState dA dB Jd B t)))).re = (N.τ (star (selWord dA dB B t) * (A * selWord dA dB B t * B'))).re

Proof-side helper: c_{st} · ⟪z_{st}, L(A) R(B) z_{st}⟫ = τ(w_{st}* A w_{st} B) in both branches of z_{st} (at zero common mass both sides vanish, since ‖ι w‖² = c = 0).