ConnectedRowCompletion.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Connected choices of finite binary completions

Three orthogonal buffer isometries let two finite rows with actual unused isometries be matched on the left by a connected unitary. Applying this to the finite shift equations gives a full binary completion with a connected left cocycle relative to a prescribed reference row. Left matching alone is not an assertion of conjugacy.

lemma OAI.WeakPureInfiniteness.connectedRow_product_gram line 21

lemma OAI.WeakPureInfiniteness.exists_connected_finite_row_leftMatch line 31

Source documentation

Only the two displayed commutations with the unused isometries are needed. The buffer need not commute with the tested finite rows.

lemma exists_connected_finite_row_leftMatch [Nontrivial E]
    {n : ℕ} (x y : Fin n → E)
    (hx : ∀ i j, star (x i) * x j = if i = j then 1 else 0)
    (hy : ∀ i j, star (y i) * y j = if i = j then 1 else 0)
    (e f : E) (he : star e * e = 1) (hf : star f * f = 1)
    (hxe : ∀ i, star (x i) * e = 0) (hyf : ∀ i, star (y i) * f = 0)
    (r : Fin 3 → E)
    (hr : ∀ i j, star (r i) * r j = if i = j then 1 else 0)
    (her : Commute (star (r 0)) e) (hfr : Commute (star (r 1)) f) :
    ∃ u : unitary E, Joined (1 : unitary E) u ∧ ∀ i, (u : E) * x i = y i := by
…

lemma OAI.WeakPureInfiniteness.exists_connected_binary_row_completion line 102

Source documentation

The tested finite row is the initial binary prefix, and the full binary row has a connected left cocycle to the specified reference.

lemma exists_connected_binary_row_completion [Nontrivial E]
    {n : ℕ} (x : Fin (n + 1) → E)
    (hx : ∀ i j, star (x i) * x j = if i = j then 1 else 0)
    (e : E) (he : star e * e = 1) (hxe : ∀ i, star (x i) * e = 0)
    (b : Fin 2 → E)
    (hb : ∀ i j, star (b i) * b j = if i = j then 1 else 0)
    (hbs : (∑ i, b i * star (b i)) = 1)
    (r : Fin 3 → E)
    (hr : ∀ i j, star (r i) * r j = if i = j then 1 else 0)
    (her : Commute (star (r 0)) e)
    (hfr : Commute (star (r 1)) (b 0 * e)) :
    ∃ a : Fin 2 → E, ∃ u : unitary E, Joined (1 : unitary E) u ∧
…