Trace from Dixmier: uniqueness of the scalar gives linearity for free
If every closed unitary-orbit hull K(x) in a factor contains exactly one scalar τ(x), then τ is additive. The key is that for a unitary average α (a convex combination of y ↦ u y u*), K(α y) ⊆ K(y), because averages compose, so τ(α y) = τ(y). Given ε, pick α with ‖α x − τx‖ < ε/2, then β with ‖β(α y) − τy‖ < ε/2. Averages are contractions and fix scalars, so βα(x + y) is within ε of τx + τy, and uniqueness gives τ(x+y) = τx + τy. In Lean, represent averages as the convex hull of conjugations inside Module.End ℝ B(H). Then K(x) is the image under evaluation (LinearMap.image_convexHull with LinearMap.applyₗ), and composition is just multiplication in Module.End. The genuinely hard part is uniqueness, which in a finite factor is equivalent to the existence of a tracial state.
Follow-up: the missing uniqueness is now proved for every finite factor, following Anantharaman–Popa §6.3 (Murray–von Neumann). You only need, for each ε, vectors η_i with Σ‖z*η_i‖² ≤ (1+ε)Σ‖zη_i‖² on M. These come from a vector state sandwiched by the dimension below a small projection, and are then spread by partial isometries. The limit trace is never constructed; uniqueness of the scalar plus this note's argument give linearity.