OAI/Analysis/OInfinity/FiniteCAR.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Finite anticommutation relations inside a relative Cuntz corner

The Jordan–Wigner recursion is carried out in the explicit corner unit q. No infinite CAR representation is used. Its even products have exact shift covariance, which is the algebraic input for finite cyclic partitions.

  1. def OAI.WeakPureInfiniteness.zeroCornerShift line 19
  2. def OAI.WeakPureInfiniteness.zeroCornerParity line 21
  3. def OAI.WeakPureInfiniteness.zeroCornerCAR line 23
  4. lemma OAI.WeakPureInfiniteness.zeroCornerShift_star line 27
  5. lemma OAI.WeakPureInfiniteness.zeroCornerShift_add line 31
  6. lemma OAI.WeakPureInfiniteness.zeroCornerShift_zero line 36
  7. lemma OAI.WeakPureInfiniteness.zeroCornerShift_support line 45
  8. lemma OAI.WeakPureInfiniteness.zeroCornerShift_mul line 58
  9. lemma OAI.WeakPureInfiniteness.zeroCornerShift_unit line 75
  10. lemma OAI.WeakPureInfiniteness.zeroCornerParity_star line 79
  11. lemma OAI.WeakPureInfiniteness.zeroCornerParity_sq line 83
  12. lemma OAI.WeakPureInfiniteness.zeroCornerParity_support line 94
  13. lemma OAI.WeakPureInfiniteness.zeroCornerShift_commute_seed line 106
  14. lemma OAI.WeakPureInfiniteness.zeroCornerShift_commute_parity line 124
  15. lemma OAI.WeakPureInfiniteness.zeroCornerCAR_seed_relations line 145
  16. lemma OAI.WeakPureInfiniteness.zeroCornerCAR_support line 169
  17. lemma OAI.WeakPureInfiniteness.zeroCornerCAR_succ_commute_parity line 191

    Source documentation

    The parity commutes with every positive-index generator.

    lemma zeroCornerCAR_succ_commute_parity (n : ℕ) :
    Commute (zeroCornerParity a b) (zeroCornerCAR a b (n + 1)) := by
…

    Mentions: OAI.WeakPureInfiniteness.zeroCornerParity, OAI.WeakPureInfiniteness.zeroCornerCAR

  18. lemma OAI.WeakPureInfiniteness.zeroCornerShift_parity_mul line 200
  19. lemma OAI.WeakPureInfiniteness.zeroCornerShift_parity_star_mul line 213
  20. lemma OAI.WeakPureInfiniteness.zeroCornerCAR_shift_even line 227

    Source documentation

    Shift covariance holds exactly for even products.

    lemma zeroCornerCAR_shift_even (i j : ℕ) :
    zeroCornerShift a b (zeroCornerCAR a b i * star (zeroCornerCAR a b j)) =
      zeroCornerCAR a b (i + 1) * star (zeroCornerCAR a b (j + 1)) := by
…

    Mentions: OAI.WeakPureInfiniteness.zeroCornerShift, OAI.WeakPureInfiniteness.zeroCornerCAR

  21. lemma OAI.WeakPureInfiniteness.zeroCornerCAR_seed_anticommute line 256
  22. lemma OAI.WeakPureInfiniteness.zeroCornerCAR_anticommute line 276
  23. lemma OAI.WeakPureInfiniteness.zeroCornerCAR_seed_star_anticommute line 303
  24. lemma OAI.WeakPureInfiniteness.zeroCornerCAR_star_anticommute line 329
  25. lemma OAI.WeakPureInfiniteness.squareZero_norm_sq_le line 368

    Source documentation

    The norm estimate for a finite CAR linear combination is algebraic: square zero and its anticommutator determine the bound.

    lemma squareZero_norm_sq_le (x q : E) (c : ℝ) (hc : 0 ≤ c)
    (hxx : x * x = 0) (hqx : q * x = x)
    (hgram : star x * x + x * star x = c • q) : ‖x‖ * ‖x‖ ≤ c := by
…
  26. lemma OAI.WeakPureInfiniteness.zeroCornerCAR_norm_le_one line 396