TransportedBuffer.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Transporting the explicit absorption anchor

The canonical Fock split transports its corner by a connected unitary, but transports its complementary isometry by left multiplication. This asymmetric transport still preserves connectedness of the absorption anchor: its anchor is conjugate to a value of the original rotation path.

def OAI.WeakPureInfiniteness.BufferAbsorptionCorner.transported line 25
Source documentation
Corner coefficients are conjugated, whereas the complementary isometry is moved by left multiplication, as in the finite Fock split.
```
def transported (D : BufferAbsorptionCorner E) (u : unitary E) : BufferAbsorptionCorner E := by
…
```
Mentions: OAI.WeakPureInfiniteness.BufferAbsorptionCorner
lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.transported_q line 61
lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.transported_w line 64
lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.transported_a line 67
lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.transported_b line 70
lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.transported_anchor line 74
Source documentation
Exact asymmetric transport identity for the anchor.
```
lemma transported_anchor (D : BufferAbsorptionCorner E) (u : unitary E) :
    (D.transported u).anchor = u * D.rotation u * star u := by
…
```
Mentions: OAI.WeakPureInfiniteness.BufferAbsorptionCorner, OAI.WeakPureInfiniteness.BufferAbsorptionCorner.anchor
lemma OAI.WeakPureInfiniteness.BufferAbsorptionCorner.transported_anchor_joined line 97
Source documentation
The anchor remains connected for the actual transported Fock corner; no path in a corner stabilizer is inferred from an ambient endpoint.
```
lemma transported_anchor_joined (D : BufferAbsorptionCorner E) (u : unitary E)
    (hD : Joined (1 : unitary E) D.anchor) (hu : Joined (1 : unitary E) u) :
    Joined (1 : unitary E) (D.transported u).anchor := by
…
```
Mentions: OAI.WeakPureInfiniteness.BufferAbsorptionCorner, OAI.WeakPureInfiniteness.BufferAbsorptionCorner.anchor