DihedralCornerDensity.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Separate L²-continuity extends the positive-power corner trace tests. Only density of their linear span in the centered corner is needed; no uniform bound on approximants is imposed.

theorem OAI.KadisonSimilarity.TracialCornerGeometry.trace_middle_eq_inner line 23
Source documentation
The trace with fixed left and right factors is a continuous functional of the middle L²-vector, by traciality and the inner-product identity.
```
theorem trace_middle_eq_inner (a x b : P) :
    G.trace (a * x * b) = inner ℂ (G.vector (star (b * a))) (G.vector x) := by
…
```

theorem OAI.KadisonSimilarity.TracialCornerGeometry.trace_middle_zero_of_mem_closed_span line 32

Source documentation

A middle-factor trace test that vanishes on generators vanishes on the closed linear span of their L²-vectors.

theorem trace_middle_zero_of_mem_closed_span (S : Set P) (a x b : P)
    (hx : G.vector x ∈ (Submodule.span ℂ (G.vector '' S)).topologicalClosure)
    (hzero : ∀ y ∈ S, G.trace (a * y * b) = 0) :
    G.trace (a * x * b) = 0 := by
…

def OAI.KadisonSimilarity.DihedralCornerWords.alternatingProduct line 56
Source documentation
Ordered alternating products, with the first list supplying fixed left letters and the second list supplying the variable right letters.
```
def alternatingProduct : List P → List P → P
  | a :: as, x :: xs => a * x * alternatingProduct as xs
  | _, _ => 1
```
theorem OAI.KadisonSimilarity.DihedralCornerWords.alternatingProduct_nil line 60
theorem OAI.KadisonSimilarity.DihedralCornerWords.alternatingProduct_cons line 61

theorem OAI.KadisonSimilarity.DihedralCornerWords.trace_alternatingProduct_zero_of_dense line 66

Source documentation

Extending one variable at a time requires only L²-density. The fixed factors may have arbitrary operator norms.

theorem trace_alternatingProduct_zero_of_dense
    (G : TracialCornerGeometry P H) (S : Set P) (as : List P) (a : P)
    (hzero : ∀ xs : List P, xs.length = as.length → (∀ x ∈ xs, x ∈ S) →
      G.trace (a * alternatingProduct as xs) = 0)
    (xs : List P) (hlen : xs.length = as.length)
    (hmem : ∀ x ∈ xs,
      G.vector x ∈ (Submodule.span ℂ (G.vector '' S)).topologicalClosure) :
    G.trace (a * alternatingProduct as xs) = 0 := by
…

Mentions: OAI.KadisonSimilarity.TracialCornerGeometry, OAI.KadisonSimilarity.DihedralCornerWords.alternatingProduct

def OAI.KadisonSimilarity.DihedralCornerWords.positiveCornerPowers line 105
Source documentation
The positive compressed rotation powers spanning the centered dihedral corner.
```
def positiveCornerPowers (p w : P) : Set P :=
…
```

theorem OAI.KadisonSimilarity.DihedralCornerWords.split_even_alternating_word line 114

Source documentation

Split an even alternating word into its two ordered lists of letters. The product identity is valid after applying any map into the ambient algebra.

theorem split_even_alternating_word (f : R → P) (w : List R)
    (hw : AlternatingCenteredWord τR AR BR true w) (heven : w.length % 2 = 0) :
    ∃ as bs : List R, as.length = bs.length ∧ w.length = 2 * as.length ∧
      (∀ a ∈ as, a ∈ AR ∧ τR a = 0) ∧ (∀ b ∈ bs, b ∈ BR ∧ τR b = 0) ∧
      (w.map f).prod = alternatingProduct (as.map f) (bs.map f) := by
…

Mentions: OAI.KadisonSimilarity.AlternatingCenteredWord, OAI.KadisonSimilarity.DihedralCornerWords.alternatingProduct

theorem OAI.KadisonSimilarity.DihedralCornerWords.alternatingProduct_eq_positive_blocks line 151

Source documentation

Choosing a positive exponent for each generator converts the alternating product to the concrete list of corner blocks.

theorem alternatingProduct_eq_positive_blocks (p w : P) (as xs : List P)
    (hlen : xs.length = as.length) (hsupport : ∀ a ∈ as, a * p = a)
    (hmem : ∀ x ∈ xs, x ∈ positiveCornerPowers p w) :
    ∃ bs : List (P × ℕ), bs.map Prod.fst = as ∧
      (∀ b ∈ bs, 0 < b.2) ∧
      alternatingProduct as xs = (bs.map fun b => b.1 * w ^ b.2 * p).prod := by
…

Mentions: OAI.KadisonSimilarity.DihedralCornerWords.positiveCornerPowers, OAI.KadisonSimilarity.DihedralCornerWords.alternatingProduct

