CornerStabilization.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Two controlled stabilization paths

The first path adds a cancelling pair on the two spare branches. The second contracts the folded pair. Their endpoints differ by at most four times the commutator error. The common corner and the ambient complement remain explicit; no central corner for an arbitrary growing cocycle is asserted.

lemma OAI.WeakPureInfiniteness.orthogonal_extension_mul line 20
lemma OAI.WeakPureInfiniteness.cornerCompression_pair_product line 37
lemma OAI.WeakPureInfiniteness.cornerCompression_triple_product line 46
def OAI.WeakPureInfiniteness.cornerStabilizationFirstPath line 69
Source documentation
Add an adjoint-cancelling pair to the two spare branches.
```
def cornerStabilizationFirstPath (a b z : E) (θ : ℝ) : E :=
…
```
def OAI.WeakPureInfiniteness.cornerStabilizationSecondPath line 73
Source documentation
Contract the folded first two branches against the third branch.
```
def cornerStabilizationSecondPath (a b z : E) (θ : ℝ) : E :=
…
```
lemma OAI.WeakPureInfiniteness.projection_norm_bound line 76
lemma OAI.WeakPureInfiniteness.relative_isometry_norm_bound line 83

lemma OAI.WeakPureInfiniteness.exists_controlled_cornerStabilization_paths line 91

Source documentation

The two explicit controlled paths leave precisely the small endpoint gap. Their common relative unit is the supplied projection q.

lemma exists_controlled_cornerStabilization_paths (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 ≤ δ)
    (haz : ‖z * a - a * z‖ ≤ δ) (hbz : ‖z * b - b * z‖ ≤ δ) :
    ∃ u v : ℝ → unitary E, Continuous u ∧ Continuous v ∧
      (u 0 : E) = cornerCompression a z ∧ (v (Real.pi / 2) : E) = 1 ∧
      ‖(u (Real.pi / 2) : E) - v 0‖ ≤ 4 * δ ∧
      (∀ θ φ, ‖(u θ : E) - u φ‖ ≤ 4 * |θ - φ|) ∧
…

Mentions: OAI.WeakPureInfiniteness.cornerCompression