TracialHaarWordColumns.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The Haar test columns used in propagation are actual reduced-word inclusions. Their isometry and product formula follow from the word model and the normalized corner Haar letters.

def OAI.KadisonSimilarity.TracialCornerGeometry.haarRepeatedWordInclusion line 45
Source documentation
Unit vacuum endpoint and unit centered Haar letters give isometric columns at every word degree.
```
def haarRepeatedWordInclusion (k n : ℕ) : WordMultiplicity (G.baseVector A 1) k →ₗᵢ[ℂ] H :=
…
```
Mentions: OAI.KadisonSimilarity.WordMultiplicity

theorem OAI.KadisonSimilarity.TracialCornerGeometry.haarRepeatedWordInclusion_baseVector line 55

Source documentation

On bounded base vectors this column is precisely the ordinary repeated product, with no independently assumed prefix formula.

theorem haarRepeatedWordInclusion_baseVector
    (hU : TracialWordFormula G A D U)
    (s : A) (hs0 : G.trace (s : P) = 0) (hsstar : star s = s) (hssq : s * s = 1)
    (k n : ℕ) (b : A) :
    G.haarRepeatedWordInclusion A D hτ U z ha htrace hhaar k n
      (G.baseSymmetryRepeatedInclusion A s hs0 hsstar hssq hτ k (G.baseVector A b)) =
      G.vector (((s : P) * (haarCornerLetter z a n : D)) ^ k * (b : P)) := by
…

Mentions: OAI.KadisonSimilarity.TracialWordFormula, OAI.KadisonSimilarity.haarCornerLetter

theorem OAI.KadisonSimilarity.TracialCornerGeometry.haarRepeatedWordInclusion_factor line 73

Source documentation

The final Haar letter is supported on q, so the product formula is the exact small-column factorization consumed by propagation.

theorem haarRepeatedWordInclusion_factor
    (hU : TracialWordFormula G A D U)
    (s : A) (hs0 : G.trace (s : P) = 0) (hsstar : star s = s) (hssq : s * s = 1)
    (m n : ℕ) (b : A) :
    G.haarRepeatedWordInclusion A D hτ U z ha htrace hhaar (m + 1) n
      (G.baseSymmetryRepeatedInclusion A s hs0 hsstar hssq hτ (m + 1)
        (G.baseVector A b)) =
      G.left (tracialWordPrefix (ι := D.subtype) z a (s : P) m n)
…

Mentions: OAI.KadisonSimilarity.TracialWordFormula, OAI.KadisonSimilarity.tracialWordPrefix

theorem OAI.KadisonSimilarity.TracialCornerGeometry.repeated_propagation_of_published_words line 95

Source documentation

The published elementary creation maps and the ordinary product formula give the manuscript's propagation estimate. The test word columns and their prefix identities are constructed here.

theorem repeated_propagation_of_published_words
    (hU : TracialWordFormula G A D U)
    (creation : RicardXuCreationInput G A D)
    (hf : ScalarFree G.trace D A) (hfaithful : Function.Injective G.vector)
    (hdense : ReducedWordGenerated G A D)
    (s : A) (hs0 : G.trace (s : P) = 0) (hsstar : star s = s) (hssq : s * s = 1)
    (m : ℕ) (Y : H →L[ℂ] H)
    (hbase : ∀ x ∈ G.baseSpace A, Y x ∈ G.baseSpace A)
    (hYD : ∀ x : D, Y.comp (G.left (x : P)) = (G.left (x : P)).comp Y)
    (B : WordMultiplicity (G.baseVector A 1) (m + 1) →L[ℂ]
      WordMultiplicity (G.baseVector A 1) (m + 1))
    (hY : ∀ v d r, Y (U.inclusion (m + 1)
…

Mentions: OAI.KadisonSimilarity.TracialWordFormula, OAI.KadisonSimilarity.RicardXuCreationInput, OAI.KadisonSimilarity.ScalarFree, OAI.KadisonSimilarity.ReducedWordGenerated, OAI.KadisonSimilarity.WordMultiplicity

theorem OAI.KadisonSimilarity.TracialCornerGeometry.all_degrees_propagation_of_published_words line 143

Source documentation

The degree-zero case is exact, and every positive degree follows from the constructed Haar test columns. Base-space invariance is derived from the same ordinary word action.

theorem all_degrees_propagation_of_published_words
    (hU : TracialWordFormula G A D U)
    (creation : RicardXuCreationInput G A D)
    (hf : ScalarFree G.trace D A) (hfaithful : Function.Injective G.vector)
    (hdense : ReducedWordGenerated G A D)
    (s : A) (hs0 : G.trace (s : P) = 0) (hsstar : star s = s) (hssq : s * s = 1)
    (Y : H →L[ℂ] H)
    (hYD : ∀ x : D, Y.comp (G.left (x : P)) = (G.left (x : P)).comp Y)
    (B : ∀ k, WordMultiplicity (G.baseVector A 1) k →L[ℂ]
      WordMultiplicity (G.baseVector A 1) k)
    (hY : ∀ k v d r, Y (U.inclusion k
        (hilbertTensorInsert v (endpointWord d (fun _ : Fin k => r)))) =
…