TailCancellationWitness.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The zero corner containing the entire remaining source copy

The internal isometry z has range inside the absorption corner. Its complement contains both the full residual source copy and a negative part of the target copy. All data below are constructed in the first buffer's commutant before applying the second-buffer comparison.

def OAI.WeakPureInfiniteness.BufferAbsorptionCorner.map line 23

lemma OAI.WeakPureInfiniteness.exists_tail_cancellation_reference line 45

Source documentation

The new comparison corner is genuinely a zero corner: its full binary row comes from the internal isometry and two orthogonal copies inside the original residual range.

lemma exists_tail_cancellation_reference [Nontrivial E]
    (D : BufferAbsorptionCorner E) (s : ℕ → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (z : E) (hz : star z * z = 1) (hqz : D.q * z = z) :
    (1 - z * star z) ≠ 0 ∧ ∃ b : Fin 2 → E,
      (∀ i j, star (b i) * b j = if i = j then 1 - z * star z else 0) ∧
      (∑ i, b i * star (b i)) = 1 - z * star z := by
…

Mentions: OAI.WeakPureInfiniteness.BufferAbsorptionCorner

lemma OAI.WeakPureInfiniteness.exists_buffered_tail_cancellation line 86

Source documentation

The second buffer compares the entire residual source representation with the complementary target corner, while fixing the retained full subcorner pointwise.

lemma exists_buffered_tail_cancellation [Nontrivial E]
    (U : Ultrafilter ℕ) [Fact ((U : Filter ℕ) ≤ atTop)]
    (R : ℕ → E) (hR : ∀ i j, star (R i) * R j = if i = j then 1 else 0)
    (D : BufferAbsorptionCorner (StarSubalgebra.centralizer ℂ (Set.range R)))
    (s t : ℕ → StarSubalgebra.centralizer ℂ (Set.range R))
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (ht : ∀ i j, star (t i) * t j = if i = j then 1 else 0)
    (z : StarSubalgebra.centralizer ℂ (Set.range R))
    (hz : star z * z = 1) (hqz : D.q * z = z)
    (hqt : ∀ i, Commute D.q (t i))
    (hzt : ∀ i, Commute z (t i) ∧ Commute (star z) (t i))
    (n : ℕ) (ε : ℝ) (hε : 0 < ε) :
…

Mentions: OAI.WeakPureInfiniteness.BufferAbsorptionCorner

lemma OAI.WeakPureInfiniteness.exists_buffered_commuting_rows_conjugacy line 160

Source documentation

Two commuting proper rows in the first buffer's commutant admit actual connected finite conjugacy in the next norm ultrapower.

lemma exists_buffered_commuting_rows_conjugacy [Nontrivial E]
    (U : Ultrafilter ℕ) [Fact ((U : Filter ℕ) ≤ atTop)]
    (R : ℕ → E) (hR : ∀ i j, star (R i) * R j = if i = j then 1 else 0)
    (s t : ℕ → StarSubalgebra.centralizer ℂ (Set.range R))
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (ht : ∀ i j, star (t i) * t j = if i = j then 1 else 0)
    (hst : bergRowsCommute s t) (n : ℕ) (ε : ℝ) (hε : 0 < ε) :
    let d := NormUltra.QuotientAlgebra.diagonalHom (A := E) U
…

Mentions: OAI.WeakPureInfiniteness.bergRowsCommute, OAI.NormUltra.QuotientAlgebra.diagonalHom