OAI.Kaplansky.kaplansky_quasitrace_counterexample
OpenThe theorem (admitted in the source, not proved there) states that there exists a separable C*-algebra A, with its complex C*-algebra structure, for which the following hold. First, A carries a normalized 2-quasitrace. Here a 1-quasitrace is a function τ : A → ℂ such that τ(xx) is a nonnegative complex number for all x; τ(xx) = τ(xx*); τ(h + i k) = τ(h) + i τ(k) for self-adjoint h and k; and the restriction of τ to every norm-closed commutative (non-unital) star-subalgebra over ℂ is ℂ-linear. It is normalized if τ(1) = 1, and it is a 2-quasitrace if it extends to a 1-quasitrace σ on the 2×2 matrices over A (as a C*-matrix algebra) satisfying σ of the matrix with a in the upper-left corner and zeros elsewhere equal to τ(a) for all a. Second, there are positive contractions a and b in A, meaning each is of the form x*x and has norm at most 1, such that every normalized 2-quasitrace τ on A satisfies Re(τ(a+b) − τ(a) − τ(b)) ≥ 1/144. So no such τ is additive on this pair.
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/KaplanskyQuasitrace.lean; bytes 1737..1807
-- Kind: theorem; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.
import Mathlib.Algebra.Order.Star.Basic
import Mathlib.Analysis.CStarAlgebra.Classes
import Mathlib.Analysis.CStarAlgebra.CStarMatrix
import Definitions.Def_KaplanskyQuasitrace
namespace OAI
noncomputable section
open scoped ComplexOrder
namespace Kaplansky
variable {A : Type*} [CStarAlgebra A]
attribute [local instance] CStarAlgebra.spectralOrder CStarAlgebra.spectralOrderedRing
theorem kaplansky_quasitrace_counterexample : MainTarget := by sorry end Kaplansky end end OAI
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.