Plectis Atlas
Search

↑ and ↓ move, Enter opens, Esc closes.

Lean statement

Uniform property $\Gamma$ from tracial real rank zero

Lean is a language for mathematical statements and proofs that a computer can verify. This page shows one statement file from OpenAI’s release, possible paper matches and independent reports. The code-like names below identify the definitions or theorems selected by the proof-verification settings.

Theorem selected for verification: OAI.ComparatorModel.CurrentMain.main

Lean statement file: UniformGamma.leanShow on the mapFamily 291. OpenAI lists this as a main result in its Lean catalogue.

See the candidate theoremWho ran the proof-verification programReport a comparison with the paper (GitHub issue)

The Lean statement

The lines of the Lean statement that state the theorem, then the definitions in the file that it uses.

theorem CurrentMain.main : MainClaim.{uNuclear} := by  sorry

A Lean statement states the theorem and leaves its proof as sorry on purpose. OpenAI’s proof is in a separate solution module, and a program called Comparator checks that proof against this statement.

Definitions needed to read it

Local definitions the statement names, followed through the definitions they name in turn. The match is by name in the source text, so a name reached only through notation can be missed; the full file is below.

  • structure OAI.Pureness.CStarAlgebraNorm line 18

    structure CStarAlgebraNorm (R : Type uR) [Ring R] [StarRing R] [Algebra ℂ R]    extends AlgebraNorm ℂ R where  cstar : ∀ x, toAlgebraNorm (star x * x) = toAlgebraNorm x * toAlgebraNorm x

  • structure OAI.Pureness.TracialState line 22

    structure TracialState (A : Type uA) [CStarAlgebra A] [PartialOrder A] where  functional : A →ₚ[ℂ] ℂ  normalized : functional 1 = 1  tracial : ∀ a b : A, functional (a * b) = functional (b * a)

  • structure OAI.Pureness.ClosedStarIdeal line 27

    structure ClosedStarIdeal (D : Type uD) [CStarAlgebra D] where  ideal : TwoSidedIdeal D  star_mem : ∀ {u : D}, u ∈ ideal → star u ∈ ideal  isClosed : IsClosed (ideal : Set D)

  • definition OAI.ComparatorModel.Pureness.IsNuclear line 44

    def IsNuclear (A : Type u) [CStarAlgebra A] : Prop :=  ∀ (B : Type v) [CStarAlgebra B], Subsingleton (CStarAlgebraNorm (A ⊗[ℂ] B))

  • definition OAI.ComparatorModel.CurrentMain.RealRankZero line 57

    def RealRankZero (D : Type) [CStarAlgebra D] : Prop :=  ∀ a : D, IsSelfAdjoint a → ∀ ε : ℝ, 0 < ε →    ∃ b : D, IsSelfAdjoint b ∧ (spectrum ℂ b).Finite ∧ ‖a - b‖ < ε

  • definition OAI.ComparatorModel.CurrentMain.traceTwoNorm line 61

    def traceTwoNorm {D : Type} [CStarAlgebra D] [PartialOrder D]    (τ : TracialState D) (a : D) : ℝ :=  Real.sqrt (τ.functional (star a * a)).re

  • abbreviation OAI.ComparatorModel.Pureness.ClosedStarIdeal.Quotient line 81

    abbrev Quotient := J.ideal.ringCon.Quotient

  • definition OAI.ComparatorModel.Pureness.ClosedStarIdeal.quotientMap line 83

    def quotientMap : D →ₐ[ℂ] J.Quotient := J.ideal.ringCon.mkₐ ℂ

  • class OAI.ComparatorModel.Pureness.ClosedStarIdeal.NormConstruction line 131

    class NormConstruction : Prop where  mul_le : ∀ {D : Type} [CStarAlgebra D] (J : ClosedStarIdeal D) (x y : J.Quotient),    ‖x*y‖ ≤ ‖x‖*‖y‖  star_eq : ∀ {D : Type} [CStarAlgebra D] (J : ClosedStarIdeal D) (x : J.Quotient),    ‖star x‖ = ‖x‖  square_le : ∀ {D : Type} [CStarAlgebra D] [PartialOrder D] [StarOrderedRing D]    (J : ClosedStarIdeal D) (x : J.Quotient), ‖x‖ * ‖x‖ ≤ ‖star x * x‖

  • definition OAI.ComparatorModel.CurrentMain.familyTwoNorm line 182

    def CurrentMain.familyTwoNorm (a : D) : ℝ := ⨆ i, traceTwoNorm (τ i) a

  • definition OAI.ComparatorModel.CurrentMain.IsFamilyNull line 201

    def CurrentMain.IsFamilyNull (F : Filter X) (u : X → D) : Prop :=  Tendsto (fun n => familyTwoNorm τ (u n)) F (𝓝 0)

  • class OAI.ComparatorModel.CurrentMain.NullConstruction line 204

    class CurrentMain.NullConstruction : Prop where
    Show the remaining 17 lines
      zero : ∀ {D I X : Type} [CStarAlgebra D] [PartialOrder D] [StarOrderedRing D] (τ : I → Pureness.TracialState D) [Nonempty I]    (F : Filter X), IsFamilyNull τ F (fun _ => 0)  add : ∀ {D I X : Type} [CStarAlgebra D] [PartialOrder D] [StarOrderedRing D] (τ : I → Pureness.TracialState D) [Nonempty I]    {F : Filter X} {u v : X → D}, IsFamilyNull τ F u → IsFamilyNull τ F v →    IsFamilyNull τ F (fun n => u n + v n)  neg : ∀ {D I X : Type} [CStarAlgebra D] [PartialOrder D] [StarOrderedRing D] (τ : I → Pureness.TracialState D) [Nonempty I]    {F : Filter X} {u : X → D}, IsFamilyNull τ F u → IsFamilyNull τ F (fun n => -u n)  star : ∀ {D I X : Type} [CStarAlgebra D] [PartialOrder D] [StarOrderedRing D] (τ : I → Pureness.TracialState D) [Nonempty I]    {F : Filter X} {u : X → D}, IsFamilyNull τ F u → IsFamilyNull τ F (fun n => star (u n))  mul_left : ∀ {D I X : Type} [CStarAlgebra D] [PartialOrder D] [StarOrderedRing D] (τ : I → Pureness.TracialState D) [Nonempty I]    {F : Filter X} {u v : X → D}, IsFamilyNull τ F v → ∀ {M : ℝ},    (∀ n, ‖u n‖ ≤ M) → IsFamilyNull τ F (fun n => u n * v n)  mul_right : ∀ {D I X : Type} [CStarAlgebra D] [PartialOrder D] [StarOrderedRing D] (τ : I → Pureness.TracialState D) [Nonempty I]    {F : Filter X} {u v : X → D}, IsFamilyNull τ F u → ∀ {M : ℝ},    (∀ n, ‖v n‖ ≤ M) → IsFamilyNull τ F (fun n => u n * v n)  closed : ∀ {D I X : Type} [CStarAlgebra D] [PartialOrder D] [StarOrderedRing D] (τ : I → Pureness.TracialState D) [Nonempty I] (F : Filter X),    IsClosed {u : lp (fun _ : X => D) ∞ | IsFamilyNull τ F (fun n => u n)}

  • definition OAI.ComparatorModel.CurrentMain.familyNullTwoSided line 227

    def CurrentMain.familyNullTwoSided (F : Filter X) : TwoSidedIdeal (lp (fun _ : X => D) ∞) :=  TwoSidedIdeal.mk' {u | IsFamilyNull τ F (fun n => u n)}    (NullConstruction.zero τ F)    (fun hu hv => NullConstruction.add τ hu hv)    (fun hu => NullConstruction.neg τ hu)    (fun {u _} hv => NullConstruction.mul_left τ hv      (lp.norm_apply_le_norm ENNReal.top_ne_zero u))    (fun {_ v} hu => NullConstruction.mul_right τ hu      (lp.norm_apply_le_norm ENNReal.top_ne_zero v))

  • definition OAI.ComparatorModel.CurrentMain.familyNullIdeal line 237

    def CurrentMain.familyNullIdeal (F : Filter X) : ClosedStarIdeal (lp (fun _ : X => D) ∞) where
    Show the remaining 12 lines
      ideal := familyNullTwoSided τ F  star_mem := by    intro u hu    apply (TwoSidedIdeal.mem_mk' _ _ _ _ _ _ (star u)).mpr    exact NullConstruction.star τ ((TwoSidedIdeal.mem_mk' _ _ _ _ _ _ u).mp hu)  isClosed := by    have he : (familyNullTwoSided τ F : Set (lp (fun _ : X => D) ∞)) =        {u | IsFamilyNull τ F (fun n => u n)} := by      ext u      exact TwoSidedIdeal.mem_mk' _ _ _ _ _ _ u    rw [he]    exact NullConstruction.closed τ F

  • definition OAI.ComparatorModel.CurrentMain.IsFamilyCauchy line 259

    def CurrentMain.IsFamilyCauchy (u : ℕ → D) : Prop :=  IsFamilyNull τ (atTop : Filter (ℕ × ℕ)) (fun p => u p.1 - u p.2)

  • class OAI.ComparatorModel.CurrentMain.CauchyConstruction line 262

    class CurrentMain.CauchyConstruction : Prop where
    Show the remaining 15 lines
      const : ∀ {D I : Type} [CStarAlgebra D] [PartialOrder D] [StarOrderedRing D]    (τ : I → Pureness.TracialState D) [Nonempty I] (a : D), IsFamilyCauchy τ (fun _ => a)  add : ∀ {D I : Type} [CStarAlgebra D] [PartialOrder D] [StarOrderedRing D]    (τ : I → Pureness.TracialState D) [Nonempty I] {u v : ℕ → D},    IsFamilyCauchy τ u → IsFamilyCauchy τ v → IsFamilyCauchy τ (fun n => u n+v n)  star : ∀ {D I : Type} [CStarAlgebra D] [PartialOrder D] [StarOrderedRing D]    (τ : I → Pureness.TracialState D) [Nonempty I] {u : ℕ → D},    IsFamilyCauchy τ u → IsFamilyCauchy τ (fun n => star (u n))  mul : ∀ {D I : Type} [CStarAlgebra D] [PartialOrder D] [StarOrderedRing D]    (τ : I → Pureness.TracialState D) [Nonempty I] {u v : ℕ → D},    IsFamilyCauchy τ u → IsFamilyCauchy τ v → ∀ {M N : ℝ},    (∀ n, ‖u n‖ ≤ M) → (∀ n, ‖v n‖ ≤ N) → IsFamilyCauchy τ (fun n => u n*v n)  closed : ∀ {D I : Type} [CStarAlgebra D] [PartialOrder D] [StarOrderedRing D]    (τ : I → Pureness.TracialState D) [Nonempty I] [Nontrivial D],    IsClosed {u : lp (fun _ : ℕ => D) ∞ | IsFamilyCauchy τ (fun n => u n)}

  • definition OAI.ComparatorModel.CurrentMain.familyCauchyAlgebra line 283

    def CurrentMain.familyCauchyAlgebra : StarSubalgebra ℂ (lp (fun _ : ℕ => D) ∞) where  carrier := {u | IsFamilyCauchy τ (fun n => u n)}  zero_mem' := CauchyConstruction.const τ 0  one_mem' := CauchyConstruction.const τ 1  add_mem' hu hv := CauchyConstruction.add τ hu hv  mul_mem' {u v} hu hv := CauchyConstruction.mul τ hu hv    (lp.norm_apply_le_norm ENNReal.top_ne_zero u)    (lp.norm_apply_le_norm ENNReal.top_ne_zero v)  algebraMap_mem' z := CauchyConstruction.const τ (algebraMap ℂ D z)  star_mem' hu := CauchyConstruction.star τ hu

  • definition OAI.ComparatorModel.CurrentMain.familyCauchyNullIdeal line 299

    def CurrentMain.familyCauchyNullIdeal : ClosedStarIdeal (familyCauchyAlgebra τ) where  ideal := TwoSidedIdeal.comap (familyCauchyAlgebra τ).val.toRingHom    (familyNullIdeal τ atTop).ideal  star_mem := by    intro u hu    apply (familyNullIdeal τ atTop).star_mem hu  isClosed := by    exact (familyNullIdeal τ atTop).isClosed.preimage      (continuous_subtype_val : Continuous (fun u : familyCauchyAlgebra τ => u.1))

  • abbreviation OAI.ComparatorModel.CurrentMain.UniformTracialCompletion line 309

    abbrev CurrentMain.UniformTracialCompletion := (familyCauchyNullIdeal τ).Quotient

  • definition OAI.ComparatorModel.Pureness.ClosedStarIdeal.descendedValue line 331

    def Pureness.ClosedStarIdeal.descendedValue : J.Quotient → ℂ := Quotient.lift τ.functional (by  intro u v huv  change J.ideal.ringCon u v at huv  rw [TwoSidedIdeal.rel_iff] at huv  have h := hτ (u-v) huv  rw [map_sub, sub_eq_zero] at h  exact h)

  • definition OAI.ComparatorModel.Pureness.ClosedStarIdeal.descendedLinear line 339

    def Pureness.ClosedStarIdeal.descendedLinear : J.Quotient →ₗ[ℂ] ℂ where  toFun := J.descendedValue τ hτ  map_add' x y := Quotient.inductionOn₂' x y (fun u v => τ.functional.map_add u v)  map_smul' c x := Quotient.inductionOn' x (fun u => τ.functional.map_smul c u)

  • definition OAI.ComparatorModel.Pureness.ClosedStarIdeal.descendedTrace line 344

    def Pureness.ClosedStarIdeal.descendedTrace : TracialState J.Quotient where
    Show the remaining 12 lines
      functional := { J.descendedLinear τ hτ with    monotone' := by      intro x y hxy      apply sub_nonneg.mp      change 0 ≤ J.descendedLinear τ hτ y - J.descendedLinear τ hτ x      rw [← map_sub]      obtain ⟨z,hz⟩ := CStarAlgebra.nonneg_iff_eq_star_mul_self.mp (sub_nonneg.mpr hxy)      rw [hz]      induction z using Quotient.inductionOn' with      | h u => exact τ.functional.map_nonneg (star_mul_self_nonneg u) }  normalized := τ.normalized  tracial x y := Quotient.inductionOn₂' x y (fun u v => τ.tracial u v)

  • definition OAI.ComparatorModel.CurrentMain.ultraTraceValue line 380

    def CurrentMain.ultraTraceValue (u : lp (fun _ : X => D) ∞) : ℂ :=  limUnder (U : Filter X) (fun n => (θ n).functional (u n))

  • class OAI.ComparatorModel.CurrentMain.LimitConstruction line 383

    class CurrentMain.LimitConstruction : Prop where  tendsto : ∀ {D X : Type} [CStarAlgebra D] [PartialOrder D] [StarOrderedRing D]    (θ : X → Pureness.TracialState D) (U : Ultrafilter X) (u : lp (fun _ : X => D) ∞),    Tendsto (fun n => (θ n).functional (u n)) (U : Filter X) (𝓝 (ultraTraceValue θ U u))

