MixedSwap.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The exact three-summand permutation in mixed stabilization

The first two target ranges are exchanged by an explicit connected self-adjoint unitary. The negative corner is fixed pointwise. This gives the literal permutation used in cancellation, with the complementary representation still present.

def OAI.WeakPureInfiniteness.mixedStabilizedRow line 21
def OAI.WeakPureInfiniteness.mixedSwappedRow line 24
lemma OAI.WeakPureInfiniteness.mixed_swap_data line 27

lemma OAI.WeakPureInfiniteness.exists_connected_mixed_swap line 68

Source documentation

The actual connected flip interchanges the two full ranges and fixes the entire remaining corner, rather than merely preserving its projection.

lemma exists_connected_mixed_swap [Nontrivial E] (t : ℕ → E)
    (ht : ∀ i j, star (t i) * t j = if i = j then 1 else 0) :
    ∃ u : unitary E, Joined 1 u ∧ star (u : E) = (u : E) ∧
      (u : E) * t 0 = t 1 ∧ (u : E) * t 1 = t 0 ∧
      (u : E) * canonicalNegativeProjection t = canonicalNegativeProjection t ∧
      canonicalNegativeProjection t * (u : E) = canonicalNegativeProjection t ∧
      ∀ i, (u : E) * (t (i + 2) * canonicalNegativeProjection t) =
        t (i + 2) * canonicalNegativeProjection t := by
…

Mentions: OAI.WeakPureInfiniteness.canonicalNegativeProjection

lemma OAI.WeakPureInfiniteness.exists_connected_mixed_stabilization_permutation line 122
Source documentation
A fixed connected unitary performs the full three-summand permutation, for every source row and every generator simultaneously.
```
lemma exists_connected_mixed_stabilization_permutation [Nontrivial E] (t : ℕ → E)
    (ht : ∀ i j, star (t i) * t j = if i = j then 1 else 0) :
    ∃ u : unitary E, Joined 1 u ∧
      ∀ (s : ℕ → E) i, (u : E) * mixedStabilizedRow s t i * star (u : E) =
        mixedSwappedRow s t i := by
…
```
Mentions: OAI.WeakPureInfiniteness.mixedStabilizedRow, OAI.WeakPureInfiniteness.mixedSwappedRow