VacuumSplit.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

A concrete almost central split of a canonical finite O∞ row

The corner and its coisometric row are constructed from unused canonical isometries and the finite word sum. Its complement is the range of an actual isometry. Thus the vacuum compression and the complement are both controlled without assuming a projection-classification theorem.

lemma OAI.WeakPureInfiniteness.transported_row line 20
lemma OAI.WeakPureInfiniteness.transported_zeroCornerRow line 45

lemma OAI.WeakPureInfiniteness.exists_canonical_vacuum_split_with_pair_and_isometry line 66

Source documentation

The explicit finite split, retaining its transported binary generators.

lemma exists_canonical_vacuum_split_with_pair_and_isometry [Nontrivial E] (s : ℕ → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (n : ℕ) (ε : ℝ) (hε : 0 < ε) :
    ∃ (f w : E) (g : Fin (n + 1) → E),
      f ≠ 0 ∧ star f = f ∧ f * f = f ∧
      star w * w = 1 ∧ w * star w = 1 - f ∧
      (∀ i j, star (g i) * g j = if i = j then f else 0) ∧
      (∑ i, g i * star (g i)) = f ∧
      (∀ i : Fin (n + 1), ‖s i * f - f * s i‖ < ε) ∧
      (∀ i : Fin (n + 1), ‖f * s i * f - g i‖ < ε) ∧
      ‖f * (1 - ∑ i : Fin (n + 1), s i * star (s i)) * f‖ < ε ∧
      f * s (n + 2) = 0 ∧
…

lemma OAI.WeakPureInfiniteness.exists_canonical_vacuum_split_with_pair line 228

Source documentation

The explicit finite split, retaining its transported binary generators.

lemma exists_canonical_vacuum_split_with_pair [Nontrivial E] (s : ℕ → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (n : ℕ) (ε : ℝ) (hε : 0 < ε) :
    ∃ (f w : E) (g : Fin (n + 1) → E),
      f ≠ 0 ∧ star f = f ∧ f * f = f ∧
      star w * w = 1 ∧ w * star w = 1 - f ∧
      (∀ i j, star (g i) * g j = if i = j then f else 0) ∧
      (∑ i, g i * star (g i)) = f ∧
      (∀ i : Fin (n + 1), ‖s i * f - f * s i‖ < ε) ∧
      (∀ i : Fin (n + 1), ‖f * s i * f - g i‖ < ε) ∧
      ‖f * (1 - ∑ i : Fin (n + 1), s i * star (s i)) * f‖ < ε ∧
      f * s (n + 2) = 0 ∧
…

lemma OAI.WeakPureInfiniteness.exists_canonical_vacuum_split line 251

Source documentation

Every finite canonical row admits the explicit vacuum-killing split. The returned row is coisometric in f, and an actual isometry fills 1-f.

lemma exists_canonical_vacuum_split [Nontrivial E] (s : ℕ → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (n : ℕ) (ε : ℝ) (hε : 0 < ε) :
    ∃ (f w : E) (g : Fin (n + 1) → E),
      f ≠ 0 ∧ star f = f ∧ f * f = f ∧
      star w * w = 1 ∧ w * star w = 1 - f ∧
      (∀ i j, star (g i) * g j = if i = j then f else 0) ∧
      (∑ i, g i * star (g i)) = f ∧
      (∀ i : Fin (n + 1), ‖s i * f - f * s i‖ < ε) ∧
      (∀ i : Fin (n + 1), ‖f * s i * f - g i‖ < ε) ∧
      ‖f * (1 - ∑ i : Fin (n + 1), s i * star (s i)) * f‖ < ε ∧
      f * s (n + 2) = 0 := by
…