Strip geometry and the negative real axis

Lemmas 4–5 combine expansion, connectedness, and explicit exponential geometry.

Part of Lasse Rempe's formalisation of Shen and Rempe-Gillen's exponential-map paper, with generative AI assistance including Copilot, Claude, and particularly ChatGPT. The initial proof architecture uses John Harrison's HOL Light formalisation. See LeanPool.ExpChaotic for attribution and the upstream source.

Lemma 4

theorem ExponentialJuliaSetMisiurewicz.expIterate_im_eq_zero_of_le {z : ℂ} {n : ℕ} (h : (expIterate n z).im = 0) (m : ℕ) : n ≤ m → (expIterate m z).im = 0

If an orbit point is real, all later orbit points are real.

theorem ExponentialJuliaSetMisiurewicz.expIterate_im_succ_eq_zero_of_int {z : ℂ} {n : ℕ} {k : ℤ} (h : (expIterate n z).im = ↑k * Real.pi) : (expIterate (n + 1) z).im = 0

If the imaginary part of an orbit point is an integer multiple of π, the next point is real.

theorem ExponentialJuliaSetMisiurewicz.deriv_expIterate_add (a b : ℕ) (z : ℂ) : deriv (expIterate (a + b)) z = deriv (expIterate a) (expIterate b z) * deriv (expIterate b) z

Chain rule for iterates: expIterate (a + b) = expIterate a ∘ expIterate b.

Strengthening: reaching the negative real axis

An orbit point whose imaginary part is an odd multiple of π has negative real image, since cos ((2m+1)π) = -1. Getting an odd multiple needs an imaginary spread of 2π rather than π, which both branches of Lemma 4 in fact supply.

def ExponentialJuliaSetMisiurewicz.EventuallyMeetsNegativeRealAxis (V : Set ℂ) : Prop

Some forward image of V lands on the negative real axis.

Equations

• One or more equations did not get rendered due to their size.

theorem ExponentialJuliaSetMisiurewicz.exp_neg_real_of_odd_mul_pi {z : ℂ} {k : ℤ} (hk : Odd k) (h : z.im = ↑k * Real.pi) : (Complex.exp z).im = 0 ∧ (Complex.exp z).re < 0

An odd multiple of π in the imaginary part gives a negative real exponential.

theorem ExponentialJuliaSetMisiurewicz.two_pi_le_abs_im_sub_of_exp_eq {a b : ℂ} (h : Complex.exp a = Complex.exp b) (hne : a ≠ b) : 2 * Real.pi ≤ |a.im - b.im|

Two distinct points with the same exponential have imaginary parts at least 2π apart.

theorem ExponentialJuliaSetMisiurewicz.pi_le_abs_im_sub_of_exp_eq {a b : ℂ} (h : Complex.exp a = Complex.exp b) (hne : a ≠ b) : Real.pi ≤ |a.im - b.im|

Two distinct points with the same exponential have imaginary parts at least π apart (indeed 2π). This is the non-injective branch of Harrison's argument.

theorem ExponentialJuliaSetMisiurewicz.lemma4_exists_im_far_apart_two_pi {V : Set ℂ} (hVopen : IsOpen V) (hVne : V.Nonempty) (hinf : {n : ℕ | Disjoint (expIterate n '' V) centralStrip}.Infinite) : ∃ (n : ℕ) (w : ℂ) (z : ℂ), w ∈ V ∧ z ∈ V ∧ 2 * Real.pi ≤ |(expIterate n w).im - (expIterate n z).im|

If infinitely many images miss the central strip, some image has imaginary diameter at least 2π. If every iterate is injective, derivative growth and Lemma 3 produce a large image disk. Otherwise, the first failure of injectivity gives a pair separated by a nonzero period of the exponential.

theorem ExponentialJuliaSetMisiurewicz.lemma4_exists_im_far_apart {V : Set ℂ} (hVopen : IsOpen V) (hVne : V.Nonempty) (hinf : {n : ℕ | Disjoint (expIterate n '' V) centralStrip}.Infinite) : ∃ (n : ℕ) (w : ℂ) (z : ℂ), w ∈ V ∧ z ∈ V ∧ Real.pi ≤ |(expIterate n w).im - (expIterate n z).im|

Some forward image of V contains two points whose imaginary parts differ by at least π, given that infinitely many forward images avoid the central strip.

