TomitaGraphClosability.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Closability of the concrete Tomita graph

A separating vector is cyclic for the commutant. The commutant matrix coefficients then show that the closed graph has no vertical vector. This is the first operator-theoretic step toward modular spectral resolution.

theorem OAI.KadisonKastler.rescaledGraph_commutant_coefficient line 23
Source documentation
Commutant coefficients identify the second graph coordinate on the dense algebraic graph and, by continuity, on its closure.
```
theorem rescaledGraph_commutant_coefficient (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H) (c : ℝ)
    (b : Algebra M.commutant) (ξ : TomitaGraphHilbert H)
    (hξ : ξ ∈ rescaledGraphSubspace M J Ω c) :
    inner ℂ (J (b.val Ω)) (ξ 1) = (c : ℂ) * inner ℂ (star b.val Ω) (ξ 0) := by
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.TomitaGraphHilbert, OAI.KadisonKastler.rescaledGraphSubspace
theorem OAI.KadisonKastler.rescaledGraph_no_vertical line 47
Source documentation
The closure of the graph is single-valued whenever the vector separates M. No modular conjugation or spectral theorem is assumed.
```
theorem rescaledGraph_no_vertical (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H) (c : ℝ)
    (hsep : Function.Injective (algebraVectorMap M Ω))
    (ξ : TomitaGraphHilbert H) (hξ : ξ ∈ rescaledGraphSubspace M J Ω c)
    (hzero : ξ 0 = 0) : ξ = 0 := by
…
```
Mentions: OAI.KadisonKastler.algebraVectorMap, OAI.KadisonKastler.TomitaGraphHilbert, OAI.KadisonKastler.rescaledGraphSubspace
theorem OAI.KadisonKastler.rescaledGraph_first_injective line 74
Source documentation
Projection onto the first coordinate is injective on the closed graph.
```
theorem rescaledGraph_first_injective (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H) (c : ℝ)
    (hsep : Function.Injective (algebraVectorMap M Ω)) :
    Function.Injective (fun ξ : rescaledGraphSubspace M J Ω c => ξ.val 0) := by
…
```
Mentions: OAI.KadisonKastler.algebraVectorMap, OAI.KadisonKastler.rescaledGraphSubspace