ConcreteRepeatedPropagation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Repeated-word propagation with all small-vector and prefix estimates constructed from the actual scalar-free tracial model.

theorem OAI.KadisonSimilarity.concrete_repeated_propagation line 34

Source documentation

The propagation conclusion for a positive degree. Only elementary word formulas remain as geometric inputs: small-vector normalization, prefix isometry, the exceptional coefficient limit, and the full-column estimate are proved in the construction.

theorem concrete_repeated_propagation
    (hf : ScalarFree G.trace D A) (hτ : G.trace 1 = 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))
    (word : ℕ → WordMultiplicity (G.baseVector A 1) (m + 1) →ₗᵢ[ℂ] H)
    (hlevel : ∀ n v, Y (word n
      (G.baseSymmetryRepeatedInclusion A s hzero hself hsquare hτ (m + 1) v)) =
      word n (Bₖ (G.baseSymmetryRepeatedInclusion A s hzero hself hsquare hτ (m + 1) v)))
    (hword : ∀ n (v : A), word n
…

Mentions: OAI.KadisonSimilarity.ScalarFree, OAI.KadisonSimilarity.WordMultiplicity