theorem ExponentialJuliaSetMisiurewicz.lemma4_exists_im_odd_mul_pi {V : Set ℂ} (hVconn : IsConnected V) (h : ∃ (n : ℕ) (w : ℂ) (z : ℂ), w ∈ V ∧ z ∈ V ∧ 2 * Real.pi ≤ |(expIterate n w).im - (expIterate n z).im|) : ∃ (n : ℕ) (y : ℂ) (k : ℤ), y ∈ V ∧ Odd k ∧ (expIterate n y).im = ↑k * Real.pi

With an imaginary spread of 2π, the intermediate value theorem finds a point whose imaginary part is an odd multiple of π: the interval contains two consecutive multiples, and one of them is odd.

theorem ExponentialJuliaSetMisiurewicz.negativeRealAxis_of_infinite_strip_misses {V : Set ℂ} (hVopen : IsOpen V) (hVconn : IsConnected V) (hVne : V.Nonempty) (hinf : {n : ℕ | Disjoint (expIterate n '' V) centralStrip}.Infinite) : EventuallyMeetsNegativeRealAxis V

Negative-axis strengthening, conditional form. If infinitely many forward images of V avoid the central strip, then some forward image meets the negative real axis.

theorem ExponentialJuliaSetMisiurewicz.lemma4_exists_im_int_mul_pi {V : Set ℂ} (hVconn : IsConnected V) (h : ∃ (n : ℕ) (w : ℂ) (z : ℂ), w ∈ V ∧ z ∈ V ∧ Real.pi ≤ |(expIterate n w).im - (expIterate n z).im|) : ∃ (n : ℕ) (y : ℂ) (k : ℤ), y ∈ V ∧ (expIterate n y).im = ↑k * Real.pi

From two far-apart imaginary parts, the intermediate value theorem on the connected set V produces a point whose imaginary part is an exact integer multiple of π.

theorem ExponentialJuliaSetMisiurewicz.lemma4_eventually_meets_centralStrip {V : Set ℂ} (hVopen : IsOpen V) (hVconn : IsConnected V) (hVne : V.Nonempty) : ∃ (N : ℕ), ∀ n ≥ N, (expIterate n '' V ∩ centralStrip).Nonempty

Lemma 4. Only finitely many forward images of a non-empty open connected set can be disjoint from the central strip. HOL Light: LEMMA_4.

Lemma 5

theorem ExponentialJuliaSetMisiurewicz.frontier_centralStrip_subset : frontier centralStrip ⊆ {z : ℂ | |z.im| = Real.pi / 3}

The frontier of the central strip consists of points with |Im z| = π/3.

theorem ExponentialJuliaSetMisiurewicz.abs_im_exp_gt_two_pi_of_frontier {z : ℂ} (hfr : |z.im| = Real.pi / 3) (hre : 4 < z.re) : 2 * Real.pi < |(Complex.exp z).im|

The geometric heart of Lemma 5. On the frontier of the central strip, inside the right half-plane, the exponential throws points clear of the wide strip: |sin| = √3/2 there, and e^4 · √3/2 already exceeds 2π.

theorem ExponentialJuliaSetMisiurewicz.IsPreconnected.subset_of_disjoint_frontier {X : Type u_1} [TopologicalSpace X] {u v : Set X} (hv : IsPreconnected v) (hu : IsOpen u) (hdisj : Disjoint (frontier u) v) (hne : (v ∩ u).Nonempty) : v ⊆ u

A connected set disjoint from the frontier of an open set, and meeting it, lies inside it. This is the Lean form of HOL Light's CONNECTED_INTER_FRONTIER.

theorem ExponentialJuliaSetMisiurewicz.IsPreconnected.inter_frontier_nonempty {X : Type u_1} [TopologicalSpace X] {u v : Set X} (hv : IsPreconnected v) (h1 : (v ∩ u).Nonempty) (h2 : (v \ u).Nonempty) : (v ∩ frontier u).Nonempty

A connected set meeting both u and its complement must meet the frontier of u. This is HOL Light's CONNECTED_INTER_FRONTIER.

def ExponentialJuliaSetMisiurewicz.doubleStrip : Set ℂ

The set w of Harrison's proof: points of the wide strip whose exponential also lies in the wide strip.

Equations

• ExponentialJuliaSetMisiurewicz.doubleStrip = {z : ℂ | |z.im| ≤ 2 * Real.pi ∧ |(Complex.exp z).im| ≤ 2 * Real.pi}

theorem ExponentialJuliaSetMisiurewicz.frontier_wideStrip_subset : frontier wideStrip ⊆ {z : ℂ | |z.im| = 2 * Real.pi}

A frontier point of the wide strip satisfies |Im z| = 2π.

theorem ExponentialJuliaSetMisiurewicz.frontier_expStrip_subset : frontier {z : ℂ | |(Complex.exp z).im| ≤ 2 * Real.pi} ⊆ {z : ℂ | |(Complex.exp z).im| = 2 * Real.pi}

