OAI/Analysis/OInfinity/ClockTransport.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

A finite clock for the actual CAR partition

The clock is the finite product of the occupation phase unitaries of the commuting Jordan–Wigner coordinates. It has exact dyadic order and cycles the corresponding partition. Its row commutators are controlled by the proved coordinate shift errors, independently of any cocycle equation.

  1. def OAI.WeakPureInfiniteness.carClockFactor line 21

    Source documentation

    The two occupation projections receive phases one and ζ.

    def carClockFactor (a : E) (ζ : ℂ) : E := star a * a + ζ • (a * star a)
  2. lemma OAI.WeakPureInfiniteness.clock_occupation line 23
  3. lemma OAI.WeakPureInfiniteness.carClockFactor_mem_unitary line 48
  4. lemma OAI.WeakPureInfiniteness.carClockFactor_mul_mode line 60
  5. lemma OAI.WeakPureInfiniteness.carClockFactor_commute_mode line 70
  6. lemma OAI.WeakPureInfiniteness.carClockFactor_commute line 74
  7. lemma OAI.WeakPureInfiniteness.carClockFactor_pow line 82
  8. def OAI.WeakPureInfiniteness.carClock line 95

    Source documentation

    Ordered finite product of the commuting occupation clocks.

    def carClock (a : ℕ → E) (ζ : ℕ → ℂ) : ℕ → E
  | 0 => 1
  | m + 1 => carClock a ζ m * carClockFactor (a m) (ζ m)

section Coordinates
variable (a : ℕ → E) (ζ : ℕ → ℂ)
  (hz : ∀ i, a i * a i = 0)
  (hg : ∀ i, star (a i) * a i + a i * star (a i) = 1)
  (hc : ∀ i j, Commute (a i) (a j))
  (hsc : ∀ i j, i ≠ j → Commute (star (a i)) (a j))
  (hζ : ∀ i, ‖ζ i‖ = 1)
…

    Mentions: OAI.WeakPureInfiniteness.carClockFactor

  9. lemma OAI.WeakPureInfiniteness.carClock_mem_unitary line 108
  10. lemma OAI.WeakPureInfiniteness.carClock_commute_factor line 116
  11. lemma OAI.WeakPureInfiniteness.carClock_pow_eq_one line 127
  12. lemma OAI.WeakPureInfiniteness.carClock_commute_later_mode line 137
  13. lemma OAI.WeakPureInfiniteness.carClock_mul_mode line 146
  14. lemma OAI.WeakPureInfiniteness.carClock_conjugate_mode line 171
  15. lemma OAI.WeakPureInfiniteness.clock_unitary_norm line 178
  16. lemma OAI.WeakPureInfiniteness.carClock_conjugate_spin line 185
  17. lemma OAI.WeakPureInfiniteness.carClock_conjugate_dyadic line 196
  18. lemma OAI.WeakPureInfiniteness.carClockFactor_smul line 225
  19. lemma OAI.WeakPureInfiniteness.carClockFactor_sub_norm line 233
  20. lemma OAI.WeakPureInfiniteness.carClockFactor_map line 246
  21. lemma OAI.WeakPureInfiniteness.carClock_map_shift_bound line 250
  22. def OAI.WeakPureInfiniteness.evenRohlinClock line 294

    Source documentation

    The actual occupation clock for the supplied even row.

    def evenRohlinClock {n : ℕ} (r : Fin 2 × Fin n → E) (L m : ℕ) : E :=
…
  23. lemma OAI.WeakPureInfiniteness.evenRohlinClock_mem_unitary line 303
  24. lemma OAI.WeakPureInfiniteness.evenRohlinClock_order line 308
  25. lemma OAI.WeakPureInfiniteness.evenRohlinClock_cycles line 314
  26. lemma OAI.WeakPureInfiniteness.evenRohlinClock_shift_bound line 321
  27. lemma OAI.WeakPureInfiniteness.evenRohlinClock_generator_commutator line 345