BergRotation.lean`

37 declarations, 0 contain sorry, 0 declared as axioms

Corner rotations for the O∞ half-flip boundary

A square-zero partial isometry determines a genuine rotation between its orthogonal initial and final corners. The formulas below retain the terminal corner explicitly. They do not assert that a finite recursive tower has a small terminal defect.

def OAI.WeakPureInfiniteness.bergSupport line 21
Source documentation
The sum of the orthogonal initial and final projections.
```
def bergSupport (a : E) : E := star a * a + a * star a
```
def OAI.WeakPureInfiniteness.bergSkew line 24
Source documentation
The skew-adjoint generator of the corner rotation.
```
def bergSkew (a : E) : E := a - star a
```
lemma OAI.WeakPureInfiniteness.berg_word_relations line 26
lemma OAI.WeakPureInfiniteness.bergSupport_star line 41
lemma OAI.WeakPureInfiniteness.bergSkew_star line 44
lemma OAI.WeakPureInfiniteness.bergSupport_sq line 48
lemma OAI.WeakPureInfiniteness.bergSkew_sq line 54
lemma OAI.WeakPureInfiniteness.bergSupport_mul_skew line 61
lemma OAI.WeakPureInfiniteness.bergSkew_mul_support line 70
def OAI.WeakPureInfiniteness.bergRotationCore line 78
Source documentation
Polynomial form of a rotation; c and s will be cosine and sine.
```
def bergRotationCore (a : E) (c s : ℝ) : E :=
…
```
lemma OAI.WeakPureInfiniteness.bergRotationCore_star line 81
lemma OAI.WeakPureInfiniteness.bergRotationCore_one_zero line 86
lemma OAI.WeakPureInfiniteness.bergRotationCore_mul line 90
def OAI.WeakPureInfiniteness.partialIsometryBergRotation line 114
Source documentation
Rotate from the initial corner toward the final corner by angle θ.
```
def partialIsometryBergRotation (a : E) (θ : ℝ) : E :=
…
```
lemma OAI.WeakPureInfiniteness.partialIsometryBergRotation_star line 117
lemma OAI.WeakPureInfiniteness.partialIsometryBergRotation_mul line 121
lemma OAI.WeakPureInfiniteness.partialIsometryBergRotation_zero line 130
lemma OAI.WeakPureInfiniteness.partialIsometryBergRotation_mem line 135
def OAI.WeakPureInfiniteness.partialIsometryBergRotationUnitary line 144
lemma OAI.WeakPureInfiniteness.partialIsometryBergRotation_continuous line 148
lemma OAI.WeakPureInfiniteness.partialIsometryBergRotationUnitary_continuous line 153
lemma OAI.WeakPureInfiniteness.partialIsometryBergRotationUnitary_joined line 160
Source documentation
The explicit angular path supplies connectedness, including the terminal quarter-turn, without selecting a logarithm.
```
lemma partialIsometryBergRotationUnitary_joined (a : E)
    (ha : a * star a * a = a) (haa : a * a = 0) (θ : ℝ) :
    Joined (1 : unitary E) (partialIsometryBergRotationUnitary a ha haa θ) := by
…
```
Mentions: OAI.WeakPureInfiniteness.partialIsometryBergRotationUnitary
lemma OAI.WeakPureInfiniteness.bergSupport_norm_le_one line 175
lemma OAI.WeakPureInfiniteness.bergSkew_norm_le_one line 182
lemma OAI.WeakPureInfiniteness.partialIsometryBergRotation_sub_norm_le line 193
Source documentation
The norm cost of changing an angular terminal boundary is at most twice its angular change, independently of the size of the ambient algebra.
```
lemma partialIsometryBergRotation_sub_norm_le (a : E)
    (ha : a * star a * a = a) (haa : a * a = 0) (θ φ : ℝ) :
    ‖partialIsometryBergRotation a θ - partialIsometryBergRotation a φ‖ ≤
      2 * |θ - φ| := by
