TracialCreationCoordinates.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Elementary reduced-word creation in the actual tracial base spaces. The normalized symmetry and corner Haar vectors are constructed, so the only word-model inputs are isometric tensor inclusions and their elementary multiplication and range formulas.

structure OAI.KadisonSimilarity.ElementaryCreationFormulas line 16

Source documentation

Elementary multiplication on two opposite reduced-word subspaces. This record carries no normalization or complete-prefix assumption.

structure ElementaryCreationFormulas {EA ED H : Type*}
    [NormedAddCommGroup EA] [InnerProductSpace ℂ EA]
    [NormedAddCommGroup ED] [InnerProductSpace ℂ ED]
    [NormedAddCommGroup H] [InnerProductSpace ℂ H]
    (S : H →L[ℂ] H) (X : ℕ → H →L[ℂ] H) (s : EA) (x : ℕ → ED)
    (DLead ALead : Submodule ℂ H) where
…

def OAI.KadisonSimilarity.TracialCornerGeometry.baseHaarLetter line 42
Source documentation
The actual normalized corner Haar vector in the centered base space.
```
def baseHaarLetter (n : ℕ) : centeredSubspace (G.baseVector D 1) :=
…
```
Mentions: OAI.KadisonSimilarity.centeredSubspace
theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseHaarLetter_coe line 48
theorem OAI.KadisonSimilarity.TracialCornerGeometry.norm_baseHaarLetter line 54
Source documentation
The normalized trace and the exact initial-projection identity give Hilbert norm one for each positive Haar power.
```
theorem norm_baseHaarLetter (n : ℕ) :
    ‖G.baseHaarLetter D z ha htrace hhaar n‖ = 1 := by
…
```
abbrev OAI.KadisonSimilarity.TracialCreationFormulas line 84
Source documentation
The standard free-product model supplies these elementary word identities. All letters and tensor factors are the actual centered tracial base spaces; no complete-prefix estimate is part of the data.
```
abbrev TracialCreationFormulas (ALead : Submodule ℂ H) :=
…
```
def OAI.KadisonSimilarity.TracialCreationFormulas.toAlternatingCreationCoordinates line 97
Source documentation
Normalize the elementary creation data using the proved norms of the actual symmetry and corner Haar vectors.
```
def toAlternatingCreationCoordinates (hself : star s = s) (hsquare : s * s = 1)
    (hτ : G.trace 1 = 1) :
    AlternatingCreationCoordinates (centeredSubspace (G.baseVector A 1))
      (centeredSubspace (G.baseVector D 1)) (G.left (s : P))
      (fun n => G.left ((haarCornerLetter z a n : D) : P)) W.vacuumᗮ where
…
```
Mentions: OAI.KadisonSimilarity.AlternatingCreationCoordinates, OAI.KadisonSimilarity.centeredSubspace, OAI.KadisonSimilarity.haarCornerLetter
theorem OAI.KadisonSimilarity.TracialCreationFormulas.prefix_isometry line 118
Source documentation
The actual alternating left multiplier is isometric on the nonvacuum head space. This is derived from the two elementary word formulas.
```
theorem prefix_isometry (hself : star s = s) (hsquare : s * s = 1)
    (hτ : G.trace 1 = 1) (m n : ℕ) (y : H) (hy : y ∈ W.vacuumᗮ) :
    ‖G.left (tracialWordPrefix (ι := D.subtype) z a (s : P) m n) y‖ = ‖y‖ :=
…
```
Mentions: OAI.KadisonSimilarity.tracialWordPrefix
theorem OAI.KadisonSimilarity.TracialCreationFormulas.prefix_bound line 127
Source documentation
The actual prefix bound follows from algebra norms and holds uniformly in the Haar frequency.
```
theorem prefix_bound (hself : star s = s) (hsquare : s * s = 1) (m n : ℕ) :
    ‖G.left (tracialWordPrefix (ι := D.subtype) z a (s : P) m n)‖ ≤
…
```
Mentions: OAI.KadisonSimilarity.tracialWordPrefix

def OAI.KadisonSimilarity.TracialCreationFormulas.repeatedWordRealization line 137

Source documentation

The concrete repeated-multiplicity insertion, together with raw word factorization and level actions, gives the propagation realization. Complete prefix isometry and uniform boundedness are both proved by this constructor.

def repeatedWordRealization (hself : star s = s) (hsquare : s * s = 1)
    (hτ : G.trace 1 = 1) (m : ℕ) (Y : H →L[ℂ] H)
    (B₀ : G.baseSpace A →L[ℂ] G.baseSpace A)
    (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)
    (small : G.baseSpace A →L[ℂ] H)
    (hsmall : ∀ v, ‖small v‖ = Real.sqrt a * ‖v‖)
    (hlevelzero : ∀ v, Y (small v) = small (B₀ v))
    (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)))
…

Mentions: OAI.KadisonSimilarity.WordMultiplicity