RFC: proof-only import for Mandelbrot connectedness

Mandelbrot.lean

@@ -0,0 +1,59 @@
+module
+import Trustless
+public import Mathlib.Analysis.Complex.Basic
+public import Mathlib.Topology.Connected.Basic
+public import Mathlib.Order.Filter.AtTopBot.Basic
+
+/-!
+## The Mandelbrot set and its complement are connected (trustless)
+
+A verifier of `IsConnected mandelbrot` and `IsConnected mandelbrotᶜ` that does not
+trust what the Ray library does while constructing a proof.
+It does trust Mathlib and Trustless.
+
+const_fill: reads the named theorem's proof term and its dependency closure straight out of
+`Ray.Mandelbrot`'s compiled olean, re-checks every constant through the kernel, and closes the
+goal with the transplanted term, activating none of the library's elaboration (notation,
+macros, instances).
+trustless_fill: The same as above except the constants are extracted from lean4export, run in a
+sandbox.
+-/
+
+open Filter (Tendsto atTop)
+open Set
+section
+
+/-- The Mandelbrot set: all points that do not escape to `∞` under `z ↦ z^2 + c`. -/
+@[expose] public def mandelbrot : Set ℂ :=
+  {c | ¬Tendsto (fun n ↦ ‖(fun z ↦ z^2 + c)^[n] c‖) atTop atTop}
+
+/-- The Mandelbrot set is connected. -/
+public theorem isConnected_mandelbrot : IsConnected mandelbrot :=
+  trustless_fill Ray.Mandelbrot
+
+/-- The complement of the Mandelbrot set is connected. -/
+public theorem isConnected_compl_mandelbrot : IsConnected mandelbrotᶜ :=
+  trustless_fill Ray.Mandelbrot
+
+/-!
+Appendix:
+  The meaning of the above theorems depends on `IsConnected` and the topology on ℂ is given by
+  an instance of `[TopologicalSpace ℂ]`. We prove they both have the usual meaning.
+-/
+
+/-- The topology on ℂ being used is the open ball topology -/
+example (u : Set ℂ) : IsOpen u ↔ ∀ z ∈ u, ∃ ε > 0, ∀ w : ℂ, ‖w - z‖ < ε → w ∈ u := by
+  simp only [Metric.isOpen_iff, subset_def, Metric.mem_ball, Complex.dist_eq]
+
+/-- `‖·‖` above is the ordinary modulus on `ℂ` -/
+example (z : ℂ) : ‖z‖ = Real.sqrt (z.re ^ 2 + z.im ^ 2) := Complex.norm_eq_sqrt_sq_add_sq z
+
+/-- IsConnected s means: s is non-empty, and if two open sets cover s
+  and each have nontrivial intersection with s, then so does their intersection.
+ -/
+example {α} [TopologicalSpace α] (s : Set α) :
+    IsConnected s ↔
+      s.Nonempty ∧
+        ∀ u v : Set α, IsOpen u → IsOpen v → s ⊆ u ∪ v →
+          (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty :=
+  Iff.rfl

Mandelbrot2.lean

@@ -0,0 +1,30 @@
+module
+import Trustless
+public import Mathlib.Analysis.Complex.Basic
+public import Mathlib.Topology.Connected.Basic
+public import Mathlib.Order.Filter.AtTopBot.Basic
+
+/-!
+const import pulls in constants without triggering elaboration (it also replays them into the
+Kernel.Environment so they get rechecked again).
+Use `trustless import` for a version that extracts a the constants from lean4export
+running in a sandbox.
+
+Ray.Mandelbrot2 declares everything inside the `Ray` namespace, so that it doesn't collide with
+our mandelbrot, isConnected_mandelbrot and isConnected_compl_mandelbrot.
+-/
+const import Ray.Mandelbrot2
+
+open Filter (Tendsto atTop)
+open Set
+section
+
+/-- The Mandelbrot set: all points that do not escape to `∞` under `z ↦ z^2 + c`. -/
+@[expose] public def mandelbrot : Set ℂ :=
+  {c | ¬Tendsto (fun n ↦ ‖(fun z ↦ z^2 + c)^[n] c‖) atTop atTop}
+
+-- The Mandelbrot set is connected.
+public theorem isConnected_mandelbrot : IsConnected mandelbrot := Ray.isConnected_mandelbrot
+
+-- The complement of the Mandelbrot set is connected.
+public theorem isConnected_compl_mandelbrot : IsConnected mandelbrotᶜ := Ray.isConnected_compl_mandelbrot

Ray/Mandelbrot2.lean

@@ -0,0 +1,42 @@
+-- Same as Mandelbrot.lean but I put namespace Ray
+module
+public import Ray.Multibrot.Defs
+import Ray.Misc.Cobounded
+import Ray.Multibrot.Basic
+import Ray.Multibrot.Connected
+
+/-!
+## The Mandelbrot set and its complement are connected
+
+The rest of our proof works via manifolds and other machinery.  Here we strip that away:
+
+1. We define the Mandebrot set directly
+2. We show it is equal to `multibrot 2`
+3. Thus, the Mandelbrot set and its complement are connected
+-/
+
+open Filter (Tendsto atTop)
+open RiemannSphere
+open Set
+open scoped Topology Real
+noncomputable section
+namespace Ray
+
+/-- The Mandelbrot set: all points that do not escape to `∞` under `z ↦ z^2 + c` -/
+@[expose] public def mandelbrot : Set ℂ :=
+  {c | ¬Tendsto (fun n ↦ ‖(fun z ↦ z^2 + c)^[n] c‖) atTop atTop}
+
+/-- The Mandelbrot set is the `d = 2` Multibrot set -/
+public theorem mandelbrot_eq_multibrot : mandelbrot = multibrot 2 := by
+  ext c
+  simp only [mandelbrot, mem_ofPred_eq, multibrot, f_f'_iter, tendsto_inf_iff_tendsto_cobounded,
+    tendsto_cobounded_iff_norm_tendsto_atTop]
+  rfl
+
+/-- The Mandelbrot set is connected -/
+public theorem isConnected_mandelbrot : IsConnected mandelbrot := by
+  rw [mandelbrot_eq_multibrot]; exact isConnected_multibrot 2
+
+/-- The complement of the Mandelbrot set is connected -/
+public theorem isConnected_compl_mandelbrot : IsConnected mandelbrotᶜ := by
+  rw [mandelbrot_eq_multibrot]; exact isConnected_compl_multibrot 2

lake-manifest.json

@@ -1,7 +1,14 @@
 {"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover-community/mathlib4",
+ [{"type": "path",
+   "scope": "",
+   "name": "trustless",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "dir": "../trustless",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
@@ -11,6 +18,16 @@
    "inputRev": "v4.33.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/lean4export",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "15f6055e299ad5b89345e533cc2192f4cc00f659",
+   "name": "lean4export",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.33.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,

lakefile.lean

@@ -4,12 +4,21 @@ open Lake DSL
 package ray where
   leanOptions := #[
     ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b`
-    ⟨`linter.docPrime, false⟩,
+    ⟨`weak.linter.docPrime, false⟩, -- `weak.`: defined by Mathlib, absent in libs that don't import it
     ⟨`autoImplicit, false⟩,
     ⟨`experimental.module, true⟩,
   ]
 
 require "leanprover-community" / "mathlib" @ git "v4.33.0"
 
+require trustless from ".." / "trustless"
+
 @[default_target]
-lean_lib Ray
+lean_lib Ray where
+  roots := #[`Ray, `Mandelbrot, `Mandelbrot2]
+  -- The fills read the sources' oleans, an edge Lake cannot see; build them first.
+  extraDepTargets := #[`RayMandelbrotSource]
+
+-- The untrusted proofs, kept out of `Ray`'s import closure.
+lean_lib RayMandelbrotSource where
+  roots := #[`Ray.Mandelbrot, `Ray.Mandelbrot2]