CornerContraction.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Finite stabilization in a coisometric two-generator corner

Splitting one range gives three branches. Folding the first two branches back into one gives another coisometric pair. This is the algebraic step behind a bounded rotation contraction of a compressed unitary. The corner unit stays q; no assertion removes its ambient complement.

def OAI.WeakPureInfiniteness.cornerThreeBranch line 21
def OAI.WeakPureInfiniteness.cornerPairFold line 23
lemma OAI.WeakPureInfiniteness.cornerThreeBranch_gram line 30
lemma OAI.WeakPureInfiniteness.cornerThreeBranch_sum line 46
lemma OAI.WeakPureInfiniteness.cornerPairFold_properties line 56
lemma OAI.WeakPureInfiniteness.corner_sandwich_norm_le line 106

lemma OAI.WeakPureInfiniteness.cornerPairFold_conjugation_error line 118

Source documentation

Folding errors are controlled by the two source commutators, independently of the ambient algebra or the unitary's path length.

lemma cornerPairFold_conjugation_error (q a b e f z : E)
    (haa : star a * a = q) (hbb : star b * b = q) (hab : star a * b = 0)
    (hqz : q * z = z) (ha : ‖a‖ ≤ 1) (hb : ‖b‖ ≤ 1) (he : ‖e‖ ≤ 1) (hf : ‖f‖ ≤ 1)
    (δ : ℝ) (hδ : 0 ≤ δ)
    (haz : ‖z * a - a * z‖ ≤ δ) (hbz : ‖z * b - b * z‖ ≤ δ) :
    ‖(e * star a + f * star b) * z * star (e * star a + f * star b) -
      (e * z * star e + f * z * star f)‖ ≤ 4 * δ := by
…