OAI/Analysis/OInfinity/RohlinPartitions.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Concrete dyadic partitions for an even Cuntz row

The phases are explicit roots of unity. The finite partitions below use the actual geometric CAR modes of the supplied even row, followed by the proved Jordan–Wigner construction. Quantitative cyclic shift control is separate from the exact partition identities.

  1. def OAI.WeakPureInfiniteness.carDyadicPhase line 19

    Source documentation

    The phase with half-period 2^i.

    def carDyadicPhase (i : ℕ) : ℂ := Complex.exp (((Real.pi / (2 : ℝ) ^ i : ℝ) : ℂ) * Complex.I)
  2. lemma OAI.WeakPureInfiniteness.carDyadicPhase_norm line 21
  3. lemma OAI.WeakPureInfiniteness.carDyadicPhase_half line 24
  4. def OAI.WeakPureInfiniteness.evenRohlinCoordinate line 36

    Source documentation

    Commuting two-level coordinates of the actual even row.

    def evenRohlinCoordinate (q : E) (r : Fin 2 × Fin n → E) (L i : ℕ) : E :=
…
  5. def OAI.WeakPureInfiniteness.evenRohlinProjection line 40

    Source documentation

    The kth cell at dyadic level m.

    def evenRohlinProjection (q : E) (r : Fin 2 × Fin n → E) (L m k : ℕ) : E :=
…
  6. lemma OAI.WeakPureInfiniteness.evenRohlinCoordinate_properties line 49
  7. lemma OAI.WeakPureInfiniteness.evenRohlinProjection_partition line 71
  8. lemma OAI.WeakPureInfiniteness.evenRohlinProjection_support line 85
  9. lemma OAI.WeakPureInfiniteness.evenRohlinBlock_shift_error line 92