ConditionalMain.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Uniform commutator estimates, hyperreflexivity, and similarity from central factor models and derivation implementation.

structure OAI.KadisonSimilarity.PublishedSeparableModel line 22
Source documentation
A central direct-integral model with separable Hilbert fibers and the finite or properly infinite factor structure.
```
structure PublishedSeparableModel (P : VonNeumannAlgebra H) where
…
```
structure OAI.KadisonSimilarity.PublishedUniformInputs line 41
Source documentation
Existence of central factor models for separable represented algebras.
```
structure PublishedUniformInputs : Prop where
…
```
theorem OAI.KadisonSimilarity.uniformCommutatorEstimate_of_published line 47
Source documentation
The universal matrix estimate with the manuscript's fixed constant.
```
theorem uniformCommutatorEstimate_of_published (inputs : PublishedUniformInputs.{u}) :
    UniformCommutatorEstimate.{u} universalConstant := by
…
```
Mentions: OAI.KadisonSimilarity.universalConstant
theorem OAI.KadisonSimilarity.universalCommutatorTheorem_of_published line 59
Source documentation
Theorem thm:universal, conditional only on the named published inputs.
```
theorem universalCommutatorTheorem_of_published (inputs : PublishedUniformInputs.{u}) :
    UniversalCommutatorTheorem.{u} :=
…
```
theorem OAI.KadisonSimilarity.similarityTheorem_sameUniverse_of_published line 67
Source documentation
Theorem thm:similarity, using Kirchberg's criterion after the proved bounded-derivation implementation. The canonical spectral order introduces no restriction on the C-star algebra.
```
theorem similarityTheorem_sameUniverse_of_published (inputs : PublishedUniformInputs.{u})
    (kirchberg : ∀ (A : Type u) [CStarAlgebra A], KirchbergDerivationCriterion.{u,u} A) :
    SimilarityTheorem.{u,u} := by
…
```
theorem OAI.KadisonSimilarity.similarityTheorem_of_published line 80
Source documentation
The full similarity statement, with unrelated source and Hilbert-space universes. The published faithful-representation criterion is used only in one common universe containing both; the actual implementing operator is then transported back.
```
theorem similarityTheorem_of_published
    (inputs : PublishedUniformInputs.{max u v})
    (kirchberg : ∀ (A : Type (max u v)) [CStarAlgebra A],
      KirchbergDerivationCriterion.{max u v, max u v} A) :
    SimilarityTheorem.{u,v} :=
…
```
theorem OAI.KadisonSimilarity.universalHyperreflexivity_of_published line 90
Source documentation
Corollary cor:hyperreflexivity, with the same universal constant and the commutant-distance formula now proved.
```
theorem universalHyperreflexivity_of_published (inputs : PublishedUniformInputs.{u}) :
    UniversalHyperreflexivity.{u} universalConstant := by
…
```
Mentions: OAI.KadisonSimilarity.universalConstant