structure CommutingRepetition.TracialExtension (N : StdTracialAlgebra) : Type (u + 1)

A tracial extension of a standard-form algebra: a second standard-form algebra N' together with a unital ∗-homomorphism of carriers and a unitary identification of the L² spaces intertwining the embeddings and both actions. The intended instance is the von Neumann algebra generated by the left action — acting on the same L² space (the extension of the trace is spatial), which is why a single unitary U carries all Section 6 comparisons back to the original data. [06_otqcs.tex, standing assumptions: "finite von Neumann algebra with faithful normal normalized trace", reached from the tracial ∗-algebra of the Section 5 output by closure]

• N' : StdTracialAlgebra
• emb : N.A →⋆ₐ[ℂ] self.N'.A
• U : N.H ≃ₗᵢ[ℂ] self.N'.H
• U_ι (a : N.A) : self.U (N.ι a) = self.N'.ι (self.emb a)
• L_emb (a : N.A) (ξ : N.H) : (self.N'.L (self.emb a)) (self.U ξ) = self.U ((N.L a) ξ)
• R_emb (a : N.A) (ξ : N.H) : (self.N'.Rop (self.emb a)) (self.U ξ) = self.U ((N.Rop a) ξ)

structure CommutingRepetition.SpectralData (N : StdTracialAlgebra) (x : N.H) : Type u

Left-modulus spectral package for a vector x (node 1.3.1; 06_otqcs.tex, eq left-polar): the consumed form of the left polar decomposition x = h_x v_x, h_x = (x x*)^{1/2}, v_x v_x* = s(h_x). Carries: the spectral distribution μ of h_x in the trace (a probability measure on ℝ, supported on [0, ∞), with the kernel atom at 0); the modulus as an L² vector hvec (‖h_x‖₂ = ‖x‖₂, second moment ∫ b² dμ = ‖x‖²); the polar partial isometry v with h_x · v = x and h_x · (v v*) = h_x; and the band spectral projections proj I = 1_I(h_x) with their ∗-lattice identities, trace masses, support absorption above 0, and the two moment pairings against hvec that the rounding estimates of eqs rounded-y/rounding-tails consume.

• μ : MeasureTheory.Measure ℝ
• μ_prob : MeasureTheory.IsProbabilityMeasure self.μ
• μ_nonneg : self.μ (Set.Iio 0) = 0
• hvec : N.H
• hvec_norm : ‖self.hvec‖ = ‖x‖
• moment2 : ∫ (b : ℝ), b ^ 2 ∂self.μ = ‖x‖ ^ 2
• v : N.A
• polar : (N.Rop self.v) self.hvec = x
• supp_vec : (N.Rop (self.v * star self.v)) self.hvec = self.hvec
• proj : Set ℝ → N.A
• proj_star (I : Set ℝ) : star (self.proj I) = self.proj I
• proj_empty : self.proj ∅ = 0
• proj_inter (I J : Set ℝ) : MeasurableSet I → MeasurableSet J → self.proj I * self.proj J = self.proj (I ∩ J)
• proj_union (I J : Set ℝ) : MeasurableSet I → MeasurableSet J → Disjoint I J → self.proj (I ∪ J) = self.proj I + self.proj J
• proj_trace (I : Set ℝ) : MeasurableSet I → N.τ (self.proj I) = ↑(self.μ I).toReal
• absorb (I : Set ℝ) : MeasurableSet I → I ⊆ Set.Ioi 0 → self.v * star self.v * self.proj I = self.proj I
• pairing1 (I : Set ℝ) : MeasurableSet I → inner ℂ (N.ι (self.proj I)) self.hvec = ↑(∫ (b : ℝ) in I, b ∂self.μ)
• pairing2 (I : Set ℝ) : MeasurableSet I → inner ℂ self.hvec ((N.Rop (self.proj I)) self.hvec) = ↑(∫ (b : ℝ) in I, b ^ 2 ∂self.μ)