ModularCoreStability.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Completing modular graph stability by descent through the regular core

The source core belongs to the neighboring modular group. The tensor gap is proved from the same complete maps used for graph comparison and is propagated through the small action alignment.

structure OAI.KadisonKastler.ModularCorePublishedInputs line 32
Source documentation
The modular representation and source-core type are explicit hypotheses for descent through the regular core.
```
structure ModularCorePublishedInputs : Prop where
…
```
theorem OAI.KadisonKastler.uniform_modular_graph_strong_stability line 45

theorem OAI.KadisonKastler.uniform_modular_matrix_graph_strong_stability line 115

Source documentation

The same original-space conclusion under actual matrix unit-ball proximity. No global linear selection of approximants is required.

theorem uniform_modular_matrix_graph_strong_stability
    (h : ModularCorePublishedInputs.{u}) {B : ℝ} (hB : 0 ≤ B)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ δ : ℝ, 0 < δ ∧
      ∀ (H : Type u) [NormedAddCommGroup H] [InnerProductSpace ℂ H]
        [CompleteSpace H] [Nontrivial H] [TopologicalSpace.SeparableSpace H],
      ∀ (M N : VonNeumannAlgebra H), TypeIIIFactor M →
      ∀ (Ω : H) (_m : ModularSpectralResolution M Ω) (n : ModularSpectralResolution N Ω)
        (J : H ≃ₗᵢ⋆[ℂ] H),
      TypeIIInfinityFactor (regularCoreAlgebra n.group n.continuous N) →
      ∀ γ : ℝ, 0 < γ → γ < δ → kkDistance M N < γ →
      MatrixNearInclusion M N γ → MatrixNearInclusion N M γ →
…

Mentions: OAI.KadisonKastler.TypeIIIFactor, OAI.KadisonKastler.ModularSpectralResolution, OAI.KadisonKastler.TypeIIInfinityFactor, OAI.KadisonKastler.regularCoreAlgebra, OAI.KadisonKastler.kkDistance, OAI.KadisonKastler.MatrixNearInclusion