MixedTower.lean`

26 declarations, 0 contain sorry, 0 declared as axioms

Two commuting Cuntz rows and their finite rectangular towers

The transfer partial isometry moves one source layer into one target layer. The source and target rectangles, and their terminal strips, remain explicit. These identities do not yet identify the two complete terminal tails by a unitary that intertwines both rows.

def OAI.WeakPureInfiniteness.bergRowsCommute line 21
Source documentation
The tensor-factor commutation relations, including adjoints.
```
def bergRowsCommute (s : I → E) (t : J → E) : Prop :=
…
```
lemma OAI.WeakPureInfiniteness.bergRowsCommute_symm line 24

lemma OAI.WeakPureInfiniteness.bergMixedFinitePartition line 32

Source documentation

The finite rectangle decomposition retains both terminal strips and their intersection. No convergence or vanishing boundary is asserted.

lemma bergMixedFinitePartition (φ ψ : E →⋆ₙₐ[ℂ] E) (N M : ℕ) :
    ((∑ k ∈ Finset.range N, ∑ l ∈ Finset.range M,
        bergTowerLayer φ k * bergTowerLayer ψ l) +
      (∑ k ∈ Finset.range N, bergTowerLayer φ k * bergTowerTail ψ M)) +
      ((∑ l ∈ Finset.range M, bergTowerTail φ N * bergTowerLayer ψ l) +
        bergTowerTail φ N * bergTowerTail ψ M) = 1 := by
…

Mentions: OAI.WeakPureInfiniteness.bergTowerLayer, OAI.WeakPureInfiniteness.bergTowerTail

lemma OAI.WeakPureInfiniteness.bergTail_commutes_generators line 48
lemma OAI.WeakPureInfiniteness.bergLayer_commutes_generators line 69
lemma OAI.WeakPureInfiniteness.bergTails_commute line 81
lemma OAI.WeakPureInfiniteness.bergLayers_commute line 97

def OAI.WeakPureInfiniteness.bergRectangle line 109

Source documentation

One rectangle in the product of the two orthogonal layer towers.

def bergRectangle (s : I → E) (t : J → 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) (k l : ℕ) : E :=
…

lemma OAI.WeakPureInfiniteness.bergRectangle_star line 115
lemma OAI.WeakPureInfiniteness.bergRectangle_sq line 123
lemma OAI.WeakPureInfiniteness.bergRectangle_orthogonal line 140
lemma OAI.WeakPureInfiniteness.bergLayer_under_first_tail line 164
lemma OAI.WeakPureInfiniteness.bergTail_source_transfer line 182
lemma OAI.WeakPureInfiniteness.bergTail_target_transfer line 199
lemma OAI.WeakPureInfiniteness.bergTransfer_pow_source line 214
Source documentation
Transfer powers have the exact global source tails.
```
lemma bergTransfer_pow_source (m : ℕ) :
    star ((finiteCuntzTransfer s t 1) ^ m) * (finiteCuntzTransfer s t 1) ^ m =
      bergTowerTail (finiteCuntzDiagonalHom s hs) m := by
…
```
Mentions: OAI.WeakPureInfiniteness.finiteCuntzTransfer, OAI.WeakPureInfiniteness.bergTowerTail, OAI.WeakPureInfiniteness.finiteCuntzDiagonalHom
lemma OAI.WeakPureInfiniteness.bergTransfer_pow_target line 240
Source documentation
Transfer powers have the exact global target tails.
```
lemma bergTransfer_pow_target (m : ℕ) :
    (finiteCuntzTransfer s t 1) ^ m * star ((finiteCuntzTransfer s t 1) ^ m) =
      bergTowerTail (finiteCuntzDiagonalHom t ht) m := by
…
```
Mentions: OAI.WeakPureInfiniteness.finiteCuntzTransfer, OAI.WeakPureInfiniteness.bergTowerTail, OAI.WeakPureInfiniteness.finiteCuntzDiagonalHom
lemma OAI.WeakPureInfiniteness.bergLayer_source_transfer line 263
lemma OAI.WeakPureInfiniteness.bergLayer_target_transfer line 280
lemma OAI.WeakPureInfiniteness.bergRectangle_transfer line 294
Source documentation
One step preserves total layer degree and moves its separator.
```
lemma bergRectangle_transfer (k l : ℕ) :
    bergRectangle s t hs ht k (l + 1) * finiteCuntzTransfer s t 1 =
      finiteCuntzTransfer s t 1 * bergRectangle s t hs ht (k + 1) l := by
…
```
Mentions: OAI.WeakPureInfiniteness.bergRectangle, OAI.WeakPureInfiniteness.finiteCuntzTransfer
lemma OAI.WeakPureInfiniteness.bergRectangle_transfer_source line 302
lemma OAI.WeakPureInfiniteness.bergRectangle_transfer_target line 327
lemma OAI.WeakPureInfiniteness.bergRectangle_transfer_square_zero line 359
lemma OAI.WeakPureInfiniteness.bergRectangle_transfer_partial line 385
lemma OAI.WeakPureInfiniteness.exists_connected_rectangle_step line 396
Source documentation
Adjacent rectangles on a shell are related by an explicit connected quarter-turn. This is a local terminal-corner move, not yet a global flip.
```
lemma exists_connected_rectangle_step (k l : ℕ) :
    ∃ u : unitary E, Joined (1 : unitary E) u ∧
      (u : E) * bergRectangle s t hs ht (k + 1) l =
        finiteCuntzTransfer s t 1 * bergRectangle s t hs ht (k + 1) l := by
…
```
Mentions: OAI.WeakPureInfiniteness.bergRectangle, OAI.WeakPureInfiniteness.finiteCuntzTransfer
lemma OAI.WeakPureInfiniteness.exists_connected_rectangle_conjugacy line 409
lemma OAI.WeakPureInfiniteness.exists_connected_rectangle_path line 430
Source documentation
A finite sequence of connected rectangle rotations transports either endpoint of a total-degree shell to the other endpoint.
```
lemma exists_connected_rectangle_path (m k l : ℕ) :
    ∃ u : unitary E, Joined (1 : unitary E) u ∧
      (u : E) * bergRectangle s t hs ht (k + m) l * star (u : E) =
        bergRectangle s t hs ht k (l + m) := by
…
```
Mentions: OAI.WeakPureInfiniteness.bergRectangle