CentralFactorAssembly.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The factor alternatives are proved, including zero Hilbert fibers. Only the central decomposition itself remains a structural input here.

theorem OAI.KadisonSimilarity.publishedFactorCases_of_scalar_center line 17
theorem OAI.KadisonSimilarity.factorCommutatorEstimate line 41
Source documentation
The manuscript's factor-representation bound, with every local input proved.
```
theorem factorCommutatorEstimate
    (hfactor : ∀ a : P.toStarSubalgebra, (∀ b, a * b = b * a) →
      ∃ c : ℂ, a = algebraMap ℂ P.toStarSubalgebra c) :
    CommutatorEstimate P factorConstant :=
…
```
Mentions: OAI.KadisonSimilarity.CommutatorEstimate, OAI.KadisonSimilarity.factorConstant
def OAI.KadisonSimilarity.publishedSeparableModel_of_central_factors line 55
Source documentation
A central decomposition into actual factors suffices; no factor model or free-position hypothesis is required from the decomposition theorem.
```
def publishedSeparableModel_of_central_factors
    (D : CentralDecompositionData μ K P)
    (hfactor : ∀ᵐ a ∂μ, ∀ x : (D.algebra a).toStarSubalgebra,
      (∀ y, x * y = y * x) →
        ∃ z : ℂ, x = algebraMap ℂ (D.algebra a).toStarSubalgebra z) :
    PublishedSeparableModel P where
…
```
Mentions: OAI.KadisonSimilarity.CentralDecompositionData, OAI.KadisonSimilarity.PublishedSeparableModel