16 more definitions are reached the same way; the full file lists them.

Possible paper match, with no recorded review

Atlas selected this possible match by comparing words in the Lean statement with every statement in the family. No review of whether the statements mean the same thing is recorded.

Words of the Lean statement, its names split into words, that also appear in the theorem: quotient, stably, ultrafilter, real, 1/2, rank, property, norm and ten more. Found in the paper’s title, which its main theorem states: tracial. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: free, infinite and unital.

Statements in Tracial projection methods and uniform property Gamma come first because the release lists only that paper for this Lean statement.

Theorem 1.1 of Tracial projection methods and uniform property Gamma

Theorem (Real rank zero and uniform property \Gamma)

Let A be a unital, separable, simple, infinite-dimensional, nuclear, stably finite C^*-algebra with T(A)\ne\varnothing, and let B=\overline A^{T(A)}. Fix any free ultrafilter \omega on \N. If B^\omega has real rank zero in its quotient C^*-norm, then there is a projection p\in B^\omega\cap B' such that

\lambda(px)=\tfrac12\lambda(x) \qquad(x\in B,\ \lambda\in\Lambda_\omega).

In particular, A has uniform property \Gamma.

Section 1, Introduction Read it in the paper TeX source, line 57
Show the TeX
Let $A$ be a unital, separable, simple, infinite-dimensional, nuclear,
stably finite $C^*$-algebra with $T(A)\ne\varnothing$, and let
$B=\overline A^{T(A)}$. Fix any free ultrafilter $\omega$ on $\N$.
If $B^\omega$ has real rank zero in its quotient $C^*$-norm, then there is
a projection $p\in B^\omega\cap B'$ such that
\[
 \lambda(px)=\tfrac12\lambda(x)
 \qquad(x\in B,\ \lambda\in\Lambda_\omega).
\]
In particular, $A$ has uniform property $\Gamma$.

