OAI.FiniteFactor.main_theorem
ProvedThe theorem states that the proposition MainTarget (at universe level 0) holds: there exist a complex Hilbert space H (in the lowest universe) and a von Neumann algebra M of bounded operators on H such that M has scalar center (every element of M commuting with all of M is a complex multiple of the identity), M is finite (every isometry v in M, meaning vv = 1, also satisfies vv = 1), M has no minimal projection (for every nonzero self-adjoint idempotent p in M there is a nonzero projection q in M with q different from p and qp = q, that is, q lies strictly below p), and M has a separable predual (there is a separable complex Banach space E whose dual is conjugate-linearly isometrically isomorphic to M as a normed star-algebra). Moreover, M contains a nonzero operator T that is quasinilpotent, meaning ‖T^n‖^(1/n) tends to 0 as n tends to infinity, and that has no nontrivial invariant projection in M: whenever p is a projection in M with (1 − p)Tp = 0, then p = 0 or p = 1.
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/FiniteFactor.lean; bytes 1709..1760
-- Kind: theorem; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.
import Mathlib.Analysis.VonNeumannAlgebra.Basic
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Definitions.Def_FiniteFactor
namespace OAI
namespace FiniteFactor
open Filter
open scoped Topology
universe u
variable {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
theorem main_theorem : MainTarget.{0} := by
sorry
end FiniteFactor
end OAI
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.