Every domain eventually meets the real axis

Lemma 6: bounded transforms and compactness contradict the strip lemmas.

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.

Towards Lemma 6

theorem ExponentialJuliaSetMisiurewicz.lemma6_eventually_meets_disc {V : Set ℂ} (hVopen : IsOpen V) (hVconn : IsConnected V) (hVne : V.Nonempty) (hnoreal : ∀ (n : ℕ), ∀ z ∈ V, (expIterate n z).im ≠ 0) : ∃ (N : ℕ), ∀ n ≥ N, (expIterate n '' V ∩ Metric.closedBall 0 (Real.exp 4)).Nonempty

Harrison's auxiliary step inside LEMMA_6: if no forward image of V meets the real axis, then all but finitely many images meet the disc of radius exp 4.

Contrapositive of Lemma 5: only finitely many images can sit inside the right half-plane, and if the image at time n misses the disc then the image at time n - 1 lay in the half-plane, since ‖exp z‖ = exp (Re z).

theorem ExponentialJuliaSetMisiurewicz.exists_double_subseq {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] {s : Set X} {t : Set Y} (hs : IsCompact s) (ht : IsCompact t) {a : ℕ → X} {b : ℕ → Y} (ha : ∀ (n : ℕ), a n ∈ s) (hb : ∀ (n : ℕ), b n ∈ t) : ∃ x ∈ s, ∃ y ∈ t, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Filter.Tendsto (a ∘ φ) Filter.atTop (nhds x) ∧ Filter.Tendsto (b ∘ φ) Filter.atTop (nhds y)

Two sequences in compact sets admit a common convergent subsequence.

theorem ExponentialJuliaSetMisiurewicz.exists_disc_points {V : Set ℂ} (hnoreal : ∀ (n : ℕ), ∀ z ∈ V, (expIterate n z).im ≠ 0) {c : ℂ} {σ : ℝ} (hσ : 0 < σ) (hsub : Metric.ball c σ ⊆ V) : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∃ y ∈ Metric.ball c σ, ‖expIterate n y‖ ≤ Real.exp 4

Along all large times, the ball contains a point whose image stays in the disc of radius exp 4.

Reduction of the lower half-plane case by conjugation

theorem ExponentialJuliaSetMisiurewicz.expIterate_conj (n : ℕ) (z : ℂ) : expIterate n ((starRingEnd ℂ) z) = (starRingEnd ℂ) (expIterate n z)

Conjugation commutes with the iterates of exp.

theorem ExponentialJuliaSetMisiurewicz.conj_image_eq_preimage (V : Set ℂ) : ⇑(starRingEnd ℂ) '' V = ⇑(starRingEnd ℂ) ⁻¹' V

Conjugation is an involution, so the image of a set is its preimage.

theorem ExponentialJuliaSetMisiurewicz.isOpen_conj_image {V : Set ℂ} (hV : IsOpen V) : IsOpen (⇑(starRingEnd ℂ) '' V)

Complex conjugation sends open sets to open sets.

theorem ExponentialJuliaSetMisiurewicz.isConnected_conj_image {V : Set ℂ} (hV : IsConnected V) : IsConnected (⇑(starRingEnd ℂ) '' V)

Complex conjugation sends connected sets to connected sets.

theorem ExponentialJuliaSetMisiurewicz.nonempty_conj_image {V : Set ℂ} (hV : V.Nonempty) : (⇑(starRingEnd ℂ) '' V).Nonempty

The conjugate image of a nonempty set is nonempty.

theorem ExponentialJuliaSetMisiurewicz.noreal_conj_image {V : Set ℂ} (hnoreal : ∀ (n : ℕ), ∀ z ∈ V, (expIterate n z).im ≠ 0) (n : ℕ) (z : ℂ) : z ∈ ⇑(starRingEnd ℂ) '' V → (expIterate n z).im ≠ 0

No image of the conjugate meets the real axis if none of V's images does.

