def CommutingRepetition.IsPosElem {A : Type u_1} [AddCommMonoid A] [Mul A] [Star A] (a : A) : Prop

Algebraic positivity: a is a finite sum of hermitian squares ∑ᵢ cᵢ* cᵢ — the algebraic positive cone of a ∗-ring. In a C*-algebra this coincides with the usual positive cone (a positive element is a single square, and a sum of squares is positive); the interface uses the sums-of-squares cone so that positivity of effects can be stated — and is closed under the POVM coarse-graining of node 1.1.3 — without any C*-structure. [DIFFERENCES.md D13]

Equations

• CommutingRepetition.IsPosElem a = ∃ (k : ℕ) (c : Fin k → A), a = ∑ i : Fin k, star (c i) * c i

theorem CommutingRepetition.isPosElem_star_mul_self {A : Type u_1} [AddCommMonoid A] [Mul A] [Star A] (c : A) : IsPosElem (star c * c)

A single hermitian square is algebraically positive.

theorem CommutingRepetition.isPosElem_zero {A : Type u_1} [AddCommMonoid A] [Mul A] [Star A] : IsPosElem 0

theorem CommutingRepetition.IsPosElem.add {A : Type u_1} [AddCommMonoid A] [Mul A] [Star A] {a b : A} (ha : IsPosElem a) (hb : IsPosElem b) : IsPosElem (a + b)

The algebraic positive cone is closed under addition.

theorem CommutingRepetition.isPosElem_sum {A : Type u_1} [AddCommMonoid A] [Mul A] [Star A] {ι : Type u_2} (s : Finset ι) (f : ι → A) (h : ∀ i ∈ s, IsPosElem (f i)) : IsPosElem (∑ i ∈ s, f i)

The algebraic positive cone is closed under finite sums — the fact POVM coarse-graining needs (node 1.1.3).

theorem CommutingRepetition.IsPosElem.smul_ofReal {A : Type u_1} [AddCommMonoid A] [Mul A] [Star A] [Module ℂ A] [SMulCommClass ℂ A A] [IsScalarTower ℂ A A] [StarModule ℂ A] {x : A} (hx : IsPosElem x) {r : ℝ} (hr : 0 ≤ r) : IsPosElem (↑r • x)

The algebraic positive cone is closed under nonnegative real scaling: r • (∑ cᵢ* cᵢ) = ∑ (√r cᵢ)* (√r cᵢ) — the fact convex combinations of effects need (05_prerounding.tex, eq effective-HK: "finite convex combinations of positive contractions in M").

structure CommutingRepetition.StdTracialAlgebra : Type (u + 1)

Standard form of a tracial ∗-algebra: carrier A with a normalized trace τ, the GNS Hilbert space H = L²(A, τ) with dense embedding ι, commuting left and right actions L, R, and the evaluation identities. [02_preliminaries.tex, "Finite tracial standard form"]

• A : Type u
• ringA : Ring self.A
• starRingA : StarRing self.A
• algebraA : Algebra ℂ self.A
• starModuleA : StarModule ℂ self.A
• τ : self.A →ₗ[ℂ] ℂ
• τ_one : self.τ 1 = 1
• τ_mul_comm (a b : self.A) : self.τ (a * b) = self.τ (b * a)
• τ_star (a : self.A) : self.τ (star a) = star (self.τ a)
• H : Type u
• nacgH : NormedAddCommGroup self.H
• ipsH : InnerProductSpace ℂ self.H
• completeH : CompleteSpace self.H
• ι : self.A →ₗ[ℂ] self.H
• ι_dense : DenseRange ⇑self.ι
• ι_inner (a b : self.A) : inner ℂ (self.ι a) (self.ι b) = self.τ (star a * b)
• L : self.A →⋆ₐ[ℂ] self.H →L[ℂ] self.H
• R : self.Aᵐᵒᵖ →⋆ₐ[ℂ] self.H →L[ℂ] self.H
• L_apply (a b : self.A) : (self.L a) (self.ι b) = self.ι (a * b)
• R_apply (a b : self.A) : (self.R (MulOpposite.op a)) (self.ι b) = self.ι (b * a)
• LR_commute (a b : self.A) : Commute (self.L a) (self.R (MulOpposite.op b))

noncomputable def CommutingRepetition.StdTracialAlgebra.traceVector (M : StdTracialAlgebra) : M.H

The trace vector Ω_τ = ι 1.

Equations

• M.traceVector = M.ι 1

noncomputable def CommutingRepetition.StdTracialAlgebra.Rop (M : StdTracialAlgebra) (a : M.A) : M.H →L[ℂ] M.H

Right action on an element written without the opposite wrapper.

Equations

• M.Rop a = M.R (MulOpposite.op a)

theorem CommutingRepetition.StdTracialAlgebra.inner_L_R (M : StdTracialAlgebra) (σ' x σ y : M.A) : inner ℂ (M.ι σ') ((M.L x) ((M.Rop y) (M.ι σ))) = M.τ (star σ' * (x * σ * y))

The evaluation identity behind everything in Sections 3–7: ⟪ι σ', L(x) R(y) ι σ⟫ = τ((σ')* x σ y). Specializes to the correlation formula ⟪σ, L(E) R(F) σ⟫ = τ(σ* E σ F) (03_tracial_reduction.tex, eq tracial-correlation-formula; audit node 1.1.4).

theorem CommutingRepetition.StdTracialAlgebra.τ_star_self_nonneg (M : StdTracialAlgebra) (a : M.A) : 0 ≤ (M.τ (star a * a)).re ∧ (M.τ (star a * a)).im = 0

τ is positive: τ(a* a) = ‖ι a‖² is a nonnegative real.

theorem CommutingRepetition.StdTracialAlgebra.L_isPositive (M : StdTracialAlgebra) {a : M.A} (ha : IsPosElem a) : (M.L a).IsPositive

The left action of an algebraically positive element is a positive operator: L(∑ cᵢ* cᵢ) = ∑ L(cᵢ)† ∘ L(cᵢ).

theorem CommutingRepetition.StdTracialAlgebra.Rop_isPositive (M : StdTracialAlgebra) {a : M.A} (ha : IsPosElem a) : (M.Rop a).IsPositive

The right action of an algebraically positive element is a positive operator: R(op(∑ cᵢ* cᵢ)) = ∑ R(op cᵢ) ∘ R(op cᵢ)†.

theorem CommutingRepetition.StdTracialAlgebra.pairing_nonneg (M : StdTracialAlgebra) (σ : M.A) {u w : M.A} (hu : IsPosElem u) (hw : IsPosElem w) : 0 ≤ (M.τ (star σ * (u * σ * w))).re

Positivity of the two-sided pairing: for algebraically positive u, w and any σ, τ(σ* u σ w) = ⟪ι σ, L(u) R(w) ι σ⟫ ≥ 0 — the commuting product of the positive operators L(u) and R(w) applied to the state ι σ (the Born-rule nonnegativity behind eq tracial-correlation-formula and the detagging inequality of node 1.1.3).