ZeroUnitCompletion.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Finite range completion in a zero unit corner

A proper finite row and an orthogonal spare are combined with a concrete coisometric row. The resulting isometry fills exactly the missing range. The construction is algebraic and does not use projection classification.

lemma OAI.WeakPureInfiniteness.coisometry_range_filler line 21
Source documentation
Turn a coisometry into an isometry by moving its initial support into one specified isometric range.
```
lemma coisometry_range_filler (A y : E)
    (hA : A * star A = 1) (hy : star y * y = 1)
    (hpy : (star A * A) * y = y) :
    let C := 1 - star A * A + y * A
…
```

lemma OAI.WeakPureInfiniteness.finite_zero_unit_range_completion line 75

Source documentation

A full finite target row fills the defect of an arbitrary finite proper row with its given orthogonal spare.

lemma finite_zero_unit_range_completion {n : ℕ}
    (x : Fin n → E) (y : E) (a : Fin (n + 1) → E)
    (hx : ∀ i j, star (x i) * x j = if i = j then 1 else 0)
    (hy : star y * y = 1) (hyx : ∀ i, star y * x i = 0)
    (ha : ∀ i j, star (a i) * a j = if i = j then 1 else 0)
    (has : (∑ i, a i * star (a i)) = 1) :
    ∃ C : E, star C * C = 1 ∧
      C * star C = 1 - ∑ i, x i * star (x i) := by
…

lemma OAI.WeakPureInfiniteness.finite_zero_unit_completion_from_binary line 115

Source documentation

A coisometric binary pair supplies every finite target size, so only an actual orthogonal spare is needed to fill the prescribed proper row.

lemma finite_zero_unit_completion_from_binary {n : ℕ}
    (x : Fin n → E) (y a b : E)
    (hx : ∀ i j, star (x i) * x j = if i = j then 1 else 0)
    (hy : star y * y = 1) (hyx : ∀ i, star y * x i = 0)
    (ha : star a * a = 1) (hb : star b * b = 1) (hab : star a * b = 0)
    (hsum : a * star a + b * star b = 1) :
    ∃ C : E, star C * C = 1 ∧
      C * star C = 1 - ∑ i, x i * star (x i) := by
…

lemma OAI.WeakPureInfiniteness.finite_zero_unit_full_row line 129

Source documentation

Appending the concrete missing-range isometry gives a full finite row.

lemma finite_zero_unit_full_row {n : ℕ}
    (x : Fin n → E) (y a b : E)
    (hx : ∀ i j, star (x i) * x j = if i = j then 1 else 0)
    (hy : star y * y = 1) (hyx : ∀ i, star y * x i = 0)
    (ha : star a * a = 1) (hb : star b * b = 1) (hab : star a * b = 0)
    (hsum : a * star a + b * star b = 1) :
    ∃ r : Fin (n + 1) → E,
      (∀ i : Fin n, r i.succ = x i) ∧
      (∀ i j, star (r i) * r j = if i = j then 1 else 0) ∧
      (∑ i, r i * star (r i)) = 1 := by
…

lemma OAI.WeakPureInfiniteness.exists_zero_unit_binary_encoding line 165

Source documentation

A countable orthogonal row in a zero-unit algebra has an exact binary encoding of each prescribed finite prefix. The next row element is the spare.

lemma exists_zero_unit_binary_encoding
    (x : ℕ → E)
    (hx : ∀ i j, star (x i) * x j = if i = j then 1 else 0)
    (a b : E) (ha : star a * a = 1) (hb : star b * b = 1)
    (hab : star a * b = 0) (hsum : a * star a + b * star b = 1) (m : ℕ) :
    ∃ A B : E, star A * A = 1 ∧ star B * B = 1 ∧ star A * B = 0 ∧
      A * star A + B * star B = 1 ∧ ∀ i ≤ m, A ^ i * B = x i := by
…

lemma OAI.WeakPureInfiniteness.relative_zero_unit_completion line 202

Source documentation

The same explicit filler in a supported corner with its actual unit q. No relation between q and the ambient identity is needed.

lemma relative_zero_unit_completion {n : ℕ}
    (q : E) (hq : star q = q) (hqq : q * q = q)
    (x : Fin n → E) (y a b : E)
    (hxs : ∀ i, q * x i = x i ∧ x i * q = x i)
    (hys : q * y = y ∧ y * q = y)
    (hx : ∀ i j, star (x i) * x j = if i = j then q else 0)
    (hy : star y * y = q) (hyx : ∀ i, star y * x i = 0)
    (ha : star a * a = q) (hb : star b * b = q) (hab : star a * b = 0)
    (hsum : a * star a + b * star b = q) :
    ∃ C : E, q * C = C ∧ C * q = C ∧ star C * C = q ∧
      C * star C = q - ∑ i, x i * star (x i) := by
…

lemma OAI.WeakPureInfiniteness.exists_relative_zero_unit_binary_encoding line 237

Source documentation

Exact finite binary encoding in the given corner. The countable proper row supplies its own next unused isometry at every finite stage.

lemma exists_relative_zero_unit_binary_encoding
    (q : E) (hq : star q = q) (hqq : q * q = q)
    (x : ℕ → E) (a b : E)
    (hxs : ∀ i, q * x i = x i ∧ x i * q = x i)
    (hx : ∀ i j, star (x i) * x j = if i = j then q else 0)
    (ha : star a * a = q) (hb : star b * b = q) (hab : star a * b = 0)
    (hsum : a * star a + b * star b = q) (m : ℕ) :
    ∃ A B : E, q * A = A ∧ A * q = A ∧ q * B = B ∧ B * q = B ∧
      star A * A = q ∧ star B * B = q ∧ star A * B = 0 ∧
      A * star A + B * star B = q ∧ ∀ i ≤ m, A ^ i * B = x i := by
…

lemma OAI.WeakPureInfiniteness.coisometry_range_filler_conjugation line 285
Source documentation
On elements commuting with the initial projection, the filler has an exact two-corner formula. This records the term that must be controlled by the canonical-shift implementer.
```
lemma coisometry_range_filler_conjugation (A y x : E)
    (hA : A * star A = 1) (hx : Commute (star A * A) x) :
    let C := 1 - star A * A + y * A
…
```

lemma OAI.WeakPureInfiniteness.binary_shift_shrink_products line 324

Source documentation

The concrete binary shift filler accepts any unitary inserted before the coisometry. Its final projection is independent of that insertion.

lemma binary_shift_shrink_products (r a : Fin 2 → E)
    (hr : ∀ i j, star (r i) * r j = if i = j then 1 else 0)
    (ha : ∀ i j, star (a i) * a j = if i = j then 1 else 0)
    (has : (∑ i, a i * star (a i)) = 1) (u : unitary E) :
    let v := (u : E) * finiteCuntzTransfer r a 1
…

Mentions: OAI.WeakPureInfiniteness.finiteCuntzTransfer