…
```
Mentions: OAI.WeakPureInfiniteness.partialIsometryBergRotation
lemma OAI.WeakPureInfiniteness.partialIsometryBergRotation_intertwining line 221
Source documentation
Exact covariance of the two corner generators passes through the rotation polynomial. This is the local shift identity used at a tower seam.
```
lemma partialIsometryBergRotation_intertwining (a b x : E)
    (ha : x * a = b * x) (hs : x * star a = star b * x) (θ : ℝ) :
    x * partialIsometryBergRotation a θ = partialIsometryBergRotation b θ * x := by
…
```
Mentions: OAI.WeakPureInfiniteness.partialIsometryBergRotation
lemma OAI.WeakPureInfiniteness.partialIsometryBergRotation_seam_norm_le line 240
Source documentation
At a terminal seam, exact covariance leaves only the change of angle. The bound states the defect that still has to be controlled by the chosen finite tower; it does not assume that this angle change is already small.
```
lemma partialIsometryBergRotation_seam_norm_le (a b x : E)
    (hb : b * star b * b = b) (hbb : b * b = 0)
    (ha : x * a = b * x) (hs : x * star a = star b * x) (θ φ : ℝ) :
    ‖partialIsometryBergRotation b θ * x - x * partialIsometryBergRotation a φ‖ ≤
      (2 * |θ - φ|) * ‖x‖ := by
…
```
Mentions: OAI.WeakPureInfiniteness.partialIsometryBergRotation
lemma OAI.WeakPureInfiniteness.partialIsometryBergRotation_quarter_mul_initial line 252
Source documentation
The quarter-turn carries the initial projection onto the given partial isometry. This explicitly records which terminal corner is moved.
```
lemma partialIsometryBergRotation_quarter_mul_initial (a : E)
    (ha : a * star a * a = a) (haa : a * a = 0) :
    partialIsometryBergRotation a (Real.pi / 2) * (star a * a) = a := by
…
```
Mentions: OAI.WeakPureInfiniteness.partialIsometryBergRotation
def OAI.WeakPureInfiniteness.doubleBergRotation line 262
Source documentation
Two simultaneous corner rotations. The right corner is moved first.
```
def doubleBergRotation (a b : E) (θ : ℝ) : E :=
…
```
lemma OAI.WeakPureInfiniteness.doubleBergRotation_mem line 265
lemma OAI.WeakPureInfiniteness.doubleBergRotation_continuous line 272
lemma OAI.WeakPureInfiniteness.doubleBergRotation_zero line 275
lemma OAI.WeakPureInfiniteness.doubleBergRotation_sub_norm_le line 278
lemma OAI.WeakPureInfiniteness.doubleBergRotation_quarter_mul_initial line 304
lemma OAI.WeakPureInfiniteness.bergCompletion_corner_data line 317
def OAI.WeakPureInfiniteness.partialIsometryBergCompletion line 378
Source documentation
An explicit angular path completing a partial isometry through a common spare range. Only its quarter-turn endpoint is required to extend v.
```
def partialIsometryBergCompletion (v r : E) (θ : ℝ) : E :=
…
```

lemma OAI.WeakPureInfiniteness.exists_controlled_berg_completion_path line 382

Source documentation

The completion path is uniformly controlled in its angular parameter.

lemma exists_controlled_berg_completion_path (v r : E)
    (hv : v * star v * v = v) (hr : star r * r = 1)
    (hpr : (star v * v) * r = 0) (hqr : (v * star v) * r = 0) :
    ∃ u : ℝ → unitary E, Continuous u ∧ (u 0 : E) = 1 ∧
      (u (Real.pi / 2) : E) * (star v * v) = v ∧
      (∀ θ, (u θ : E) = partialIsometryBergCompletion v r θ) ∧
      ∀ θ φ, ‖(u θ : E) - u φ‖ ≤ 4 * |θ - φ| := by
…

Mentions: OAI.WeakPureInfiniteness.partialIsometryBergCompletion