CornerShortPath.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Closing the small stabilization gap

The principal-argument path between unitary elements at distance less than 2 has speed at most π. Thus the middle gap in the finite corner construction is closed by a genuine path with a uniform bound. The fixed corner hypotheses are retained.

lemma OAI.WeakPureInfiniteness.selfAdjoint_expUnitary_sub_one_norm_le line 20
lemma OAI.WeakPureInfiniteness.selfAdjoint_expUnitary_sub_norm_le line 32
lemma OAI.WeakPureInfiniteness.unitary_shortPath_sub_norm_le line 51
lemma OAI.WeakPureInfiniteness.exists_controlled_unitary_shortPath line 68
Source documentation
The principal-argument bridge closes the actual middle gap, with a uniform speed bound independent of the two endpoint unitaries.
```
lemma exists_controlled_unitary_shortPath (u v : unitary E)
    (huv : ‖(u : E) - v‖ < 2) :
    ∃ p : Path u v, ∀ t s, ‖(p t : E) - p s‖ ≤ Real.pi * |(t : ℝ) - s| := by
…
```

lemma OAI.WeakPureInfiniteness.unitaryPath_trans_sub_norm_le line 75

Source documentation

Concatenating two uniformly controlled paths costs only the time rescaling.

lemma unitaryPath_trans_sub_norm_le {a b c : unitary E}
    (p : Path a b) (q : Path b c) (L : ℝ)
    (hp : ∀ t s, ‖(p t : E) - p s‖ ≤ L * |(t : ℝ) - s|)
    (hq : ∀ t s, ‖(q t : E) - q s‖ ≤ L * |(t : ℝ) - s|) :
    ∀ t s, ‖((p.trans q) t : E) - (p.trans q) s‖ ≤ 2 * L * |(t : ℝ) - s| := by
…

def OAI.WeakPureInfiniteness.unitaryQuarterPath line 120
Source documentation
Restrict a uniformly controlled angular path to its quarter-turn interval.
```
def unitaryQuarterPath (u : ℝ → unitary E) (hu : Continuous u) :
    Path (u 0) (u (Real.pi / 2)) where
…
```
lemma OAI.WeakPureInfiniteness.unitaryQuarterPath_sub_norm_le line 127

lemma OAI.WeakPureInfiniteness.exists_uniform_compressed_unitary_path line 140

Source documentation

The small middle gap is closed, yielding a uniformly controlled genuine path for the compressed unitary. The fixed corner hypotheses are explicit.

lemma exists_uniform_compressed_unitary_path (q a b z : E)
    (hqstar : star q = q) (hqq : q * q = q)
    (haa : star a * a = q) (hbb : star b * b = q) (hab : star a * b = 0)
    (hsum : a * star a + b * star b = q)
    (hqz : q * z = z) (hzq : z * q = z)
    (hzz : star z * z = q) (hzz' : z * star z = q)
    (δ : ℝ) (hδ : 0 ≤ δ) (hsmall : 4 * δ < 2)
    (haz : ‖z * a - a * z‖ ≤ δ) (hbz : ‖z * b - b * z‖ ≤ δ) :
    ∃ u : unitary E, (u : E) = cornerCompression a z ∧
      ∃ p : Path u 1, ∀ t s, ‖(p t : E) - p s‖ ≤ (8 * Real.pi) * |(t : ℝ) - s| := by
…

Mentions: OAI.WeakPureInfiniteness.cornerCompression