Parabolic fibers are aperiodic in characteristic zero

Finite periodicity of a point does not imply finite order of the ambient rotation matrix. The opening therefore needs a point-level argument at normalized traces 2 and -2. The explicit parabolic-line translations give that argument in characteristic zero.

theorem BGS.Markoff.iterate_normalizedRotate1_parabolicLineAtTwo_ne_self_of_pos {K : Type u} [Field K] [CharZero K] (n : ℕ) (hn : 0 < n) (i t : K) (hi : i ^ 2 = -1) : normalizedRotate1^[n] (parabolicLineAtTwo i t) ≠ parabolicLineAtTwo i t

No positive iterate of the trace-2 rotation fixes a point on either parabolic line in characteristic zero.

theorem BGS.Markoff.iterate_normalizedRotate1_parabolicLineAtNegTwo_ne_self_of_pos {K : Type u} [Field K] [CharZero K] (n : ℕ) (hn : 0 < n) (i t : K) (hi : i ^ 2 = -1) : normalizedRotate1^[n] (parabolicLineAtNegTwo i t) ≠ parabolicLineAtNegTwo i t

No positive iterate of the trace--2 rotation fixes a point on either parabolic line in characteristic zero.

theorem BGS.Markoff.iterate_normalizedRotate1_ne_self_of_mem_fiber1_two {K : Type u} [Field K] [CharZero K] (i : K) (hi : i ^ 2 = -1) {x : NormalizedPoint K} (hx : x ∈ normalizedFiber1 2) (n : ℕ) (hn : 0 < n) : normalizedRotate1^[n] x ≠ x

Every point of the normalized trace-2 fiber is aperiodic once a square root of -1 is fixed.

theorem BGS.Markoff.iterate_normalizedRotate1_ne_self_of_mem_fiber1_neg_two {K : Type u} [Field K] [CharZero K] (i : K) (hi : i ^ 2 = -1) {x : NormalizedPoint K} (hx : x ∈ normalizedFiber1 (-2)) (n : ℕ) (hn : 0 < n) : normalizedRotate1^[n] x ≠ x

Every point of the normalized trace--2 fiber is aperiodic once a square root of -1 is fixed.