CentralBufferImage.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The central buffer commutes with both complete factor images

Generator density puts every constant factor element in the actual buffer commutant. Thus finite split data chosen in either factor inherit exact commutation; no extra centrality assumption on those data is needed.

lemma OAI.WeakPureInfiniteness.oInfinity_image_mem_centralizer line 23
Source documentation
Exact commutation on the canonical generators extends to the whole image of O∞ by its proved closed star-span density.
```
lemma oInfinity_image_mem_centralizer (f : OInfinity →⋆ₐ[ℂ] E) (r : ℕ → E)
    (hgen : ∀ i j, Commute (f (oInfinityIsometry i)) (r j) ∧
      Commute (star (f (oInfinityIsometry i))) (r j)) :
    ∀ x : OInfinity, f x ∈ StarSubalgebra.centralizer ℂ (Set.range r) := by
…
```
Mentions: OAI.WeakPureInfiniteness.OInfinity, OAI.WeakPureInfiniteness.oInfinityIsometry

lemma OAI.WeakPureInfiniteness.exists_normUltrapower_factor_buffer line 45

Source documentation

The already constructed third row centralizes every element of both constant O∞ factor images, including all finite vacuum-split data.

lemma exists_normUltrapower_factor_buffer [Nontrivial E]
    (U : Ultrafilter ℕ) [Fact ((U : Filter ℕ) ≤ atTop)]
    (f g : OInfinity →⋆ₐ[ℂ] E)
    (hfg : ∀ x y, Commute (f x) (g y)) :
    ∃ r : ℕ → NormUltra.QuotientAlgebra (fun _ : ℕ => E) U,
      (∀ i j, star (r i) * r j = if i = j then 1 else 0) ∧
      (∀ x : OInfinity, NormUltra.QuotientAlgebra.diagonalHom U (f x) ∈
        StarSubalgebra.centralizer ℂ (Set.range r)) ∧
      ∀ x : OInfinity, NormUltra.QuotientAlgebra.diagonalHom U (g x) ∈
        StarSubalgebra.centralizer ℂ (Set.range r) := by
…

Mentions: OAI.WeakPureInfiniteness.OInfinity, OAI.NormUltra.QuotientAlgebra, OAI.NormUltra.QuotientAlgebra.diagonalHom