ClockCocycleFamily.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Finite families of clocked cocycle contractions

A single joint partition must control every coefficient homotopy. The maximum cocycle length is fixed before the clock and all error tolerances are chosen. The final theorem constructs the finite family on that one partition; it makes no choice of independent towers for different lengths.

def OAI.WeakPureInfiniteness.clockCocycleCost line 20
lemma OAI.WeakPureInfiniteness.clockCocycleCost_pos line 24
lemma OAI.WeakPureInfiniteness.family_product_commutator line 28

lemma OAI.WeakPureInfiniteness.clocked_cocycle_path_on_partition line 44

Source documentation

Finite fragmentation is applied to the supplied partition; only its actual mixed quarter paths are needed.

lemma clocked_cocycle_path_on_partition (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) {N : ℕ} (e : ZMod N → E)
    (he : ∀ j, IsStarProjection (e j)) (η : ℝ) (hη : 0 < η)
    (hS : ∀ j, ‖finiteRowShift s (e j) - e (j + 1)‖ ≤ η)
    (hT : ∀ j, ‖finiteRowShift t (e j) - e (j + 1)‖ ≤ η) (n : ℕ)
    (hquarter : ∀ i r l : Fin 2, i ≠ l → ∃ p : Path
      (binaryCornerUnitary (s i * s r)
        (binaryProduct_isometry _ _ (by simpa using hs i i) (by simpa using hs r r))
…

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

lemma OAI.WeakPureInfiniteness.family_isometry_norm line 149
lemma OAI.WeakPureInfiniteness.family_near_commutator line 155

lemma OAI.WeakPureInfiniteness.exists_joint_clocked_quarter_family_angular line 170

Source documentation

A single clock supplies all mixed quarter paths up to the prescribed finite length.

lemma exists_joint_clocked_quarter_family_angular [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 M : ℕ) (ε : ℝ) (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

lemma OAI.WeakPureInfiniteness.exists_joint_clocked_quarter_family line 286

lemma OAI.WeakPureInfiniteness.exists_joint_clocked_cocycle_family line 333

Source documentation

One actual joint partition controls every cocycle path in the chosen finite range. Both errors are selected after that range and the tower height have been fixed.

lemma exists_joint_clocked_cocycle_family [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 M : ℕ) (ε : ℝ) (hε : 0 < ε) :
    ∃ e : ZMod (2 ^ m) → E,
      (∀ j, IsStarProjection (e j)) ∧ (∑ j, e j) = 1 ∧
      (∀ j l, j ≠ l → e j * e l = 0) ∧
      (∀ j, ‖finiteRowShift s (e j) - e (j + 1)‖ < ε) ∧
      (∀ j, ‖finiteRowShift t (e j) - e (j + 1)‖ < ε) ∧
      ∀ n : ℕ, n ≤ M → ∃ p : Path (binaryRowCocycleUnitary s t hs ht hsum htsum n) 1,
…

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