CanonicalFreeCornerEstimate.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The original operator is recovered after applying the local free-corner argument in the actual generated GNS model. All generation, faithfulness, and compression requirements are proved here; the remaining local hypotheses are the explicitly cited published structural inputs.

def OAI.KadisonSimilarity.CanonicalSecondFrame line 48
Source documentation
The chosen closed-range proof is included inside this data type.
```
def CanonicalSecondFrame (b : ℝ) : Type _ := by
…
```
def OAI.KadisonSimilarity.canonicalGeneratedSmallFrame line 53
Source documentation
The fixed small frame transported into the actual free second factor.
```
def canonicalGeneratedSmallFrame {b : ℝ} (Q : SmallFreeCornerData τR.toLinearMap b) :
    CanonicalSecondFrame τB hB ω trB ψ hψ b := by
…
```
Mentions: OAI.KadisonSimilarity.SmallFreeCornerData, OAI.KadisonSimilarity.CanonicalSecondFrame
abbrev OAI.KadisonSimilarity.CanonicalFreeCornerInput line 64
Source documentation
Published local data on the exact canonical free-product model.
```
abbrev CanonicalFreeCornerInput {b : ℝ}
    (Q : CanonicalSecondFrame τB hB ω trB ψ hψ b)
    (x : B) (hxsq : x * x = 1) : Prop := by
…
```
Mentions: OAI.KadisonSimilarity.CanonicalSecondFrame

theorem OAI.KadisonSimilarity.canonicalFreeCornerInput_of_normal_source line 77

Source documentation

The generated-factor comparison used by the local application is proved from the normal source, rather than supplied independently.

theorem canonicalFreeCornerInput_of_normal_source
    (hω : (ω : Filter ℕ) ≤ Filter.cofinite)
    (hf : ScalarFree (quotientTrace τB hB ω trB).toLinearMap
      (constant τB hB ω trB).range ψ.range)
    (hsource : τR.gnsStarAlgHom.range =
      (representationVonNeumannAlgebra τR.gnsStarAlgHom).toStarSubalgebra)
    (hsize : Filter.Tendsto (fun j => (Fintype.card (I j) : ℝ)) Filter.atTop Filter.atTop)
    {b : ℝ} (Q : CanonicalSecondFrame τB hB ω trB ψ hψ b)
    (x : B) (hxsq : x * x = 1) :
    CanonicalFreeCornerInput τB τR hB ω trB ψ hψτ hψ M Q x hxsq := by
…

Mentions: OAI.KadisonSimilarity.ScalarFree, OAI.KadisonSimilarity.representationVonNeumannAlgebra, OAI.KadisonSimilarity.CanonicalSecondFrame, OAI.KadisonSimilarity.CanonicalFreeCornerInput

theorem OAI.KadisonSimilarity.original_symmetry_bound_of_free_corner line 98

Source documentation

A centered symmetry in the original finite algebra obeys the free-corner bound. The tested operator is the original GNS operator, not a separately chosen operator on a model.

theorem original_symmetry_bound_of_free_corner
    (hω : (ω : Filter ℕ) ≤ Filter.cofinite)
    (hD : ψ.range ≤ (Φ).range)
    (hf : ScalarFree (quotientTrace τB hB ω trB).toLinearMap
      (constant τB hB ω trB).range ψ.range)
    (S : RealTracialSequence τR.toLinearMap)
    (hsize : Filter.Tendsto (fun j => (Fintype.card (I j) : ℝ)) Filter.atTop Filter.atTop)
    {b : ℝ} (Q : CanonicalSecondFrame τB hB ω trB ψ hψ b)
    (x : B) (hxstar : star x = x) (hxsq : x * x = 1) (hx0 : τB x = 0)
    (source_balls : ∀ C : ℝ, IsClosed (gnsTracialVector τB '' Metric.closedBall (0 : B) C))
    (published : CanonicalFreeCornerInput τB τR hB ω trB ψ hψτ hψ M Q x hxsq)
    (rounding : SpectralProjectionRoundingInput τA)
…

Mentions: OAI.KadisonSimilarity.ScalarFree, OAI.KadisonSimilarity.RealTracialSequence, OAI.KadisonSimilarity.CanonicalSecondFrame, OAI.KadisonSimilarity.gnsTracialVector, OAI.KadisonSimilarity.CanonicalFreeCornerInput, OAI.KadisonSimilarity.SpectralProjectionRoundingInput