FiniteRowCompletion.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Connected completion of the finite row isometry

A second unused source isometry is orthogonal to the entire finite sum. When its range is the complement of the target corner, it is an actual common spare for the two-swap completion. The complementary projection is therefore the range of an explicit unit-source isometry.

lemma OAI.WeakPureInfiniteness.finiteRowWordSum_unused line 21
lemma OAI.WeakPureInfiniteness.finiteRowIsometry_unused line 37
lemma OAI.WeakPureInfiniteness.finiteRowRange_unused line 44

lemma OAI.WeakPureInfiniteness.exists_connected_finiteRowCompletion line 54

Source documentation

The completion retains a literal complement isometry, not only a K-theoretic relation between projections.

lemma exists_connected_finiteRowCompletion [Nontrivial E]
    (s t : I → E) (r q z : E)
    (hq : q * q = q) (hqs : star q = q) (hrr : star r * r = 1)
    (hr : ∀ i, star r * s i = 0)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (htq : ∀ i, t i * q = t i) (ht : ∑ i, t i * star (t i) = q)
    (hz : star z * z = 1) (hzr : star z * r = 0)
    (hzs : ∀ i, star z * s i = 0) (hqz : q = 1 - z * star z) (m : ℕ) :
    ∃ u : unitary E, Joined (1 : unitary E) u ∧
      (u : E) = partialIsometryCompletion z q (finiteRowIsometry s t r q m) ∧
      (u : E) * q = finiteRowIsometry s t r q m ∧
      star ((u : E) * z) * ((u : E) * z) = 1 ∧
…

Mentions: OAI.WeakPureInfiniteness.partialIsometryCompletion, OAI.WeakPureInfiniteness.finiteRowIsometry