JointWordCycle.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Joint word rows and their finite coordinate cycle

The row consists of n source letters followed by one target letter. Its coordinate cycle is a finite matrix permutation, with a path bound independent of n. Identifying a different cocycle with this permutation requires an equality; no nonzero-gauge cocycle is silently substituted.

def OAI.WeakPureInfiniteness.finiteJointWord line 20
lemma OAI.WeakPureInfiniteness.sum_finFunction_succ line 25
lemma OAI.WeakPureInfiniteness.finiteJointWord_support line 34
lemma OAI.WeakPureInfiniteness.finiteJointWord_gram line 56
lemma OAI.WeakPureInfiniteness.finiteJointWord_sum line 94

lemma OAI.WeakPureInfiniteness.exists_controlled_jointWordCycle_path line 123

Source documentation

The actual coordinate permutation of the joint word row has a uniform path, independently of the number of source letters.

lemma exists_controlled_jointWordCycle_path [Nontrivial E]
    (q : E) (s t : I → E) (hqstar : star q = q) (hqq : q * q = q)
    (hs : ∀ i j, star (s i) * s j = if i = j then q else 0)
    (ht : ∀ i j, star (t i) * t j = if i = j then q else 0)
    (hsum : (∑ i, s i * star (s i)) = q)
    (htsum : (∑ i, t i * star (t i)) = q) (n : ℕ) :
    ∃ p : Path (1 : unitary E)
        (finiteRowPermutationUnitary q (finiteJointWord s t n) hqstar hqq
          (finiteJointWord_gram q s t hqstar hqq hs ht hsum htsum n)
          (finiteJointWord_sum q s t hqstar hqq hs hsum htsum n)
          (finiteCoordinateCycle (n + 1))),
      ∀ a b, ‖(p a : E) - p b‖ ≤ (4 * Real.pi) * |(a : ℝ) - b| := by
…

Mentions: OAI.WeakPureInfiniteness.finiteRowPermutationUnitary, OAI.WeakPureInfiniteness.finiteJointWord, OAI.WeakPureInfiniteness.finiteJointWord_gram, OAI.WeakPureInfiniteness.finiteJointWord_sum, OAI.WeakPureInfiniteness.finiteCoordinateCycle