theorem OAI.KadisonSimilarity.DihedralCornerWords.trace_positive_corner_generators_zero line 183

Source documentation

The original scalar freeness supplies every positive-generator test, with the support factors and exponent choices constructed explicitly.

theorem trace_positive_corner_generators_zero
    (G : TracialCornerGeometry P H) (D A : StarSubalgebra ℂ P)
    (hf : ScalarFree G.trace D A) {d s : P}
    (hd : d ∈ D) (hs : s ∈ A) (hd0 : G.trace d = 0) (hs0 : G.trace s = 0)
    (p : P) (as xs : List P) (hne : as ≠ []) (hlen : xs.length = as.length)
    (hD : ∀ a ∈ as, a ∈ D) (hzero : ∀ a ∈ as, G.trace a = 0)
    (habsorb : ∀ a ∈ as, a * d = a)
    (hleft : ∀ a ∈ as, p * a = a) (hright : ∀ a ∈ as, a * p = a)
    (hmem : ∀ x ∈ xs, x ∈ positiveCornerPowers p (d * s)) :
    G.trace (alternatingProduct as xs) = 0 := by
…

Mentions: OAI.KadisonSimilarity.TracialCornerGeometry, OAI.KadisonSimilarity.ScalarFree, OAI.KadisonSimilarity.DihedralCornerWords.positiveCornerPowers, OAI.KadisonSimilarity.DihedralCornerWords.alternatingProduct

theorem OAI.KadisonSimilarity.DihedralCornerWords.trace_corner_alternating_zero_of_dense line 210

Source documentation

Every even cyclic product of centered corner letters vanishes once the positive compressed powers have dense span in the centered second corner.

theorem trace_corner_alternating_zero_of_dense
    (G : TracialCornerGeometry P H) (D A : StarSubalgebra ℂ P)
    (hf : ScalarFree G.trace D A) {d s : P}
    (hd : d ∈ D) (hs : s ∈ A) (hd0 : G.trace d = 0) (hs0 : G.trace s = 0)
    (p : P) (as xs : List P) (hne : as ≠ []) (hlen : xs.length = as.length)
    (hD : ∀ a ∈ as, a ∈ D) (hzero : ∀ a ∈ as, G.trace a = 0)
    (habsorb : ∀ a ∈ as, a * d = a)
    (hleft : ∀ a ∈ as, p * a = a) (hright : ∀ a ∈ as, a * p = a)
    (hmem : ∀ x ∈ xs, G.vector x ∈
      (Submodule.span ℂ (G.vector '' positiveCornerPowers p (d * s))).topologicalClosure) :
    G.trace (alternatingProduct as xs) = 0 := by
…

theorem OAI.KadisonSimilarity.DihedralCornerWords.coe_corner_list_prod line 229
Source documentation
Coercing a corner product inserts the corner identity at its right end.
```
theorem coe_corner_list_prod (p : P) (hp : IsStarProjection p)
    (w : List (CStarCorner p hp)) :
    (w.prod : P) = (List.map (fun x : CStarCorner p hp => (x : P)) w).prod * p := by
…
```
Mentions: OAI.KadisonSimilarity.CStarCorner

theorem OAI.KadisonSimilarity.DihedralCornerWords.scalarFree_corner_of_positive_power_density line 242

Source documentation

Actual corner freeness follows from the original scalar freeness and density of the centered positive compressed rotation powers. The density input is a geometric word-span statement, not a freeness assumption.

theorem scalarFree_corner_of_positive_power_density
    (G : TracialCornerGeometry P H) (D A C : StarSubalgebra ℂ P)
    (hf : ScalarFree G.trace D A) {d s : P}
    (hd : d ∈ D) (hs : s ∈ A) (hd0 : G.trace d = 0) (hs0 : G.trace s = 0)
    (p : P) (hp : IsStarProjection p) (hpD : p ∈ D) (hpC : p ∈ C)
    (hpd : p * d = p) (ht : G.trace p ≠ 0)
    (hdense : ∀ x : CStarCorner p hp, (x : P) ∈ C → G.trace (x : P) = 0 →
      G.vector (x : P) ∈
        (Submodule.span ℂ (G.vector '' positiveCornerPowers p (d * s))).topologicalClosure) :
    ScalarFree (CStarCorner.normalizedTrace p hp G.trace)
      (CStarCorner.subalgebra p hp D hpD) (CStarCorner.subalgebra p hp C hpC) := by
…

Mentions: OAI.KadisonSimilarity.TracialCornerGeometry, OAI.KadisonSimilarity.ScalarFree, OAI.KadisonSimilarity.CStarCorner, OAI.KadisonSimilarity.DihedralCornerWords.positiveCornerPowers, OAI.KadisonSimilarity.CStarCorner.normalizedTrace, OAI.KadisonSimilarity.CStarCorner.subalgebra