TracialFreeCornerEstimate.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual tracial word model supplies both errors in the Fourier compression argument. The only remaining Fourier hypotheses below concern the spectral test operator itself; level preservation and propagation are derived from the matrix symmetries and the cited published inputs.

theorem OAI.KadisonSimilarity.TracialCornerGeometry.tracial_word_level_ranges line 52
Source documentation
Both the operator and its adjoint preserve the actual word levels. Star closure supplies the second conclusion; it is not additional data.
```
theorem tracial_word_level_ranges :
    (∀ n x, Y (U.inclusion n x) ∈ (U.inclusion n).toLinearMap.range) ∧
    (∀ n x, Y.adjoint (U.inclusion n x) ∈ (U.inclusion n).toLinearMap.range) := by
…
```

theorem OAI.KadisonSimilarity.TracialCornerGeometry.free_corner_estimate_of_published_words line 92

Source documentation

The free-corner estimate with all word-structure and propagation prerequisites derived. The published derivation inputs, the elementary reduced creation model, and the standard support/comparison data are explicit. The spectral test is used only through its norm and exact finite Fourier compression.

theorem free_corner_estimate_of_published_words
    (creation : RicardXuCreationInput G A D) (hf : ScalarFree G.trace D A)
    (hdense : ReducedWordGenerated G A D)
    {q : D} {hq : IsStarProjection q} (z : unitary (CStarCorner q hq))
    {a : ℝ} (ha : 0 < a) (htrace : G.trace (q : P) = (a : ℂ))
    (hhaar : HaarCornerMoments (G.baseGeometry D).trace z a)
    (τ : P → ℝ) (support : TracialRightSupportInput τ (q : P) A)
    (e₀ : P) (he₀ : IsStarProjection e₀) (he₀D : e₀ ∈ D)
    (hqe : τ (q : P) ≤ τ e₀) (comparison : FiniteFactorProjectionComparison τ)
    {N₀ : ℕ} (hN₀ : 0 < N₀) (frame : Fin N₀ → D)
    (hframe : ∀ i j, star (frame i : P) * (frame j : P) = if i = j then e₀ else 0)
    (hsum : ∑ i, (frame i : P) * star (frame i : P) = 1)
…

Mentions: OAI.KadisonSimilarity.RicardXuCreationInput, OAI.KadisonSimilarity.ScalarFree, OAI.KadisonSimilarity.ReducedWordGenerated, OAI.KadisonSimilarity.CStarCorner, OAI.KadisonSimilarity.HaarCornerMoments, OAI.KadisonSimilarity.TracialRightSupportInput, OAI.KadisonSimilarity.FiniteFactorProjectionComparison