FactorAssembly.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The three factor branches

The finite branch records only the fixed trace, matrix presentation, and local published inputs used in the preceding application. The alternatives are the structural factor classification; no alternative assumes an operator estimate.

structure OAI.KadisonSimilarity.FiniteFactorModel line 30
Source documentation
The complete finite-factor presentation required for the application.
```
structure FiniteFactorModel (P : VonNeumannAlgebra H) where
…
```
theorem OAI.KadisonSimilarity.FiniteFactorModel.estimate line 64
Source documentation
Every finite presentation gives the concrete represented estimate.
```
theorem FiniteFactorModel.estimate [TopologicalSpace.SeparableSpace H]
    {P : VonNeumannAlgebra H} (F : FiniteFactorModel P) :
    CommutatorEstimate P (3 * cornerConstant + 2) := by
…
```
Mentions: OAI.KadisonSimilarity.FiniteFactorModel, OAI.KadisonSimilarity.CommutatorEstimate, OAI.KadisonSimilarity.cornerConstant
structure OAI.KadisonSimilarity.FiniteMatrixFactorModel line 81
Source documentation
The structural data of a finite type-I factor in its given representation.
```
structure FiniteMatrixFactorModel (P : VonNeumannAlgebra H) where
…
```
theorem OAI.KadisonSimilarity.FiniteMatrixFactorModel.estimate line 88
theorem OAI.KadisonSimilarity.CommutatorEstimate.mono line 94
Source documentation
Increasing the numerical constant preserves the same estimate.
```
theorem CommutatorEstimate.mono {P : VonNeumannAlgebra H} {c C : ℝ}
    (h : CommutatorEstimate P c) (hc : c ≤ C) : CommutatorEstimate P C := by
…
```
Mentions: OAI.KadisonSimilarity.CommutatorEstimate
def OAI.KadisonSimilarity.PublishedFactorCasesInput line 104
Source documentation
Precisely the factor alternatives needed downstream. The finite model is supplied by Popa's increasing-matrix subfactor theorem and the listed local inputs; the other two alternatives are projection/type classification.
```
def PublishedFactorCasesInput (P : VonNeumannAlgebra H) : Prop :=
…
```
theorem OAI.KadisonSimilarity.factor_estimate_of_published_cases line 109
Source documentation
All three structural alternatives yield the same fixed factor constant.
```
theorem factor_estimate_of_published_cases [TopologicalSpace.SeparableSpace H]
    (P : VonNeumannAlgebra H)
    (cases : PublishedFactorCasesInput P)
    (dickson : DicksonTwoBound (A := P) (RectangularSum H H)) :
…
```
Mentions: OAI.KadisonSimilarity.PublishedFactorCasesInput, OAI.KadisonSimilarity.DicksonTwoBound, OAI.KadisonSimilarity.RectangularSum