Other possible paper matches, closest wording first

  • Corollary 1.2 of Tracial projection methods and uniform property Gamma. Words of the Lean statement, its names split into words, that also appear in the theorem: unique, completion, continuous, quotient, real, state and six more.
  • Theorem 1.5 of Tracial projection methods and uniform property Gamma. Words of the Lean statement, its names split into words, that also appear in the theorem: stably, nonempty, trace, property, bounded, gamma and six more. Found in the paper’s title, which its main theorem states: tracial.
  • Theorem 11.4 of Tracial projection methods and uniform property Gamma. Words of the Lean statement, its names split into words, that also appear in the theorem: state, space, nonempty, tracial, property, gamma and eight more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: infinite and unital.
  • Proposition 8.1 of Tracial projection methods and uniform property Gamma. Words of the Lean statement, its names split into words, that also appear in the theorem: values, ranks, trace, bound, simple, integer and four more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: infinite and unital.
  • Theorem 1.4 of Tracial projection methods and uniform property Gamma. Words of the Lean statement, its names split into words, that also appear in the theorem: property, gamma, simple, uniform, dimensional, nuclear and two more. Found in the paper’s title, which its main theorem states: tracial and projection. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: infinite and unital.
  • Proposition 11.2 of Tracial projection methods and uniform property Gamma. Words of the Lean statement, its names split into words, that also appear in the theorem: sqrt, limit, construction, commuting, norm, properties and one more.

How Atlas selects possible matches: it compares words in the Lean statement with every statement in the family. It also splits Lean names into words. The release’s label and note receive less weight; a main theorem wins a close match. If the Lean wording yields no clear match, Atlas uses the catalogue description. This selects passages to compare; it does not establish that they mean the same thing.

Reported Comparator runs

three independent groups report that Comparator accepted runs for this Lean statement file: Carlos Toledo’s cert-machine; MathVet; Neal McBurnett’s openai-math-lean-tooling. Each group reports its own Comparator run for this statement file. Atlas has not repeated the runs.

For a configured theorem, Comparator tests whether OpenAI’s proof proves the exact Lean statement. Some files instead configure definitions for comparison by name and type. Acceptance does not establish that the statement means the same thing as the paper’s theorem.

Carlos Toledo’s cert-machine

How they ran it, in their words

Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule; every family’s challenge statements read against OpenAI’s headline, clause by clause. Decider: Comparator (leanprover/comparator d03acab1 = tag v4.34.0, built with the release’s toolchain v4.34.1), lean4export 076e8e57, landrun 811cfff5, nanoda_lib 3a240721 — on GitHub’s Linux runners (.github/workflows/openai-math-kernel.yml), one j…

  • Accepted Their term: “CERTIFIED”.

    Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.

    Reported 10 October 2026, at the release version shown here. Original verification report

MathVet

How they ran it, in their words

An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge. Its protocol describes a planned error-rate study; this import does not establish that the study has been completed.

  • Accepted Their term: “comparator-sandboxed-pass”.

    Re-run through Comparator in a sandboxed virtual machine: accepted.

    Reported 8 October 2026, at the release version shown here. Original verification report

Neal McBurnett’s openai-math-lean-tooling

How they ran it, in their words

Each challenge’s solution is built and checked by Comparator at the pinned release, on Lean leanprover/lean4:v4.34.1, recording the verdict, the check time and the peak memory; the run was still in progress at this snapshot (192 accepted, 224 pending).

  • Accepted Their term: “accepted”.

    Re-run through Comparator with Lean’s kernel: accepted (the check took 544 s; peak memory 6.5 GiB).

    Reported 11 October 2026, at the release version shown here. Original verification report

What an accepted Comparator run would establish

If Comparator is run under this configuration and accepts, the solution proves the configured theorem using only the allowed axioms, and the Lean kernel accepts every step.

This configuration lists no definition holes, so every definition the statement uses is compared as it is written in this file.

Allowed axioms: propext, Quot.sound, Classical.choice

Acceptance leaves open whether the Lean statement means the same thing as the paper’s theorem, whether the paper’s other claims are correct, and whether the result is new. Those questions require comparing the definitions and statements, reviewing the paper’s arguments, and reading the earlier literature.

Do family 291’s Lean statements express the advertised result?

These assessments compare all the family’s Lean statements with the whole result OpenAI describes in its catalogue. They do not assess this statement alone. Each group uses its own published rules.

Neither group finds that the Lean statements express or imply the whole advertised result. They describe what the statements express in different terms.

  • MathVet

    Finds a supporting or a different result stated Their term: “supporting-only”.

    The challenge statements state a lemma or auxiliary result, not the headline. Their record

    Their note: The single challenge is CurrentMain.main : MainClaim, i.e. Statement (for a simple separable nuclear stably finite infinite-dimensional C*-algebra with tracial states and a free ultrafilter U, if the uniform tracial ultrapower of the uniform tracial completion has real rank zero then UniformPropertyGammaAt A U), preceded by existential witnesses for the hand-built NormConstruction/NullConstruction/CauchyConstruction/LimitConstruction/TraceConstruction classes. This is a supporting technical implication (docs: 'real rank zero ... implies uniform property Γ'). The summary's headline results, equivariant Jiang-Su stability for every countable discrete amenable group action and the unital Toms-Winter conjecture (strict comparison ⇔ finite nuclear dimension ⇔ Jiang-Su stability), are not stated.

    Definitions the group asks readers to compare with the paper: The uniform tracial completion and ultrapowers are hand-built quotients: UniformTracialCompletion := (familyCauchyNullIdeal τ).Quotient, FamilyUltrapower := (familyNullIdeal τ U).Quotient, with class NormConstruction : Prop/NullConstruction/CauchyConstruction/LimitConstruction/TraceConstruction and MainClaim := ∃ h0 : NormConstruction, ... ∃ h4 : TraceConstruction, Statement, i.e. the C*-algebra structure is posited as existentially provable classes inside the claim; IsNuclear and RealRankZero are also local definitions.

  • Carlos Toledo’s cert-machine

    Finds a supporting or a different result stated Their term: “DIFFERENT”.

    The challenge statements state a different theorem from the headline. Their record

    Their note: The only challenge (UniformGamma) states a different theorem from the 'Tracial projection methods' manuscript: real rank zero of the uniform tracial ultrapower of the uniform tracial completion implies uniform property Γ (Schafhauser–Tikuisis–White Problem XXI). Neither headline clause is stated, and the stated theorem is neither implied by nor implies them.

Read the complete assessments on the family page.

OpenAI’s own note on what this Lean statement covers

“The formalization proves that real rank zero of the uniform tracial ultrapower of the uniform tracial completion implies uniform property $\Gamma$ for a simple separable unital infinite-dimensional nuclear stably finite $C^*$-algebra with traces. The conclusion holds at every specified free ultrafilter under the corresponding real-rank-zero hypothesis.”

An AI agent drafted an interpretation of that note, classifying this statement as “states a paper’s theorem as the paper does”. No human review of the draft is recorded.

Supporting material

The complete Lean statement file

607 lines, copied from release version fd4aeeb. A name defined in this file links to its line; pointing at the name shows its definition.

Declared in this fileOpenAI’s library at fd4aeebOther linked names open the current documentation for Mathlib, Lean’s mathematical library.

Links in the file: 239 to its own declarations, 343 to Mathlib’s documentation. 45 declared names also link to the same declaration in OpenAI’s library. 2 identifiers stay plain because they resolve to no single declaration: variables Lean binds automatically, notation, or names the scan of the pinned sources did not find. OpenAI uses Mathlib version d13f23b. The linked documentation describes the current version, so names that have since changed may be missing there.

