BufferAnchor.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The concrete absorption anchor is connected

For the binary pair constructed by the two-swap zero-corner completion, the absorption anchor times that completion is the elementary swap of q and w q w*. Both factors have explicit paths to the identity.

lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.anchor_joined_of_completion line 22
Source documentation
The additional equations are satisfied by the explicit zero-corner completion. They identify the anchor's component without a K₁ assumption.
```
lemma BufferAbsorptionCorner.anchor_joined_of_completion
    (D : BufferAbsorptionCorner E) (u : unitary E)
    (hu : Joined (1 : unitary E) u)
    (huq : (u : E) * D.q = D.b)
    (huw : (u : E) * D.w = (1 - D.q) + D.a) :
    Joined (1 : unitary E) D.anchor := by
…
```
Mentions: OAI.WeakPureInfiniteness.BufferAbsorptionCorner

lemma OAI.WeakPureInfiniteness.completion_on_initial line 109

Source documentation

A two-swap completion acts on its prescribed initial projection.

private lemma completion_on_initial (v r : E) (hv : v * star v * v = v)
    (hr : star r * r = 1) (hpr : (star v * v) * r = 0)
    (hqr : (v * star v) * r = 0) :
    partialIsometryCompletion r (star v * v) v * (star v * v) = v := by
…

Mentions: OAI.WeakPureInfiniteness.partialIsometryCompletion

lemma OAI.WeakPureInfiniteness.exists_connected_buffer_corner line 119

Source documentation

The actual three-isometry construction supplies all the extra anchor equations as well as the binary row.

lemma exists_connected_buffer_corner (w r z : E)
    (hw : star w * w = 1) (hr : star r * r = 1) (hz : star z * z = 1)
    (hwr : star w * r = 0) (hwz : star w * z = 0) (hrz : star r * z = 0) :
    ∃ D : BufferAbsorptionCorner E,
      D.q = 1 - w * star w ∧ D.w = w ∧ D.a = r * D.q ∧
      Joined (1 : unitary E) D.anchor ∧
      ∀ y : E,
        Commute w y → Commute (star w) y →
        Commute r y → Commute (star r) y →
        Commute z y → Commute (star z) y →
        Commute D.a y ∧ Commute (star D.a) y ∧
        Commute D.b y ∧ Commute (star D.b) y := by
…

Mentions: OAI.WeakPureInfiniteness.BufferAbsorptionCorner

lemma OAI.WeakPureInfiniteness.exists_connected_finite_buffer_absorption line 240

Source documentation

Finite-row absorption by an actual three-isometry buffer, now with an ambient path from the identity. The target is a coisometric row in the literal complement of the first buffer isometry.

lemma exists_connected_finite_buffer_absorption {I : Type*} [Fintype I] [DecidableEq I]
    (s t : I → E) (r w a b : E)
    (hr : star r * r = 1) (hrs : ∀ i, star r * s i = 0)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (hw : star w * w = 1) (ha : star a * a = 1) (hb : star b * b = 1)
    (hwa : star w * a = 0) (hwb : star w * b = 0) (hab : star a * b = 0)
    (hwr : Commute w r) (hwsr : Commute (star w) r)
    (hws : ∀ i, Commute w (s i) ∧ Commute (star w) (s i))
    (hwt : ∀ i, Commute w (t i) ∧ Commute (star w) (t i))
    (hat : ∀ i, Commute a (t i) ∧ Commute (star a) (t i))
    (hbt : ∀ i, Commute b (t i) ∧ Commute (star b) (t i))
    (htq : ∀ i, t i * (1 - w * star w) = t i)
…