ZeroUnitRows.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Finite proper-row comparison through the zero-unit buffer

Only one unused row element is needed for the finite binary encoding. The unit and complementary isometries remain explicit throughout.

lemma OAI.WeakPureInfiniteness.exists_finite_zero_unit_binary_encoding line 20

Source documentation

The binary encoding construction needs only the tested finite prefix and its next unused isometry, rather than a countable row extension.

lemma exists_finite_zero_unit_binary_encoding (n : ℕ)
    (x : Fin (n + 2) → 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) :
    ∃ A B : E, star A * A = 1 ∧ star B * B = 1 ∧ star A * B = 0 ∧
      A * star A + B * star B = 1 ∧
      ∀ i : Fin (n + 1), A ^ (i : ℕ) * B = x i.castSucc := by
…

lemma OAI.WeakPureInfiniteness.exists_relative_finite_zero_unit_binary_encoding line 63

Source documentation

Finite encoding in an actual projection corner. In particular this applies to a proper prefix of the finite coisometric vacuum-split row.

lemma exists_relative_finite_zero_unit_binary_encoding (n : ℕ)
    (q : E) (hq : star q = q) (hqq : q * q = q)
    (x : Fin (n + 2) → 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) :
    ∃ 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 : Fin (n + 1), A ^ (i : ℕ) * B = x i.castSucc := by
…

lemma OAI.WeakPureInfiniteness.exists_finite_zeroUnit_buffer_comparison line 96

Source documentation

A finite proper row in the buffer commutant has a connected ambient comparison with the corresponding negative buffer prefix. Its initial unit is carried to the buffer unit exactly.

lemma exists_finite_zeroUnit_buffer_comparison [Nontrivial E]
    (r : ℕ → E)
    (hr : ∀ i j, star (r i) * r j = if i = j then 1 else 0)
    (q w z : StarSubalgebra.centralizer ℂ (Set.range r))
    (hq : star q = q) (hqq : q * q = q) (hq0 : q ≠ 0)
    (hw : star w * w = 1) (hww : w * star w = 1 - q)
    (hz : star z * z = 1) (hqz : q * z = z)
    (n : ℕ) (x : Fin (n + 2) → StarSubalgebra.centralizer ℂ (Set.range r))
    (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)
    (a b : StarSubalgebra.centralizer ℂ (Set.range r))
    (ha : star a * a = q) (hb : star b * b = q) (hab : star a * b = 0)
…