MixedNegative.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Mixed stabilization in the explicit zero-unit corner

The row t₁ sᵢ t₁* + tᵢ₊₂ p is the direct sum of the source row and the negative target corner, with unit 1 - t₀t₀*. Its Gram and support formulas do not require the two rows to commute. The comparison below uses the actual third buffer and retains the exact corner transport; it does not cancel the negative summand or claim ambient half-flip.

def OAI.WeakPureInfiniteness.mixedNegativeRow line 23
lemma OAI.WeakPureInfiniteness.mixedNegativeRow_self line 26
lemma OAI.WeakPureInfiniteness.mixedNegativeRow_gram line 29
lemma OAI.WeakPureInfiniteness.mixedNegativeRow_support line 71
lemma OAI.WeakPureInfiniteness.mixedNegativeRow_commutes line 87
lemma OAI.WeakPureInfiniteness.mixedNegativeRow_coe line 94
lemma OAI.WeakPureInfiniteness.map_canonicalTailProjection line 102
lemma OAI.WeakPureInfiniteness.map_mixedNegativeRow line 107
lemma OAI.WeakPureInfiniteness.map_canonicalNegativeRow line 113

lemma OAI.WeakPureInfiniteness.exists_mixedNegative_buffer_comparison line 120

Source documentation

Both rows are compared through the same actual buffer. The resulting ambient connected unitary preserves the mixed row's unit exactly.

lemma exists_mixedNegative_buffer_comparison [Nontrivial E]
    (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)
    (n : ℕ) (ε : ℝ) (hε : 0 < ε) :
    ∃ u : unitary E, Joined (1 : unitary E) u ∧
      (u : E) * canonicalTailProjection (fun j => (t j : E)) 1 * star (u : E) =
        canonicalTailProjection (fun j => (t j : E)) 1 ∧
      ∀ i : Fin (n + 1),
        ‖(u : E) * mixedNegativeRow (fun j => (s j : E)) (fun j => (t j : E)) i *
…

Mentions: OAI.WeakPureInfiniteness.canonicalTailProjection, OAI.WeakPureInfiniteness.mixedNegativeRow

lemma OAI.WeakPureInfiniteness.exists_mixedNegative_factor_ultrapower_comparison line 221
Source documentation
The third row is constructed, not assumed: the two commuting factor images admit mixed stabilization in their actual norm ultrapower.
```
lemma exists_mixedNegative_factor_ultrapower_comparison [Nontrivial E]
    (U : Ultrafilter ℕ) [Fact ((U : Filter ℕ) ≤ Filter.atTop)]
    (f g : OInfinity →⋆ₐ[ℂ] E) (hfg : ∀ x y, Commute (f x) (g y))
    (n : ℕ) (ε : ℝ) (hε : 0 < ε) :
    let d := NormUltra.QuotientAlgebra.diagonalHom (A := E) U
…
```
Mentions: OAI.WeakPureInfiniteness.OInfinity, OAI.NormUltra.QuotientAlgebra.diagonalHom
lemma OAI.WeakPureInfiniteness.exists_connected_mixedNegative_factor_comparison line 275
Source documentation
Finite mixed comparison descends to a connected ambient unitary. The corner is preserved to the requested tolerance; its complement is retained.
```
lemma exists_connected_mixedNegative_factor_comparison [Nontrivial E]
    (U : Ultrafilter ℕ) [Fact ((U : Filter ℕ) ≤ Filter.atTop)]
    (f g : OInfinity →⋆ₐ[ℂ] E) (hfg : ∀ x y, Commute (f x) (g y))
    (n : ℕ) (ε : ℝ) (hε : 0 < ε) :
    let s := fun i => f (oInfinityIsometry i)
…
```
Mentions: OAI.WeakPureInfiniteness.OInfinity, OAI.WeakPureInfiniteness.oInfinityIsometry