UnconditionalMain.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform matrix commutator estimates and universal hyperreflexivity, with the numerical constant obtained from the factor estimates and central decomposition.

theorem OAI.KadisonSimilarity.uniformCommutatorEstimate line 15
Source documentation
The manuscript's uniform matrix commutator estimate, with no remaining published structural hypotheses.
```
theorem uniformCommutatorEstimate : UniformCommutatorEstimate.{u} universalConstant :=
…
```
Mentions: OAI.KadisonSimilarity.universalConstant
theorem OAI.KadisonSimilarity.universalCommutatorTheorem line 19
Source documentation
Theorem thm:universal of the manuscript.
Distinct definitions of this name: ComparatorChallenges/KadisonSimilarity.lean:107 (same statement text; different proof or body). Qualify references as OAI.KadisonSimilarity.universalCommutatorTheorem@path.
```
theorem universalCommutatorTheorem : UniversalCommutatorTheorem.{u} :=
…
```
theorem OAI.KadisonSimilarity.universalHyperreflexivity line 23
Source documentation
Corollary cor:hyperreflexivity of the manuscript.
Distinct definitions of this name: ComparatorChallenges/KadisonSimilarity.lean:111 (same statement text; different proof or body). Qualify references as OAI.KadisonSimilarity.universalHyperreflexivity@path.
```
theorem universalHyperreflexivity : UniversalHyperreflexivity.{u} universalConstant :=
…
```
Mentions: OAI.KadisonSimilarity.universalConstant
theorem OAI.KadisonSimilarity.similarityTheorem_of_kirchberg line 28
Source documentation
Kirchberg's derivation criterion and the universal commutator estimate imply similarity, with independent source and Hilbert universes.
```
theorem similarityTheorem_of_kirchberg
    (kirchberg : ∀ (A : Type (max u v)) [CStarAlgebra A],
      KirchbergDerivationCriterion.{max u v, max u v} A) : SimilarityTheorem.{u,v} :=
…
```