structure CommutingRepetition.JointSpectralData {N : StdTracialAlgebra} {x y : N.H} (dA : SpectralData N x) (dB : SpectralData N y) : Type

Joint left–right spectral coupling of two modulus packages (node 1.3.2; 06_otqcs.tex, eqs joint-measure + joint-moments): a probability measure on ℝ × ℝ whose marginals are the two spectral distributions, whose rectangle masses are the traces τ(1_I(h) 1_J(k)) (eq joint-measure — in particular those traces are nonnegative), and whose second cross moment is ‖h − k‖₂² (eq joint-moments; the coordinate second moments come from the marginals and SpectralData.moment2). No joint PVM for h, k inside the algebra is asserted.

• ν : MeasureTheory.Measure (ℝ × ℝ)
• ν_prob : MeasureTheory.IsProbabilityMeasure self.ν
• margA : MeasureTheory.Measure.map Prod.fst self.ν = dA.μ
• margB : MeasureTheory.Measure.map Prod.snd self.ν = dB.μ
• cross (I J : Set ℝ) : MeasurableSet I → MeasurableSet J → N.τ (dA.proj I * dB.proj J) = ↑(self.ν (I ×ˢ J)).toReal
• crossMoment : ∫ (p : ℝ × ℝ), (p.1 - p.2) ^ 2 ∂self.ν = ‖dA.hvec - dB.hvec‖ ^ 2

structure CommutingRepetition.ModulusFamily (N : StdTracialAlgebra) {S : Type v} {T : Type w} (x : S → N.H) (y : T → N.H) : Type (max (max u v) w)

Modulus family over label families of vectors (nodes 1.3.1 + 1.3.2): per-vector spectral packages for Alice's x_s and Bob's y_t, a joint coupling for every pair, and the modulus stability bound ‖h_s − k_t‖₂² ≤ 2 ‖x_s − y_t‖₂² (node 1.3.1; 06_otqcs.tex, lem otqcs-modulus, eq modulus-stability — stated pairwise, which is how eq Dbar-Delta consumes it).

• dataA (s : S) : SpectralData N (x s)
• dataB (t : T) : SpectralData N (y t)
• joint (s : S) (t : T) : JointSpectralData (self.dataA s) (self.dataB t)
• stability (s : S) (t : T) : ‖(self.dataA s).hvec - (self.dataB t).hvec‖ ^ 2 ≤ 2 * ‖x s - y t‖ ^ 2

theorem CommutingRepetition.exists_modulusFamily (N : StdTracialAlgebra) {S : Type v} {T : Type w} (x : S → N.H) (y : T → N.H) : ∃ (ext : TracialExtension N), Nonempty (ModulusFamily ext.N' (fun (s : S) => ext.U (x s)) fun (t : T) => ext.U (y t))

Existence of the modulus family over a tracial extension (nodes 1.3.1 + 1.3.2; 06_otqcs.tex, §"Left moduli and a joint left–right spectral measure"): every finite-vector family over a standard-form algebra admits, after passing to a tracial extension (the von Neumann algebra generated by the left action, acting on the unitarily identified L² — OTQCS/Modulus.lean), left-modulus spectral packages, pairwise joint couplings, and the stability bound. The single von Neumann root of Section 6 (work package B7: polar decomposition, Borel functional calculus, the joint PVM of strongly commuting actions, and the L²-Lipschitz bound of appendix otqcs-absolute-value).