On the frontier of the preimage of the wide strip, |Im (exp z)| = 2π.

theorem ExponentialJuliaSetMisiurewicz.disjoint_frontier_centralStrip : Disjoint (frontier centralStrip) (doubleStrip ∩ rightHalfPlane)

The frontier of the central strip misses w ∩ h: this is where the estimate bites.

theorem ExponentialJuliaSetMisiurewicz.im_exp_eq_zero_of_abs_im_eq_two_pi {z : ℂ} (h : |z.im| = 2 * Real.pi) : (Complex.exp z).im = 0

If |Im z| = 2π then exp z is real.

theorem ExponentialJuliaSetMisiurewicz.rightHalfPlane_exp_of_mem {z : ℂ} (hs : z ∈ centralStrip) (hh : z ∈ rightHalfPlane) : Complex.exp z ∈ rightHalfPlane

Points of the central strip in the right half-plane stay in the right half-plane.

theorem ExponentialJuliaSetMisiurewicz.deriv_expIterate_ne_zero (n : ℕ) (z : ℂ) : deriv (expIterate n) z ≠ 0

The derivative of an iterate never vanishes.

theorem ExponentialJuliaSetMisiurewicz.isOpen_image_expIterate {V : Set ℂ} (hV : IsOpen V) (n : ℕ) : IsOpen (expIterate n '' V)

Every iterate is an open map, so images of open sets are open.

The π-strips, for the negative-axis argument

theorem ExponentialJuliaSetMisiurewicz.neg_real_of_abs_im_eq_pi {z : ℂ} (h : |z.im| = Real.pi) : (Complex.exp z).im = 0 ∧ (Complex.exp z).re < 0

|Im z| = π makes the exponential a negative real number.

def ExponentialJuliaSetMisiurewicz.piStrip : Set ℂ

The closed strip of imaginary height π used for the negative-real-axis argument.

Equations

• ExponentialJuliaSetMisiurewicz.piStrip = {z : ℂ | |z.im| ≤ Real.pi}

def ExponentialJuliaSetMisiurewicz.piDoubleStrip : Set ℂ

Points whose imaginary parts, before and after one exponential, have absolute value at most π.

Equations

• ExponentialJuliaSetMisiurewicz.piDoubleStrip = {z : ℂ | |z.im| ≤ Real.pi ∧ |(Complex.exp z).im| ≤ Real.pi}

theorem ExponentialJuliaSetMisiurewicz.frontier_piStrip_subset : frontier piStrip ⊆ {z : ℂ | |z.im| = Real.pi}

A frontier point of piStrip satisfies |Im z| = π.

theorem ExponentialJuliaSetMisiurewicz.frontier_expPiStrip_subset : frontier {z : ℂ | |(Complex.exp z).im| ≤ Real.pi} ⊆ {z : ℂ | |(Complex.exp z).im| = Real.pi}

On the frontier of the preimage of piStrip, |Im (exp z)| = π.

theorem ExponentialJuliaSetMisiurewicz.disjoint_frontier_centralStrip_pi : Disjoint (frontier centralStrip) (piDoubleStrip ∩ rightHalfPlane)

The frontier estimate still bites with π in place of 2π.

theorem ExponentialJuliaSetMisiurewicz.lemma5_negative_real_axis {V : Set ℂ} (hVopen : IsOpen V) (hVconn : IsConnected V) (hVne : V.Nonempty) (hfrequent : {n : ℕ | Set.MapsTo (expIterate n) V rightHalfPlane}.Infinite) : EventuallyMeetsNegativeRealAxis V

Lemma 5, negative-axis form. If infinitely many images of V lie in the right half-plane, some image meets the negative real axis.

The π-strips replace Harrison's 2π-strips: on their frontiers |Im z| = π, where the exponential is negative real rather than positive. The final step no longer appeals to the standing hypothesis at all — the image is open, hence contains a non-real point, whose orbit would have to stay in the central strip forever, contradicting Lemma 2b.

theorem ExponentialJuliaSetMisiurewicz.lemma5_real_axis_of_frequently_in_rightHalfPlane {V : Set ℂ} (hVopen : IsOpen V) (hVconn : IsConnected V) (hVne : V.Nonempty) (hfrequent : {n : ℕ | Set.MapsTo (expIterate n) V rightHalfPlane}.Infinite) : EventuallyMeetsRealAxis V

Lemma 5. If infinitely many images of a non-empty open connected set are contained in the right half-plane, then an image meets the real axis. HOL Light: LEMMA_5.