NegativeComparison.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Comparison of stabilized canonical rows on their common corner

The finite binary encodings are constructed inside the two closed row algebras. Restriction to the product of their units gives commuting full binary rows, so the proved connected binary comparison applies. The two complementary corners are retained; this is not yet the global half-flip.

lemma OAI.WeakPureInfiniteness.zeroCornerRow_castSucc line 21

def OAI.WeakPureInfiniteness.commutingProjectionRestriction line 35

Source documentation

Multiplication by a commuting projection is a genuine nonunital star hom.

def commutingProjectionRestriction (C : StarSubalgebra ℂ E) (q : E)
    (hq : star q = q) (hqq : q * q = q) (hc : ∀ x : C, Commute (x : E) q) :
    C →⋆ₙₐ[ℂ] E where
…

lemma OAI.WeakPureInfiniteness.nonunital_map_pow_mul line 54
lemma OAI.WeakPureInfiniteness.canonicalTailProjection_coe line 60
lemma OAI.WeakPureInfiniteness.canonicalNegativeRow_coe line 66
lemma OAI.WeakPureInfiniteness.exists_relative_binary_power_conjugacy line 73

lemma OAI.WeakPureInfiniteness.canonicalCommonCorner_nonzero line 92

Source documentation

The product of the two first-tail units is nonzero: it contains the range of the literal isometry s₁t₁.

lemma canonicalCommonCorner_nonzero [Nontrivial E]
    (s t : ℕ → E)
    (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)
    (hc : bergRowsCommute s t) :
    canonicalTailProjection s 1 * canonicalTailProjection t 1 ≠ 0 := by
…

Mentions: OAI.WeakPureInfiniteness.bergRowsCommute, OAI.WeakPureInfiniteness.canonicalTailProjection

lemma OAI.WeakPureInfiniteness.restrict_commuting_binary_rows line 124

Source documentation

Restrict two full binary rows in commuting algebras to the product of their units. Both the Gram relations and cross commutation are exact.

lemma restrict_commuting_binary_rows
    (C D : StarSubalgebra ℂ E) [IsClosed (C : Set E)] [IsClosed (D : Set E)]
    (hc : ∀ x : C, ∀ y : D, Commute (x : E) (y : E))
    (p : C) (q : D) (hp : star p = p) (hpp : p * p = p)
    (hq : star q = q) (hqq : q * q = q)
    (a : Fin 2 → C) (b : Fin 2 → D)
    (ha : ∀ i j, star (a i) * a j = if i = j then p else 0)
    (hb : ∀ i j, star (b i) * b j = if i = j then q else 0)
    (has : (∑ i, a i * star (a i)) = p)
    (hbs : (∑ i, b i * star (b i)) = q) :
    let f := commutingProjectionRestriction C (q : E)
…

Mentions: OAI.WeakPureInfiniteness.commutingProjectionRestriction

lemma OAI.WeakPureInfiniteness.exists_canonicalNegative_common_comparison line 190

Source documentation

Actual finite stabilized-row comparison on the common corner. The unitary is connected to one and fixes the complementary identity exactly.

lemma exists_canonicalNegative_common_comparison [Nontrivial E]
    (C D : StarSubalgebra ℂ E) [IsClosed (C : Set E)] [IsClosed (D : Set E)]
    (hc : ∀ x : C, ∀ y : D, Commute (x : E) (y : E))
    (s : ℕ → C) (t : ℕ → D)
    (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)
    (m : ℕ) (ε : ℝ) (hε : 0 < ε) :
    let S : ℕ → E := fun i => s i
…

def OAI.WeakPureInfiniteness.closedCanonicalRowAlgebra line 291
Source documentation
The closed unital algebra generated by the complete canonical row.
```
def closedCanonicalRowAlgebra (s : ℕ → E) : StarSubalgebra ℂ E :=
…
```
instance OAI.WeakPureInfiniteness.closedCanonicalRowAlgebra_isClosed line 294
lemma OAI.WeakPureInfiniteness.mem_closedCanonicalRowAlgebra line 298
lemma OAI.WeakPureInfiniteness.closedCanonicalRowAlgebras_commute line 302

lemma OAI.WeakPureInfiniteness.exists_canonicalNegative_comparison line 321

Source documentation

No chosen binary encodings or commutant assumptions remain in this application to the original two commuting canonical rows.

lemma exists_canonicalNegative_comparison [Nontrivial E]
    (s t : ℕ → E)
    (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)
    (hc : bergRowsCommute s t) (m : ℕ) (ε : ℝ) (hε : 0 < ε) :
    let P := canonicalTailProjection s 1
…

Mentions: OAI.WeakPureInfiniteness.bergRowsCommute, OAI.WeakPureInfiniteness.canonicalTailProjection