theorem ExponentialJuliaSetMisiurewicz.conj_image_up_of_down {V : Set ℂ} {n : ℕ} (h : ∀ z ∈ V, (expIterate n z).im < 0) (z : ℂ) : z ∈ ⇑(starRingEnd ℂ) '' V → 0 < (expIterate n z).im

Times at which V lands in the lower half-plane are times at which the conjugate lands in the upper one.

theorem ExponentialJuliaSetMisiurewicz.eventuallyMeetsRealAxis_of_conj {V : Set ℂ} (h : EventuallyMeetsRealAxis (⇑(starRingEnd ℂ) '' V)) : EventuallyMeetsRealAxis V

The conjugation reduction. If the conjugate set has an image meeting the real axis, so does the original.

theorem ExponentialJuliaSetMisiurewicz.expIterate_real_orbit {p : ℂ} (hp : p.im = 0) (m : ℕ) : (expIterate m p).im = 0 ∧ p.re + ↑m ≤ (expIterate m p).re

The orbit of a real point stays real and its real part grows by at least 1 each step.

theorem ExponentialJuliaSetMisiurewicz.exists_re_gt_four_of_real {p : ℂ} (hp : p.im = 0) : ∃ (m : ℕ), 4 < (expIterate m p).re

A real point's orbit escapes to the right: some iterate has real part exceeding 4.

theorem ExponentialJuliaSetMisiurewicz.lemma6_accumulation_up {V : Set ℂ} (hVopen : IsOpen V) (hVne : V.Nonempty) (hnoreal : ∀ (n : ℕ), ∀ z ∈ V, (expIterate n z).im ≠ 0) {T : Set ℕ} (hTinf : T.Infinite) (hTup : ∀ n ∈ T, ∀ z ∈ V, 0 < (expIterate n z).im) : ∃ (p : ℂ) (y : ℂ), 0 ≤ p.im ∧ ∀ η > 0, ∃ δ > 0, Metric.ball y δ ⊆ V ∧ ∀ (K : ℕ), ∃ (n : ℕ), K ≤ n ∧ ∀ z ∈ Metric.ball y δ, ‖expIterate n z - p‖ < η

Accumulation. If infinitely many images of V lie in the upper half-plane and none meets the real axis, there is a finite point p and a centre y such that arbitrarily small balls about y are carried, at arbitrarily late times, into arbitrarily small neighbourhoods of p. This is weak Montel in the form Lemma 6 consumes.

theorem ExponentialJuliaSetMisiurewicz.isClosed_centralStrip : IsClosed centralStrip

The central strip is closed, since the absolute imaginary-part function is continuous.

theorem ExponentialJuliaSetMisiurewicz.isOpen_rightHalfPlane : IsOpen rightHalfPlane

The half-plane Re z > 4 is open.

theorem ExponentialJuliaSetMisiurewicz.lemma6_contradiction_up {V : Set ℂ} (hVopen : IsOpen V) (hVne : V.Nonempty) (hnoreal : ∀ (n : ℕ), ∀ z ∈ V, (expIterate n z).im ≠ 0) {T : Set ℕ} (hTinf : T.Infinite) (hTup : ∀ n ∈ T, ∀ z ∈ V, 0 < (expIterate n z).im) : False

The upper half-plane case of Lemma 6 is contradictory.

theorem ExponentialJuliaSetMisiurewicz.lemma6_every_domain_eventually_meets_real_axis {V : Set ℂ} (hVopen : IsOpen V) (hVconn : IsConnected V) (hVne : V.Nonempty) : EventuallyMeetsRealAxis V

Lemma 6. Every non-empty open connected set has a forward image meeting the real axis. HOL Light: LEMMA_6.

Harrison uses Montel's fundamental normality test for families omitting two values. Since the images here omit the whole real axis and are connected, each lies in one open half-plane, so a Cayley transform makes the family bounded and the Cauchy estimate suffices: see equicontinuous_cayleyUp and lemma6_accumulation_up. The lower half-plane case reduces to the upper one by conjugation.