import Mathlibnamespace OAInoncomputable section/-!The final claim constructs the tracial quotients and states the original gamma assertion.`Analysis.TracialSplitting.Challenge.main_iff_original` verifies statement preservation.-/universe uA uD uE uI uR uX u vnamespace Purenessopen scoped ComplexOrderstructure CStarAlgebraNorm (R : Type uR) [Ring R] [StarRing R] [Algebra ℂ R]    extends AlgebraNorm ℂ R where  cstar : ∀ x, toAlgebraNorm (star x * x) = toAlgebraNorm x * toAlgebraNorm xstructure TracialState (A : Type uA) [CStarAlgebra A] [PartialOrder A] where  functional : A →ₚ[ℂ] ℂ  normalized : functional 1 = 1  tracial : ∀ a b : A, functional (a * b) = functional (b * a)structure ClosedStarIdeal (D : Type uD) [CStarAlgebra D] where  ideal : TwoSidedIdeal D  star_mem : ∀ {u : D}, u ∈ ideal → star u ∈ ideal  isClosed : IsClosed (ideal : Set D)end Purenessuniverse uNuclearnamespace ComparatorModelnamespace Purenessopen scoped TensorProduct ComplexOrderabbrev CStarAlgebraNorm := @_root_.OAI.Pureness.CStarAlgebraNormdef IsNuclear (A : Type u) [CStarAlgebra A] : Prop :=  ∀ (B : Type v) [CStarAlgebra B], Subsingleton (CStarAlgebraNorm (A ⊗[ℂ] B))abbrev TracialState := @_root_.OAI.Pureness.TracialStateend Purenessnamespace CurrentMainopen _root_.OAI.ComparatorModel.Purenessopen scoped ComplexOrderdef RealRankZero (D : Type) [CStarAlgebra D] : Prop :=  ∀ a : D, IsSelfAdjoint a → ∀ ε : ℝ, 0 < ε →    ∃ b : D, IsSelfAdjoint b ∧ (spectrum ℂ b).Finite ∧ ‖a - b‖ < εdef traceTwoNorm {D : Type} [CStarAlgebra D] [PartialOrder D]    (τ : TracialState D) (a : D) : ℝ :=  Real.sqrt (τ.functional (star a * a)).reend CurrentMainsectionopen Filteropen scoped Topology NNReal ENNRealabbrev Pureness.ClosedStarIdeal := @_root_.OAI.Pureness.ClosedStarIdealnamespace Pureness.ClosedStarIdealsectionvariable {D : Type} [CStarAlgebra D] (J : ClosedStarIdeal D)abbrev Quotient := J.ideal.ringCon.Quotientdef quotientMap : D →ₐ[ℂ] J.Quotient := J.ideal.ringCon.mkₐ ℂinstance quotientStar : Star (J.Quotient) where  star := Quotient.map' star (by    intro u v h    change J.ideal.ringCon u v at h    change J.ideal.ringCon (star u) (star v)    rw [TwoSidedIdeal.rel_iff] at h ⊢    simpa only [star_sub] using J.star_mem h)instance quotientStarRing : StarRing (J.Quotient) where  star_involutive x := Quotient.inductionOn' x (fun u => congrArg J.quotientMap (star_star u))  star_mul x y := Quotient.inductionOn₂' x y (fun u v => congrArg J.quotientMap (star_mul u v))  star_add x y := Quotient.inductionOn₂' x y (fun u v => congrArg J.quotientMap (star_add u v))instance quotientStarModule : StarModule ℂ (J.Quotient) where  star_smul c x := Quotient.inductionOn' x (fun u => congrArg J.quotientMap (star_smul c u))abbrev idealSubmodule : Submodule ℂ (D) :=  (J.quotientMap).toLinearMap.kerinstance idealSubmodule_closed : IsClosed (J.idealSubmodule : Set D) := by  have he : (J.idealSubmodule : Set D) = (J.ideal : Set D) := by    ext u    change J.ideal.ringCon.mk' u = J.ideal.ringCon.mk' 0 ↔ u ∈ J.ideal    exact Quotient.eq  rw [he]  exact J.isCloseddef quotientLinearEquiv :    (D ⧸ J.idealSubmodule) ≃ₗ[ℂ] J.Quotient :=  (J.quotientMap).toLinearMap.quotKerEquivOfSurjective ((J.ideal.ringCon.mkₐ_surjective (α := ℂ)))instance quotientNormedAddCommGroup : NormedAddCommGroup (J.Quotient) :=  NormedAddCommGroup.induced _ _ (J.quotientLinearEquiv).symm    (J.quotientLinearEquiv).symm.injectiveinstance quotientNormedSpace : NormedSpace ℂ (J.Quotient) :=  NormedSpace.induced ℂ _ _ (J.quotientLinearEquiv).symmdef quotientNormEquiv : J.Quotient ≃ₗᵢ[ℂ]    (D ⧸ J.idealSubmodule) where  __ := (J.quotientLinearEquiv).symm  norm_map' _ := rflinstance quotientCompleteSpace : CompleteSpace (J.Quotient) :=  (J.quotientNormEquiv).toIsometryEquiv.completeSpace_iff.mpr inferInstanceclass NormConstruction : Prop where  mul_le : ∀ {D : Type} [CStarAlgebra D] (J : ClosedStarIdeal D) (x y : J.Quotient),    ‖x*y‖ ≤ ‖x‖*‖y‖  star_eq : ∀ {D : Type} [CStarAlgebra D] (J : ClosedStarIdeal D) (x : J.Quotient),    ‖star x‖ = ‖x‖  square_le : ∀ {D : Type} [CStarAlgebra D] [PartialOrder D] [StarOrderedRing D]    (J : ClosedStarIdeal D) (x : J.Quotient), ‖x‖ * ‖x‖ ≤ ‖star x * x‖variable [ComparatorModel.Pureness.ClosedStarIdeal.NormConstruction]instance quotientNormedRing : NormedRing (J.Quotient) where  dist_eq := dist_eq_norm_neg_add  norm_mul_le := NormConstruction.mul_le Jinstance quotientNormedAlgebra : NormedAlgebra ℂ (J.Quotient) where  norm_smul_le := norm_smul_leinstance quotientNormedStarGroup : NormedStarGroup (J.Quotient) where  norm_star_le x := (NormConstruction.star_eq J x).leendopen Filteropen scoped Topology NNReal ENNRealvariable {D : Type} [CStarAlgebra D] [PartialOrder D] [StarOrderedRing D]variable (J : ClosedStarIdeal D)variable [ComparatorModel.Pureness.ClosedStarIdeal.NormConstruction]instance quotientCStarAlgebra : CStarAlgebra (J.Quotient) where  norm_mul_self_le := NormConstruction.square_le Jend Pureness.ClosedStarIdealendsectionopen _root_.OAI.ComparatorModel.Purenesssection UniformTraceNormvariable {D : Type} {I : Type} [CStarAlgebra D] [PartialOrder D] [StarOrderedRing D]variable (τ : I → TracialState D) [Nonempty I]variable [ComparatorModel.Pureness.ClosedStarIdeal.NormConstruction]def CurrentMain.familyTwoNorm (a : D) : ℝ := ⨆ i, traceTwoNorm (τ i) aend UniformTraceNormopen _root_.OAI.ComparatorModel.Pureness Filteropen scoped Topology NNReal ENNRealvariable [ComparatorModel.Pureness.ClosedStarIdeal.NormConstruction]instance CurrentMain.boundedFamilyProductCStar {X : Type} {D : Type} [CStarAlgebra D] [Nontrivial D] :    CStarAlgebra (lp (fun _ : X => D) ∞) wheresection UniformNullvariable {D : Type} {I : Type} {X : Type} [CStarAlgebra D] [PartialOrder D] [StarOrderedRing D]variable (τ : I → TracialState D) [Nonempty I]def CurrentMain.IsFamilyNull (F : Filter X) (u : X → D) : Prop :=  Tendsto (fun n => familyTwoNorm τ (u n)) F (𝓝 0)class CurrentMain.NullConstruction : Prop where  zero : ∀ {D I X : Type} [CStarAlgebra D] [PartialOrder D] [StarOrderedRing D] (τ : I → Pureness.TracialState D) [Nonempty I]    (F : Filter X), IsFamilyNull τ F (fun _ => 0)  add : ∀ {D I X : Type} [CStarAlgebra D] [PartialOrder D] [StarOrderedRing D] (τ : I → Pureness.TracialState D) [Nonempty I]    {F : Filter X} {u v : X → D}, IsFamilyNull τ F u → IsFamilyNull τ F v →    IsFamilyNull τ F (fun n => u n + v n)  neg : ∀ {D I X : Type} [CStarAlgebra D] [PartialOrder D] [StarOrderedRing D] (τ : I → Pureness.TracialState D) [Nonempty I]    {F : Filter X} {u : X → D}, IsFamilyNull τ F u → IsFamilyNull τ F (fun n => -u n)  star : ∀ {D I X : Type} [CStarAlgebra D] [PartialOrder D] [StarOrderedRing D] (τ : I → Pureness.TracialState D) [Nonempty I]    {F : Filter X} {u : X → D}, IsFamilyNull τ F u → IsFamilyNull τ F (fun n => star (u n))  mul_left : ∀ {D I X : Type} [CStarAlgebra D] [PartialOrder D] [StarOrderedRing D] (τ : I → Pureness.TracialState D) [Nonempty I]    {F : Filter X} {u v : X → D}, IsFamilyNull τ F v → ∀ {M : ℝ},    (∀ n, ‖u n‖ ≤ M) → IsFamilyNull τ F (fun n => u n * v n)  mul_right : ∀ {D I X : Type} [CStarAlgebra D] [PartialOrder D] [StarOrderedRing D] (τ : I → Pureness.TracialState D) [Nonempty I]    {F : Filter X} {u v : X → D}, IsFamilyNull τ F u → ∀ {M : ℝ},    (∀ n, ‖v n‖ ≤ M) → IsFamilyNull τ F (fun n => u n * v n)  closed : ∀ {D I X : Type} [CStarAlgebra D] [PartialOrder D] [StarOrderedRing D] (τ : I → Pureness.TracialState D) [Nonempty I] (F : Filter X),    IsClosed {u : lp (fun _ : X => D) ∞ | IsFamilyNull τ F (fun n => u n)}variable [Nontrivial D]variable [ComparatorModel.CurrentMain.NullConstruction]def CurrentMain.familyNullTwoSided (F : Filter X) : TwoSidedIdeal (lp (fun _ : X => D) ∞) :=  TwoSidedIdeal.mk' {u | IsFamilyNull τ F (fun n => u n)}    (NullConstruction.zero τ F)    (fun hu hv => NullConstruction.add τ hu hv)    (fun hu => NullConstruction.neg τ hu)    (fun {u _} hv => NullConstruction.mul_left τ hv      (lp.norm_apply_le_norm ENNReal.top_ne_zero u))    (fun {_ v} hu => NullConstruction.mul_right τ hu      (lp.norm_apply_le_norm ENNReal.top_ne_zero v))def CurrentMain.familyNullIdeal (F : Filter X) : ClosedStarIdeal (lp (fun _ : X => D) ∞) where  ideal := familyNullTwoSided τ F  star_mem := by    intro u hu    apply (TwoSidedIdeal.mem_mk' _ _ _ _ _ _ (star u)).mpr    exact NullConstruction.star τ ((TwoSidedIdeal.mem_mk' _ _ _ _ _ _ u).mp hu)  isClosed := by    have he : (familyNullTwoSided τ F : Set (lp (fun _ : X => D) ∞)) =        {u | IsFamilyNull τ F (fun n => u n)} := by      ext u      exact TwoSidedIdeal.mem_mk' _ _ _ _ _ _ u    rw [he]    exact NullConstruction.closed τ Fend UniformNullvariable {D : Type} {I : Type} [CStarAlgebra D] [PartialOrder D] [StarOrderedRing D]variable (τ : I → TracialState D) [Nonempty I]variable [ComparatorModel.CurrentMain.NullConstruction]def CurrentMain.IsFamilyCauchy (u : ℕ → D) : Prop :=  IsFamilyNull τ (atTop : Filter (ℕ × ℕ)) (fun p => u p.1 - u p.2)class CurrentMain.CauchyConstruction : Prop where  const : ∀ {D I : Type} [CStarAlgebra D] [PartialOrder D] [StarOrderedRing D]    (τ : I → Pureness.TracialState D) [Nonempty I] (a : D), IsFamilyCauchy τ (fun _ => a)  add : ∀ {D I : Type} [CStarAlgebra D] [PartialOrder D] [StarOrderedRing D]    (τ : I → Pureness.TracialState D) [Nonempty I] {u v : ℕ → D},    IsFamilyCauchy τ u → IsFamilyCauchy τ v → IsFamilyCauchy τ (fun n => u n+v n)  star : ∀ {D I : Type} [CStarAlgebra D] [PartialOrder D] [StarOrderedRing D]    (τ : I → Pureness.TracialState D) [Nonempty I] {u : ℕ → D},    IsFamilyCauchy τ u → IsFamilyCauchy τ (fun n => star (u n))  mul : ∀ {D I : Type} [CStarAlgebra D] [PartialOrder D] [StarOrderedRing D]    (τ : I → Pureness.TracialState D) [Nonempty I] {u v : ℕ → D},    IsFamilyCauchy τ u → IsFamilyCauchy τ v → ∀ {M N : ℝ},    (∀ n, ‖u n‖ ≤ M) → (∀ n, ‖v n‖ ≤ N) → IsFamilyCauchy τ (fun n => u n*v n)  closed : ∀ {D I : Type} [CStarAlgebra D] [PartialOrder D] [StarOrderedRing D]    (τ : I → Pureness.TracialState D) [Nonempty I] [Nontrivial D],    IsClosed {u : lp (fun _ : ℕ => D) ∞ | IsFamilyCauchy τ (fun n => u n)}variable [Nontrivial D]variable [ComparatorModel.CurrentMain.CauchyConstruction]def CurrentMain.familyCauchyAlgebra : StarSubalgebra ℂ (lp (fun _ : ℕ => D) ∞) where  carrier := {u | IsFamilyCauchy τ (fun n => u n)}  zero_mem' := CauchyConstruction.const τ 0  one_mem' := CauchyConstruction.const τ 1  add_mem' hu hv := CauchyConstruction.add τ hu hv  mul_mem' {u v} hu hv := CauchyConstruction.mul τ hu hv    (lp.norm_apply_le_norm ENNReal.top_ne_zero u)    (lp.norm_apply_le_norm ENNReal.top_ne_zero v)  algebraMap_mem' z := CauchyConstruction.const τ (algebraMap ℂ D z)  star_mem' hu := CauchyConstruction.star τ huinstance CurrentMain.familyCauchy_complete : CompleteSpace (familyCauchyAlgebra τ) :=  (CauchyConstruction.closed τ).completeSpace_coeinstance CurrentMain.familyCauchy_cstar : CStarAlgebra (familyCauchyAlgebra τ) wheredef CurrentMain.familyCauchyNullIdeal : ClosedStarIdeal (familyCauchyAlgebra τ) where  ideal := TwoSidedIdeal.comap (familyCauchyAlgebra τ).val.toRingHom    (familyNullIdeal τ atTop).ideal  star_mem := by    intro u hu    apply (familyNullIdeal τ atTop).star_mem hu  isClosed := by    exact (familyNullIdeal τ atTop).isClosed.preimage      (continuous_subtype_val : Continuous (fun u : familyCauchyAlgebra τ => u.1))abbrev CurrentMain.UniformTracialCompletion := (familyCauchyNullIdeal τ).Quotientendsectionopen scoped ComplexOrdervariable {D : Type} [CStarAlgebra D] [PartialOrder D] [StarOrderedRing D]variable [ComparatorModel.Pureness.ClosedStarIdeal.NormConstruction] [ComparatorModel.CurrentMain.NullConstruction] [ComparatorModel.CurrentMain.CauchyConstruction]instance Pureness.ClosedStarIdeal.quotientOrder (J : ClosedStarIdeal D) : PartialOrder J.Quotient :=  CStarAlgebra.spectralOrder _instance Pureness.ClosedStarIdeal.quotientStarOrdered (J : ClosedStarIdeal D) : StarOrderedRing J.Quotient :=  CStarAlgebra.spectralOrderedRing _variable (J : Pureness.ClosedStarIdeal D)variable (τ : Pureness.TracialState D) (hτ : ∀ a ∈ J.ideal, τ.functional a = 0)def Pureness.ClosedStarIdeal.descendedValue : J.Quotient → ℂ := Quotient.lift τ.functional (by  intro u v huv  change J.ideal.ringCon u v at huv  rw [TwoSidedIdeal.rel_iff] at huv  have h := hτ (u-v) huv  rw [map_sub, sub_eq_zero] at h  exact h)def Pureness.ClosedStarIdeal.descendedLinear : J.Quotient →ₗ[ℂ] ℂ where  toFun := J.descendedValue τ hτ  map_add' x y := Quotient.inductionOn₂' x y (fun u v => τ.functional.map_add u v)  map_smul' c x := Quotient.inductionOn' x (fun u => τ.functional.map_smul c u)def Pureness.ClosedStarIdeal.descendedTrace : TracialState J.Quotient where  functional := { J.descendedLinear τ hτ with    monotone' := by      intro x y hxy      apply sub_nonneg.mp      change 0 ≤ J.descendedLinear τ hτ y - J.descendedLinear τ hτ x      rw [← map_sub]      obtain ⟨z,hz⟩ := CStarAlgebra.nonneg_iff_eq_star_mul_self.mp (sub_nonneg.mpr hxy)      rw [hz]      induction z using Quotient.inductionOn' with      | h u => exact τ.functional.map_nonneg (star_mul_self_nonneg u) }  normalized := τ.normalized  tracial x y := Quotient.inductionOn₂' x y (fun u v => τ.tracial u v)endsectionopen _root_.OAI.ComparatorModel.Pureness Filteropen scoped Topology NNReal ENNReal ComplexOrdersection UltraTracevariable {D : Type} {X : Type} [CStarAlgebra D] [PartialOrder D] [StarOrderedRing D] [Nontrivial D]variable (θ : X → TracialState D) (U : Ultrafilter X)variable [ComparatorModel.Pureness.ClosedStarIdeal.NormConstruction] [ComparatorModel.CurrentMain.NullConstruction] [ComparatorModel.CurrentMain.CauchyConstruction]instance CurrentMain.boundedFamilyProductOrder : PartialOrder (lp (fun _ : X => D) ∞) :=  CStarAlgebra.spectralOrder _instance CurrentMain.boundedFamilyProductStarOrdered : StarOrderedRing (lp (fun _ : X => D) ∞) :=  CStarAlgebra.spectralOrderedRing _def CurrentMain.ultraTraceValue (u : lp (fun _ : X => D) ∞) : ℂ :=  limUnder (U : Filter X) (fun n => (θ n).functional (u n))class CurrentMain.LimitConstruction : Prop where  tendsto : ∀ {D X : Type} [CStarAlgebra D] [PartialOrder D] [StarOrderedRing D]    (θ : X → Pureness.TracialState D) (U : Ultrafilter X) (u : lp (fun _ : X => D) ∞),    Tendsto (fun n => (θ n).functional (u n)) (U : Filter X) (𝓝 (ultraTraceValue θ U u))variable [ComparatorModel.CurrentMain.LimitConstruction]def CurrentMain.ultraTraceLinear : lp (fun _ : X => D) ∞ →ₗ[ℂ] ℂ where  toFun := ultraTraceValue θ U  map_add' u v := by    apply tendsto_nhds_unique (LimitConstruction.tendsto θ U (u+v))    simpa only [lp.coeFn_add, Pi.add_apply, map_add] using      (LimitConstruction.tendsto θ U u).add (LimitConstruction.tendsto θ U v)  map_smul' z u := by    apply tendsto_nhds_unique (LimitConstruction.tendsto θ U (z • u))    simpa only [lp.coeFn_smul, Pi.smul_apply, map_smul, RingHom.id_apply, smul_eq_mul] using      (LimitConstruction.tendsto θ U u).const_mul zdef CurrentMain.boundedFamilyEval (n : X) : lp (fun _ : X => D) ∞ →⋆ₐ[ℂ] D where  toFun u := u n  map_zero' := rfl  map_one' := rfl  map_add' _ _ := rfl  map_mul' _ _ := rfl  commutes' _ := rfl  map_star' _ := rfldef CurrentMain.ultraTrace : TracialState (lp (fun _ : X => D) ∞) where  functional := { ultraTraceLinear θ U with    monotone' := by      intro u v huv      exact le_of_tendsto_of_tendsto (LimitConstruction.tendsto θ U u)        (LimitConstruction.tendsto θ U v) (Eventually.of_forall (fun n =>          (θ n).functional.monotone (map_rel (boundedFamilyEval n) huv))) }  normalized := by    apply tendsto_nhds_unique (LimitConstruction.tendsto θ U 1)    have he (n : X) : (θ n).functional ((1 : lp (fun _ : X => D) ∞) n) = 1 :=      (θ n).normalized    simp only [he]    exact tendsto_const_nhds  tracial u v := by    change ultraTraceValue θ U (u*v) = ultraTraceValue θ U (v*u)    apply tendsto_nhds_unique (LimitConstruction.tendsto θ U (u*v))    have he (n : X) : (θ n).functional ((u*v) n) = (θ n).functional ((v*u) n) :=      (θ n).tracial (u n) (v n)    simpa only [he] using LimitConstruction.tendsto θ U (v*u)end UltraTracesection UniformQuotientvariable {D : Type} {I : Type} {X : Type} [CStarAlgebra D] [PartialOrder D] [StarOrderedRing D] [Nontrivial D]variable (τ : I → TracialState D) [Nonempty I] (U : Ultrafilter X)variable [ComparatorModel.Pureness.ClosedStarIdeal.NormConstruction] [ComparatorModel.CurrentMain.NullConstruction] [ComparatorModel.CurrentMain.CauchyConstruction] [ComparatorModel.CurrentMain.LimitConstruction]abbrev CurrentMain.FamilyUltrapower := (familyNullIdeal τ (U : Filter X)).Quotientclass CurrentMain.TraceConstruction : Prop where  null : ∀ {D I X : Type} [CStarAlgebra D] [PartialOrder D] [StarOrderedRing D] [Nontrivial D] (τ : I → Pureness.TracialState D) [Nonempty I]    (U : Ultrafilter X) (s : X → I) (u : lp (fun _ : X => D) ∞),    IsFamilyNull τ (U : Filter X) (fun n => u n) →      (ultraTrace (fun n => τ (s n)) U).functional u = 0variable [ComparatorModel.CurrentMain.TraceConstruction]def CurrentMain.familyLimitTrace (s : X → I) : TracialState (FamilyUltrapower τ U) :=  (familyNullIdeal τ (U : Filter X)).descendedTrace    (ultraTrace (fun n => τ (s n)) U) (fun u hu => by      apply TraceConstruction.null τ U s u      have he : u ∈ familyNullTwoSided τ (U : Filter X) ↔          IsFamilyNull τ (U : Filter X) (fun n => u n) := by        unfold familyNullTwoSided        exact TwoSidedIdeal.mem_mk' _ _ _ _ _ _ u      exact he.mp hu)end UniformQuotientsection PullbackTracevariable {D : Type} {E : Type} [CStarAlgebra D] [PartialOrder D] [StarOrderedRing D]variable [CStarAlgebra E] [PartialOrder E] [StarOrderedRing E]variable [ComparatorModel.Pureness.ClosedStarIdeal.NormConstruction] [ComparatorModel.CurrentMain.NullConstruction] [ComparatorModel.CurrentMain.CauchyConstruction] [ComparatorModel.CurrentMain.LimitConstruction] [ComparatorModel.CurrentMain.TraceConstruction]def CurrentMain.pullbackTrace (τ : TracialState E) (ι : D →⋆ₐ[ℂ] E) : TracialState D where  functional := { τ.functional.toLinearMap.comp ι.toLinearMap with    monotone' := fun _ _ h => τ.functional.monotone (map_rel ι h) }  normalized := by change τ.functional (ι 1) = 1; rw [map_one, τ.normalized]  tracial x y := by    change τ.functional (ι (x*y)) = τ.functional (ι (y*x))    rw [map_mul ι x y, map_mul ι y x]    exact τ.tracial _ _end PullbackTracesection CompletionTracesvariable {D : Type} {I : Type} [CStarAlgebra D] [PartialOrder D] [StarOrderedRing D]variable [Nontrivial D] (τ : I → TracialState D) [Nonempty I]variable [ComparatorModel.Pureness.ClosedStarIdeal.NormConstruction] [ComparatorModel.CurrentMain.NullConstruction] [ComparatorModel.CurrentMain.CauchyConstruction] [ComparatorModel.CurrentMain.LimitConstruction] [ComparatorModel.CurrentMain.TraceConstruction]instance CurrentMain.familyCauchyOrder : PartialOrder (familyCauchyAlgebra τ) :=  CStarAlgebra.spectralOrder _instance CurrentMain.familyCauchyStarOrdered : StarOrderedRing (familyCauchyAlgebra τ) :=  CStarAlgebra.spectralOrderedRing _def CurrentMain.cauchyTrace (i : I) : TracialState (familyCauchyAlgebra τ) :=  pullbackTrace (ultraTrace (fun _ : ℕ => τ i) (Ultrafilter.of atTop))    (familyCauchyAlgebra τ).subtypedef CurrentMain.completionTrace (i : I) : TracialState (UniformTracialCompletion τ) :=  (familyCauchyNullIdeal τ).descendedTrace (cauchyTrace τ i) (fun u hu => by    apply TraceConstruction.null τ (Ultrafilter.of atTop) (fun _ => i) u.1    have he : u.1 ∈ familyNullTwoSided τ atTop ↔        IsFamilyNull τ atTop (fun n => u.1 n) := by      unfold familyNullTwoSided      exact TwoSidedIdeal.mem_mk' _ _ _ _ _ _ u.1    have hn : IsFamilyNull τ atTop (fun n => u.1 n) := he.mp hu    exact hn.mono_left (Ultrafilter.of_le atTop))def CurrentMain.boundedFamilyConstant {X : Type} (a : D) : lp (fun _ : X => D) ∞ :=  ⟨fun _ => a, memℓp_infty_iff.mpr ⟨‖a‖,by rintro _ ⟨n,rfl⟩; exact le_rfl⟩⟩instance CurrentMain.completionNontrivial : Nontrivial (UniformTracialCompletion τ) := by  obtain ⟨i⟩ := ‹Nonempty I›  refine ⟨⟨1,0,?_⟩⟩  intro h  have he := congrArg (completionTrace τ i).functional h  rw [(completionTrace τ i).normalized, map_zero] at he  exact one_ne_zero heend CompletionTracesvariable {D : Type} {I : Type} {X : Type} [CStarAlgebra D] [PartialOrder D] [StarOrderedRing D]variable [Nontrivial D] (τ : I → TracialState D) [Nonempty I] (U : Ultrafilter X)variable [ComparatorModel.Pureness.ClosedStarIdeal.NormConstruction] [ComparatorModel.CurrentMain.NullConstruction] [ComparatorModel.CurrentMain.CauchyConstruction] [ComparatorModel.CurrentMain.LimitConstruction] [ComparatorModel.CurrentMain.TraceConstruction]def CurrentMain.familyUltrapowerMap : D →⋆ₐ[ℂ] FamilyUltrapower τ U where  toFun a := (familyNullIdeal τ (U : Filter X)).quotientMap (boundedFamilyConstant a)  map_zero' := (familyNullIdeal τ (U : Filter X)).quotientMap.map_zero  map_one' := (familyNullIdeal τ (U : Filter X)).quotientMap.map_one  map_add' a b := (familyNullIdeal τ (U : Filter X)).quotientMap.map_add    (boundedFamilyConstant a) (boundedFamilyConstant b)  map_mul' a b := (familyNullIdeal τ (U : Filter X)).quotientMap.map_mul    (boundedFamilyConstant a) (boundedFamilyConstant b)  commutes' z := (familyNullIdeal τ (U : Filter X)).quotientMap.commutes z  map_star' _a := rflendsectionopen Filter Topologyvariable {A : Type uA} [NormedRing A]variable [ComparatorModel.Pureness.ClosedStarIdeal.NormConstruction] [ComparatorModel.CurrentMain.NullConstruction] [ComparatorModel.CurrentMain.CauchyConstruction] [ComparatorModel.CurrentMain.LimitConstruction] [ComparatorModel.CurrentMain.TraceConstruction]def Pureness.TopologicallySimple (A : Type uA) [NormedRing A] : Prop :=  ∀ I : TwoSidedIdeal A, IsClosed (I : Set A) → I = ⊥ ∨ I = ⊤endsectionopen _root_.OAI.ComparatorModel.Pureness Filtervariable [ComparatorModel.Pureness.ClosedStarIdeal.NormConstruction] [ComparatorModel.CurrentMain.NullConstruction] [ComparatorModel.CurrentMain.CauchyConstruction] [ComparatorModel.CurrentMain.LimitConstruction] [ComparatorModel.CurrentMain.TraceConstruction]def CurrentMain.StablyFinite (A : Type uA) [CStarAlgebra A] : Prop :=  ∀ n : ℕ, ∀ v : CStarMatrix (Fin n) (Fin n) A,    star v*v = 1 → v*star v = 1def CurrentMain.UniformPropertyGammaAt (A : Type) [CStarAlgebra A]    [PartialOrder A] [StarOrderedRing A] [Nontrivial A]    [Nonempty (TracialState A)] (U : Ultrafilter ℕ) : Prop :=  ∃ p : FamilyUltrapower (completionTrace (fun τ : TracialState A => τ)) U,    IsStarProjection p ∧ ∀ x : UniformTracialCompletion (fun τ : TracialState A => τ),      p * familyUltrapowerMap (completionTrace (fun τ : TracialState A => τ)) U x =        familyUltrapowerMap (completionTrace (fun τ : TracialState A => τ)) U x * p ∧      ∀ s : ℕ → TracialState A,        (familyLimitTrace (completionTrace (fun τ : TracialState A => τ)) U s).functional          (p * familyUltrapowerMap (completionTrace (fun τ : TracialState A => τ)) U x) =        (1/2 : ℂ) *        (familyLimitTrace (completionTrace (fun τ : TracialState A => τ)) U s).functional          (familyUltrapowerMap (completionTrace (fun τ : TracialState A => τ)) U x)open _root_.OAI.ComparatorModel.Pureness Filterdef CurrentMain.Statement : Prop := ∀    {A : Type} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]    [Nontrivial A] [TopologicalSpace.SeparableSpace A]    (_hsimple : TopologicallySimple A) (_hinf : ¬FiniteDimensional ℂ A)    (_hA : IsNuclear.{0, uNuclear} A) (_hfinite : StablyFinite A)    [Nonempty (TracialState A)] (U : Ultrafilter ℕ)    (_hfree : (U : Filter ℕ) ≤ atTop)    (_hRR : RealRankZero (FamilyUltrapower (completionTrace (fun τ : TracialState A => τ)) U)),    UniformPropertyGammaAt A Uenddef CurrentMain.MainClaim : Prop :=  ∃ h0 : ComparatorModel.Pureness.ClosedStarIdeal.NormConstruction, letI := h0;  ∃ h1 : ComparatorModel.CurrentMain.NullConstruction, letI := h1;  ∃ h2 : ComparatorModel.CurrentMain.CauchyConstruction, letI := h2;  ∃ h3 : ComparatorModel.CurrentMain.LimitConstruction, letI := h3;  ∃ h4 : ComparatorModel.CurrentMain.TraceConstruction, letI := h4;  Statement.{uNuclear}theorem CurrentMain.main : MainClaim.{uNuclear} := by  sorryend ComparatorModelendend OAI
Every extracted statement of the accompanying papers

The statements the atlas extracted automatically from each accompanying paper’s TeX source, with links to the full sources.

Tracial projection methods and uniform property Gamma

Theorem (Real rank zero and uniform property \Gamma)

Let A be a unital, separable, simple, infinite-dimensional, nuclear, stably finite C^*-algebra with T(A)\ne\varnothing, and let B=\overline A^{T(A)}. Fix any free ultrafilter \omega on \N. If B^\omega has real rank zero in its quotient C^*-norm, then there is a projection p\in B^\omega\cap B' such that

\lambda(px)=\tfrac12\lambda(x) \qquad(x\in B,\ \lambda\in\Lambda_\omega).

In particular, A has uniform property \Gamma.

Section 1, Introduction Read it in the paper TeX source, line 57
Show the TeX
Let $A$ be a unital, separable, simple, infinite-dimensional, nuclear,
stably finite $C^*$-algebra with $T(A)\ne\varnothing$, and let
$B=\overline A^{T(A)}$. Fix any free ultrafilter $\omega$ on $\N$.
If $B^\omega$ has real rank zero in its quotient $C^*$-norm, then there is
a projection $p\in B^\omega\cap B'$ such that
\[
 \lambda(px)=\tfrac12\lambda(x)
 \qquad(x\in B,\ \lambda\in\Lambda_\omega).
\]
In particular, $A$ has uniform property $\Gamma$.
Corollary (Traces on the completion)

Under the hypotheses of Theorem r:thm:main, including real rank zero of B^\omega in its quotient C^*-norm, every tracial state of B is the designated extension of a unique trace in T(A). Thus restriction is an affine homeomorphism T(B)\to T(A), with inverse \tau\mapsto\bar\tau. Moreover,

|\sigma(b)|\le\|b\|_{2,T(A)} \qquad(b\in B,\ \sigma\in T(B)),

so every tracial state of B is continuous for the designated uniform 2-norm.

Section 1, Introduction Read it in the paper TeX source, line 123
Show the TeX
Under the hypotheses of Theorem~\ref{r:thm:main}, including real rank zero
of $B^\omega$ in its quotient $C^*$-norm, every tracial state of $B$ is
the designated extension of a unique trace in $T(A)$. Thus restriction
is an affine homeomorphism $T(B)\to T(A)$, with inverse
$\tau\mapsto\bar\tau$. Moreover,
\[
 |\sigma(b)|\le\|b\|_{2,T(A)}
 \qquad(b\in B,\ \sigma\in T(B)),
\]
so every tracial state of $B$ is continuous for the designated uniform
$2$-norm.
Theorem (Finite-set central splitting)

Let A\subseteq D be a unital inclusion of C^*-algebras, with A nuclear, D of real rank zero, and T(D)\ne\varnothing. Suppose that for every \delta>0 there is a full projection g\in D with \sup_{\tau\in T(D)}\tau(g)<\delta. For every finite K\subseteq\mathcal U(A) and \varepsilon>0 there is a projection P\in D such that, for every x\in K,

\sup_{\tau\in T(D)}\|[P,x]\|_{2,\tau}<\varepsilon, \qquad \sup_{\tau\in T(D)}|\tau(Px)-\tfrac12\tau(x)|<\varepsilon.
Section 1, Introduction Read it in the paper TeX source, line 143
Show the TeX
Let $A\subseteq D$ be a unital inclusion of $C^*$-algebras, with $A$ nuclear,
$D$ of real rank zero, and $T(D)\ne\varnothing$. Suppose that for every
$\delta>0$ there is a full projection $g\in D$ with
$\sup_{\tau\in T(D)}\tau(g)<\delta$.
For every finite $K\subseteq\mathcal U(A)$ and $\varepsilon>0$ there is a
projection $P\in D$ such that, for every $x\in K$,
\[
 \sup_{\tau\in T(D)}\|[P,x]\|_{2,\tau}<\varepsilon,
 \qquad
 \sup_{\tau\in T(D)}|\tau(Px)-\tfrac12\tau(x)|<\varepsilon.
\]
Theorem (The direct unital comparison route)

Let A be a simple, separable, unital, infinite-dimensional nuclear C^*-algebra with strict comparison in the preceding sense. Then A\cong A\otimes\Z. When T(A)\ne\varnothing, the proof constructs uniform property \Gamma directly.

Section 1, Introduction Read it in the paper TeX source, line 207
Show the TeX
Let $A$ be a simple, separable, unital, infinite-dimensional nuclear
$C^*$-algebra with strict comparison in the preceding sense.
Then $A\cong A\otimes\Z$. When $T(A)\ne\varnothing$, the proof constructs
uniform property $\Gamma$ directly.
Theorem (The direct stably projectionless route)

Let A be a nonzero simple, separable, nuclear C^*-algebra such that A\otimes\K has no nonzero projections. Suppose that every trace in T_{\mathrm{lsc}}(A) is bounded on the positive unit ball and that T_1(A) is nonempty and weak-* compact. Assume that, for a,b\in(A\otimes\K)_+ with b\ne0,

d_\tau(a)<1\quad \text{for every }\tau\in T_{\mathrm{lsc}}(A) \text{ with }d_\tau(b)=1 \quad\Longrightarrow\quad a\precsim b.

Then A has uniform property \Gamma and A\cong A\otimes\Z.

Section 1, Introduction Read it in the paper TeX source, line 237
Show the TeX
Let $A$ be a nonzero simple, separable, nuclear $C^*$-algebra such that
$A\otimes\K$ has no nonzero projections. Suppose that every trace in
$T_{\mathrm{lsc}}(A)$ is bounded on the positive unit ball and that
$T_1(A)$ is nonempty and weak-$*$ compact. Assume that, for
$a,b\in(A\otimes\K)_+$ with $b\ne0$,
\[
 d_\tau(a)<1\quad
 \text{for every }\tau\in T_{\mathrm{lsc}}(A)
 \text{ with }d_\tau(b)=1
 \quad\Longrightarrow\quad a\precsim b.
\]
Then $A$ has uniform property $\Gamma$ and $A\cong A\otimes\Z$.
Configuration and file facts
OpenAI’s Lean catalogue
OpenAI lists this as a main result in its Lean catalogue.
Allowed axioms
propext, Quot.sound, Classical.choiceThe axioms this configuration allows a proof to use. A replay shows which of them a proof uses.
Imports
Mathlib
Imports from outside Mathlib
None
Local vocabulary
67 local vocabulary declarations
Lines of Lean, without comments or blank lines
331
Second proof-verification program (nanoda)
Off in OpenAI's configuration.

Statement comparison

A shareable summary of this page: the proposed paper match, what the Lean statement expresses, and which reviews are recorded.

Plectis Atlas

Uniform property $\Gamma$ from tracial real rank zero

Family 291: Cuntz comparison, nuclear dimension, and equivariant Jiang–Su stability

Candidate pairing

Theorem (Real rank zero and uniform property \Gamma)

Let A be a unital, separable, simple, infinite-dimensional, nuclear, stably finite C^*-algebra with T(A)\ne\varnothing, and let B=\overline A^{T(A)}. Fix any free ultrafilter \omega on \N. If B^\omega has real rank zero in its quotient C^*-norm, then there is a projection p\in B^\omega\cap B' such that

\lambda(px)=\tfrac12\lambda(x) \qquad(x\in B,\ \lambda\in\Lambda_\omega).

In particular, A has uniform property \Gamma.

Tracial projection methods and uniform property Gamma

TeX label r:thm:main, build/sections/01_introduction.tex, line 57

The Lean statement says

theorem CurrentMain.main : MainClaim.{uNuclear} := by  sorry

A Lean statement states the theorem and leaves its proof as sorry on purpose. OpenAI’s proof is in a separate solution module, and a program called Comparator checks that proof against this statement.

Atlas selected this possible match because the two statements share words. No review of whether they mean the same thing is recorded.three independent groups report that Comparator accepted runs for this file at the release version shown here.Statement review: none recorded

67 local vocabulary declarationsAllowed axioms: propext, Quot.sound, Classical.choiceopenai/math at fd4aeebwcook04.github.io/plectis-atlas/statements/UniformGamma.html

Recorded comparisons with the paper

Atlas records no contributed comparison of this statement with the paper.

Contributed Comparator run reports

Atlas records no contributed report of running Comparator for this statement file.

More about this statement

  • Commentary The headline claims equivariant Jiang-Su stability and the unital Toms-Winter conjecture, but only a real-rank-zero implication for uniform property Gamma is formalised. Robert Joseph George, Do the Lean statements in openai/math match their papers?, 2026-10-07 Source

Questions to resolve when comparing this statement with the paper

  • Both independent readers find this family's challenges state less than its headline, while the atlas's AI draft classes this file as stating a paper's theorem as the paper does; check which part of the headline it covers.

Compare this statement with the paperShare a Comparator run reportSuggest a change