ZeroUnitBuffer.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Shrinking zero-unit rows against the actual third buffer

The initial corner, its complementary isometry and the isometry inside it remain explicit. These are the data supplied by the finite vacuum split; no equivalence of arbitrary projections is assumed.

lemma OAI.WeakPureInfiniteness.exists_commuting_binary_corner_shrink line 22

Source documentation

A full binary row in any supported corner can be shrunk against an orthogonal commuting buffer row, with no change in its finite-word error.

lemma exists_commuting_binary_corner_shrink
    (q : E) (hq : star q = q) (hqq : q * q = q) (hq0 : q ≠ 0)
    (a r : Fin 2 → E)
    (ha : ∀ i j, star (a i) * a j = if i = j then q else 0)
    (has : (∑ i, a i * star (a i)) = q)
    (hr : ∀ i j, star (r i) * r j = if i = j then 1 else 0)
    (har : bergRowsCommute a r)
    (hqr : ∀ j, Commute q (r j))
    (m : ℕ) (ε : ℝ) (hε : 0 < ε) :
    ∃ c : E, q * c = c ∧ c * q = c ∧ star c * c = q ∧
      c * star c = q * (1 - r 0 * star (r 0)) ∧
      ∀ i ≤ m, ‖c * (a 0 ^ i * a 1) * star c -
…

Mentions: OAI.WeakPureInfiniteness.bergRowsCommute

lemma OAI.WeakPureInfiniteness.closedCanonicalRowAlgebra_commutes_element line 82
Source documentation
Every element of the buffer's closed row algebra inherits its exact commutation with the supplied finite construction data.
```
lemma closedCanonicalRowAlgebra_commutes_element
    (r : ℕ → E) (x : E)
    (hx : ∀ i, Commute (r i) x ∧ Commute (star (r i)) x)
    (b : closedCanonicalRowAlgebra r) : Commute (b : E) x := by
…
```
Mentions: OAI.WeakPureInfiniteness.closedCanonicalRowAlgebra

lemma OAI.WeakPureInfiniteness.exists_complementary_binary_corner_shrink line 98

Source documentation

The explicit complement isometry and an isometry inside q give the reverse shrink. The initial corner is p; the final corner is exactly pq. No equivalence of an unspecified complementary projection is required.

lemma exists_complementary_binary_corner_shrink
    (p q w z : E)
    (hp : star p = p) (hpp : p * p = p) (hp0 : p ≠ 0)
    (hw : star w * w = 1) (hww : w * star w = 1 - q)
    (hz : star z * z = 1) (hqz : q * z = z)
    (hpw : Commute p w) (hpz : Commute p z)
    (b : Fin 2 → E)
    (hb : ∀ i j, star (b i) * b j = if i = j then p else 0)
    (hbs : (∑ i, b i * star (b i)) = p)
    (hbw : ∀ i, Commute (b i) w ∧ Commute (b i) (star w))
    (hbz : ∀ i, Commute (b i) z ∧ Commute (b i) (star z))
    (m : ℕ) (ε : ℝ) (hε : 0 < ε) :
…

lemma OAI.WeakPureInfiniteness.exists_buffer_binary_encoding line 149

Source documentation

A third canonical row supplies its finite binary encoding inside the closed buffer algebra. Consequently all supplied construction data commute with the encoding, including their adjoints.

lemma exists_buffer_binary_encoding [Nontrivial E]
    (r : ℕ → E)
    (hr : ∀ i j, star (r i) * r j = if i = j then 1 else 0)
    (m : ℕ) :
    ∃ b : Fin 2 → closedCanonicalRowAlgebra r,
      (∀ i j, star (b i : E) * (b j : E) =
        if i = j then canonicalTailProjection r 1 else 0) ∧
      (∑ i, (b i : E) * star (b i : E)) = canonicalTailProjection r 1 ∧
      ∀ i ≤ m, (b 0 : E) ^ i * (b 1 : E) = canonicalNegativeRow r i := by
…

Mentions: OAI.WeakPureInfiniteness.closedCanonicalRowAlgebra, OAI.WeakPureInfiniteness.canonicalTailProjection, OAI.WeakPureInfiniteness.canonicalNegativeRow