ClockedCancellation.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Actual clock-corrected quarter paths on the joint tower

The clock removes the two off-diagonal transport degrees of the actual length-two/length-one cancellation. Every surviving commutator is bounded from the supplied rows and the actual joint cyclic partition.

lemma OAI.WeakPureInfiniteness.clock_left_commutator_norm line 19
lemma OAI.WeakPureInfiniteness.clockDegreeCorrection_one_commutator line 28
lemma OAI.WeakPureInfiniteness.clockDegreeCorrection_neg_one_commutator line 39
lemma OAI.WeakPureInfiniteness.clocked_isometry_norm line 49

lemma OAI.WeakPureInfiniteness.clockCorrectedCancellation_cell_commutator line 56

Source documentation

The two corrected off-diagonal terms now have degree zero with respect to the actual cyclic cells.

lemma clockCorrectedCancellation_cell_commutator {N : ℕ} [NeZero N]
    (k : unitary E) (e : ZMod N → E) (he : ∀ j, star (e j) = e j)
    (hk : ∀ j, (k : E) * e j = e (j + 1) * (k : E))
    (a b : E) (u : unitary E) (ha : star a * a = 1) (hb : star b * b = 1)
    (δ : ℝ) (hδ : 0 ≤ δ)
    (hat : ∀ j, ‖a * e j - e (j + 2) * a‖ ≤ δ)
    (hbt : ∀ j, ‖b * e j - e (j + 1) * b‖ ≤ δ)
    (hut : ∀ j, ‖(u : E) * e j - e j * (u : E)‖ ≤ δ)
    (θ : ℝ) (j : ZMod N) :
    ‖clockCorrectedCancellation k a b u θ * e j -
      e j * clockCorrectedCancellation k a b u θ‖ ≤ 20 * δ := by
…

Mentions: OAI.WeakPureInfiniteness.clockCorrectedCancellation

lemma OAI.WeakPureInfiniteness.clocked_near_commutator line 139

lemma OAI.WeakPureInfiniteness.exists_joint_clocked_quarter_paths line 155

Source documentation

Actual quarter-cancellation paths for every relevant pair of source words, on one jointly constructed clock and cyclic partition. The path, its endpoints, cell commutators and sample bound are all supplied here.

lemma exists_joint_clocked_quarter_paths [Nontrivial E] (s t : Fin 2 → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (ht : ∀ i j, star (t i) * t j = if i = j then 1 else 0)
    (hsum : (∑ i, s i * star (s i)) = 1)
    (htsum : (∑ i, t i * star (t i)) = 1)
    (hcomm : bergRowsCommute s t) (m n : ℕ) (ε : ℝ) (hε : 0 < ε) :
    ∃ (k : unitary E) (e : ZMod (2 ^ m) → E),
      (k : E) ^ (2 ^ m) = 1 ∧
      (∀ j, IsStarProjection (e j)) ∧ (∑ j, e j) = 1 ∧
      (∀ j l, j ≠ l → e j * e l = 0) ∧
      (∀ j, (k : E) * e j = e (j + 1) * (k : E)) ∧
      ‖finiteRowShift s k - (k : E)‖ < ε ∧
…

Mentions: OAI.WeakPureInfiniteness.bergRowsCommute, OAI.WeakPureInfiniteness.finiteRowShift