ZeroUnitComparison.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Zero-unit finite comparison with a concrete central buffer

The two complementary isometries remain supplied as actual elements. The common-corner restriction uses only the closed algebra of the buffer and its commutant, so no arbitrary-map uniqueness theorem is invoked.

lemma OAI.WeakPureInfiniteness.bufferAlgebra_commutes_commutant line 21
Source documentation
Elements in the closed buffer algebra commute with its full star commutant, not just with individual row generators.
```
lemma bufferAlgebra_commutes_commutant (r : ℕ → E)
    (x : StarSubalgebra.centralizer ℂ (Set.range r))
    (y : closedCanonicalRowAlgebra r) : Commute (x : E) (y : E) := by
…
```
Mentions: OAI.WeakPureInfiniteness.closedCanonicalRowAlgebra

lemma OAI.WeakPureInfiniteness.exists_buffer_common_binary_comparison line 31

Source documentation

Restrict a full binary row in the buffer commutant and its finite buffer encoding to their actual common unit, then compare them there.

lemma exists_buffer_common_binary_comparison
    (r : ℕ → E)
    (q : StarSubalgebra.centralizer ℂ (Set.range r))
    (p : closedCanonicalRowAlgebra r)
    (hq : star q = q) (hqq : q * q = q)
    (hp : star p = p) (hpp : p * p = p)
    (hqp0 : (q : E) * (p : E) ≠ 0)
    (a : Fin 2 → StarSubalgebra.centralizer ℂ (Set.range r))
    (b : Fin 2 → closedCanonicalRowAlgebra r)
    (ha : ∀ i j, star (a i) * a j = if i = j then q else 0)
    (hb : ∀ i j, star (b i) * b j = if i = j then p else 0)
    (has : (∑ i, a i * star (a i)) = q)
…

Mentions: OAI.WeakPureInfiniteness.closedCanonicalRowAlgebra

lemma OAI.WeakPureInfiniteness.exists_zeroUnit_buffer_comparison_with_unit line 95

Source documentation

Compare the finite encoding of a zero-unit row with the actual negative buffer row. Both a complement isometry and an isometry inside the initial corner are retained as concrete data. The resulting ambient unitary is connected to one; this does not compare the original unsplit generators.

lemma exists_zeroUnit_buffer_comparison_with_unit [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)
    (a : Fin 2 → StarSubalgebra.centralizer ℂ (Set.range r))
    (ha : ∀ i j, star (a i) * a j = if i = j then q else 0)
    (has : (∑ i, a i * star (a i)) = q)
    (m : ℕ) (ε : ℝ) (hε : 0 < ε) :
    ∃ u : unitary E, Joined (1 : unitary E) u ∧
…

lemma OAI.WeakPureInfiniteness.exists_zeroUnit_buffer_comparison line 309

Source documentation

The comparison-only form preserves the original finite interface.

lemma exists_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)
    (a : Fin 2 → StarSubalgebra.centralizer ℂ (Set.range r))
    (ha : ∀ i j, star (a i) * a j = if i = j then q else 0)
    (has : (∑ i, a i * star (a i)) = q)
    (m : ℕ) (ε : ℝ) (hε : 0 < ε) :
    ∃ u : unitary E, Joined (1 : unitary E) u ∧
…