DihedralColumnIdentification.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Identify the normalized actual dihedral columns with completed word maps.

theorem OAI.KadisonSimilarity.TracialCornerGeometry.actual_dihedral_column_apply line 34

Source documentation

On every completed base vector, the actual normalized dihedral column is the normalized repeated word supplied by the reduced-word model.

theorem actual_dihedral_column_apply (hf : ScalarFree G.trace D A)
    (hU : TracialWordFormula G A D U) (k : ℕ) (v : G.baseSpace A) :
    G.tracialDihedralInclusion D A hf hτ d s e hdstar hdsq hd0 hsstar hssq hs0
      he ht hte k v =
      dihedralNormalization t • U.inclusion k (hilbertTensorInsert
        (G.baseSymmetryRepeatedInclusion A s hs0 hsstar hssq hτ k v)
        (tracialEndpointWord G D k e (fun _ => d) (fun _ => hd0))) := by
…

Mentions: OAI.KadisonSimilarity.ScalarFree, OAI.KadisonSimilarity.TracialWordFormula, OAI.KadisonSimilarity.dihedralNormalization, OAI.KadisonSimilarity.hilbertTensorInsert, OAI.KadisonSimilarity.tracialEndpointWord

theorem OAI.KadisonSimilarity.TracialCornerGeometry.actual_dihedral_columns_apply line 64

Source documentation

The finite family used in Fourier compression has the same repeated-word coordinates, with no independently assumed word isometries.

theorem actual_dihedral_columns_apply (hf : ScalarFree G.trace D A)
    (hU : TracialWordFormula G A D U) (N : ℕ) (i : Fin N) (v : G.baseSpace A) :
    G.tracialDihedralColumns D A hf hτ d s e hdstar hdsq hd0 hsstar hssq hs0
      he ht hte N i v =
      dihedralNormalization t • U.inclusion i.val (hilbertTensorInsert
        (G.baseSymmetryRepeatedInclusion A s hs0 hsstar hssq hτ i.val v)
        (tracialEndpointWord G D i.val e (fun _ => d) (fun _ => hd0))) := by
…

theorem OAI.KadisonSimilarity.TracialCornerGeometry.actual_dihedral_column_eq_repeated line 76

Source documentation

The Fourier columns are exactly the normalized repeated-letter columns used by propagation, with normalization derived from the projection trace.

theorem actual_dihedral_column_eq_repeated (hf : ScalarFree G.trace D A)
    (hU : TracialWordFormula G A D U) (k : ℕ) (v : G.baseSpace A) :
    G.tracialDihedralInclusion D A hf hτ d s e hdstar hdsq hd0 hsstar hssq hs0
      he ht hte k v =
    G.repeatedDihedralInclusion D A hτ d s e hdstar hdsq hd0 hsstar hssq hs0
      he ht hte U k v := by
…

Mentions: OAI.KadisonSimilarity.ScalarFree, OAI.KadisonSimilarity.TracialWordFormula