JointClock.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A clock on the actual joint cyclic partition

The clock lies in the source-row algebra. Its source partition is convolved with a target-row partition. Thus the clock cycles the joint partition exactly, while both row endomorphisms shift that same partition approximately. The construction does not replace the joint partition by a source-only one.

lemma OAI.WeakPureInfiniteness.jointRohlinProjection_clock line 20
lemma OAI.WeakPureInfiniteness.exists_binary_clock_in line 41

lemma OAI.WeakPureInfiniteness.exists_joint_binary_clock line 72

Source documentation

Actual joint partition and its exact finite-order clock. Every object comes from the two specified commuting full binary rows.

lemma exists_joint_binary_clock (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)
    (hc : bergRowsCommute s t) (m : ℕ) (ε : ℝ) (hε : 0 < ε) :
    ∃ (u : E) (e : ZMod (2 ^ m) → E),
      u ∈ unitary E ∧ u ^ (2 ^ m) = 1 ∧
      (∀ k, IsStarProjection (e k)) ∧ (∑ k, e k) = 1 ∧
      (∀ k l, k ≠ l → e k * e l = 0) ∧
      (∀ k, u * e k = e (k + 1) * u) ∧
      ‖finiteRowShift s u - u‖ < ε ∧
…

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