# Nonstandard analysis you can run: a tutorial

This guide accompanies four compiled Lean files in `Tutorial/` and the offline animation in
`animation/`. Nothing in `Reeken` imports them, so they cannot change the Jordan theorem or
its trust base. They are checked by `lake build Tutorial`; the axiom audit covers them.

## What you will learn

1. **Why finite pictures fail and what replaces them.** A wild simple closed curve can have
   corridors thinner than any sampling scale. Kanovei and Reeken use one *internal* polygon
   whose standard shadow is exactly the curve, and keep only **deep** points, whose whole
   monad lies on one side. Deep points cannot be wiggled across the curve.
2. **Why two colours are not yet a theorem.** Transfer gives two disjoint open deep regions
   covering the complement of the curve, but it would accept a split with an empty side just as
   well. The common boundary needs the geometry of the published Section 3.
3. **How to use the library.** Internal sets, standard parts, countable saturation through the
   tactic `star_saturate`, and continuous shadows of S-continuous internal functions.
4. **Where every hypothesis lives.** The free ultrafilter, the internality of each set, and
   the finite-intersection premise are visible in statements and named in error messages.

Reading order:

| File | Topic |
| --- | --- |
| [`Tutorial/Saturation.lean`](../Tutorial/Saturation.lean) | One point for countably many wishes; the tactic's two refusals and why each is mathematically necessary |
| [`Tutorial/NestedCompact.lean`](../Tutorial/NestedCompact.lean) | Cantor's intersection theorem in three visible steps |
| [`Tutorial/ArzelaAscoli.lean`](../Tutorial/ArzelaAscoli.lean) | Arzelà–Ascoli from the continuous-shadow theorem |
| [`Tutorial/JordanStory.lean`](../Tutorial/JordanStory.lean) | The Jordan proof scene by scene, using the completed proof's declarations |
| [`animation/index.html`](../animation/index.html) | Finite illustrations of the same scenes |

## The model in one paragraph

Fix `U : Ultrafilter ℕ` and a proof `hU : (U : Filter ℕ) ≤ atTop` that `U` is free (it
contains every tail). `Star U α` is the ultrapower of `α`; `std a` embeds a standard point;
an `InternalSet U α` is an element of `Star U (Set α)`, and `std S` is the extension of a
standard set, whose points form `starSet S`. Two internal points are `Near` when their
distance is below every positive standard real. A standard point is in the `shadow` of an
internal set when it is near one of its points, and is `deep` in it when its whole monad lies
in it. Freeness is an ordinary hypothesis, never a hidden instance. For mathlib's concrete
`hyperfilter ℕ` it is the theorem `Nat.hyperfilter_le_atTop`.

```lean
variable {U : Ultrafilter ℕ} (hU : (U : Filter ℕ) ≤ atTop)
include hU   -- stated once; every theorem in the section carries it visibly
```

## Countable saturation

Countable saturation is the step where a proof says "choose one point that does everything at
once". It is proved here by a diagonal construction (`countable_saturation_of_le_atTop`), not
assumed. The user interface is in `Reeken/Nonstandard/Saturate.lean`:

| You know | Use |
| --- | --- |
| `∀ n, ∃ x, ∀ k ≤ n, x ∈ s k` | `InternalSet.countable_saturation`, or `star_saturate` |
| `s` decreasing, each `s n` has a point | `InternalSet.fip_of_antitone` |
| every finite subfamily has a common point | `InternalSet.fip_of_finset`, `countable_saturation_of_countable` |
| a family over standard scales `ε > 0`, growing with `ε` | `InternalSet.exists_forall_pos_mem` |
| points of `s` within every standard `ε` of an internal `c` | `InternalSet.exists_near_iff_forall_starDist_lt` |

`InternalSet.countable_saturation` no longer asks for `[Nonempty α]`: stage `0` of the
premise already supplies a point.

### The tactic

`star_saturate hU` proves `∃ x : Star U α, ∀ k, x ∈ s k` and leaves exactly one goal, tagged
`fip`. For `ℕ`-indexed families that goal is `∀ n, ∃ x, ∀ k ≤ n, x ∈ s k`; for any other
countable index type it is `∀ F : Finset ι, ∃ x, ∀ k ∈ F, x ∈ s k`. The family is read off the
goal, so `x ∈ starSet (K ∩ t k)` is recognized as the internal set `std (K ∩ t k)`.

```lean
example : ∃ N : Star U ℕ, ∀ k : ℕ, N ∈ (std (Ici k) : InternalSet U ℕ) := by
  star_saturate          -- uses hU from the context
  intro n                -- stage n: wishes 0, …, n
  exact ⟨std n, fun k hk ↦ (InternalSet.std_mem_std _ _).mpr hk⟩

example (s : ℕ → InternalSet U α) (hs : Antitone s) (hne : ∀ n, ∃ x, x ∈ s n) :
    ∃ x, ∀ n, x ∈ s n := by
  star_saturate using InternalSet.fip_of_antitone hs hne    -- `?_` holes become goals
```

If `hU` is omitted, a local hypothesis of exactly that type is used, or
`Nat.hyperfilter_le_atTop` for `hyperfilter ℕ`. The tactic never assumes freeness. Its
diagnostics are pinned verbatim in
[`Verification/SaturationTests.lean`](../Verification/SaturationTests.lean):

| Situation | The message says |
| --- | --- |
| goal is not `∃ x, ∀ k, x ∈ s k` | the expected shape, the actual goal, and the `Set.nonempty_iInter` rewrite for `(⋂ k, s k).Nonempty` |
| a constraint is an external set (a monad, standard points) | that saturation holds only for internal sets, the counterexample theorem, and how to state an internal set |
| no freeness hypothesis | the missing type, and that saturation is false for principal ultrafilters (with the theorem) |
| the freeness argument has the wrong type | expected and actual types |
| `using h` does not prove the premise | the exact premise and Lean's type mismatch |
| an uncountable index type (`ℝ`) | that only countably many constraints are realized, and the scale lemma to use |
| a bounded index (`∀ ε > 0`) | the scale lemma, or reindex by a subtype |
| a conjunction of constraints | intersect them with `⊓` first (`InternalSet.mem_inf`) |
| a function applied to the point | move it into the set with `InternalSet.preimage` |
| an ultrafilter not on `ℕ` | that this interface is for free ultrafilters on `ℕ` |

Two refusals are backed by theorems showing the hypothesis cannot be dropped:
`InternalSet.not_exists_forall_mem_Ici_pure` (over a principal ultrafilter the decreasing
nonempty internal sets `*[k, ∞)` have no common point) and
`InternalSet.not_exists_forall_mem_standard_above` (the external sets of standard naturals above
`k` are decreasing and nonempty with no common point, for every ultrafilter).

**Scope.** This is countable saturation of internal sets over a free ultrafilter on `ℕ`. It is
not κ-saturation for larger κ, not saturation for external sets, and not saturation of
arbitrary first-order types; mathlib's `CountableInterFilter` (countable completeness) is a
different notion. Stronger saturation would need a separate construction, such as a good
ultrafilter on a larger index set, with explicit cardinal and language bounds.

## Standard parts and continuous shadows

`compact_standard_part` gives a standard part in a compact set; `closed_standard_part` keeps it
in a closed set. `Reeken/Nonstandard/ContinuousShadow.lean` adds the analysis checkpoint:

- `exists_continuousOn_near`: if an internal `F` maps `*K` into `*L` (both compact) and is
  S-continuous there, a continuous standard `f` maps `K` into `L` and is infinitely close to `F`
  at **every** internal point of `*K`. Saturation enters once, to turn "no bad point is near
  `b`" into a standard `δ`.
- `forall_near_app_iff_uniform`: an indexed family is infinitely close to `*g` at every internal
  point of `*K` exactly when, for each standard `ε`, almost every member is uniformly `ε`-close
  to `g` on `K`. No freeness is used.
- `Near.starDist`, `Near.standardPart_le`, `starDist_triangle`: the bookkeeping that keeps
  representative sequences out of proofs.

[`Tutorial/ArzelaAscoli.lean`](../Tutorial/ArzelaAscoli.lean) proves Arzelà–Ascoli
(uniformly equicontinuous maps from a compact set into a compact set have a uniformly
convergent subsequence with continuous limit) from these in about thirty lines. Two steps
carry the analysis: equicontinuity makes `f N` S-continuous, and the continuous shadow is
the limit.

## The Jordan story

[`Tutorial/JordanStory.lean`](../Tutorial/JordanStory.lean) restates each step with the
completed proof's declarations, so the story is checked against the proof:

1. `exists_simple_polygon`: one internal simple polygon with exactly the curve as its shadow.
2. **Membership is not deepness**, proved: a ball of infinitesimal radius contains its centre,
   but an infinitely close point lies outside it. Then the three facts that make deep points
   useful: `isDeep_of_ball_subset`, `IsDeep.of_near`, `Separates.standard_part_mem_deep`.
3. **Where saturation enters**: the proof that shadows are closed, now written with
   `exists_forall_pos_mem`.
4. **Two colours are not yet a theorem**, proved: for any closed `B`, the split `(∅, Bᶜ)` is an
   internal separation whose deep regions cover the complement of the shadow, with one side
   empty. Then `ball_inter_deep_nonempty` and the two frontier theorems.
5. `exists_closed_polygon_inside_of_isCompact` and `isSimplyConnected_standardInside`.
6. The proof of `Reeken.jordanCurveTheorem`, annotated scene by scene.

## Second theorems: what was done and what is next

- **Nested compact intersection** (`Tutorial.NestedCompact`): done. Compared with the earlier
  handoff version, the `Nonempty α` workaround, the representative family, and the membership
  conversions are gone.
- **Arzelà–Ascoli** (`Tutorial.ArzelaAscoli`): done, through the reusable continuous shadow.
- **Peano existence** (scalar, by Euler polygons): not done. Assessment: the nonstandard half
  is now short. The internal Euler polygon at an unlimited step count is S-continuous from a
  Lipschitz bound, its continuous shadow `y` exists by `exists_continuousOn_near`, and
  `forall_near_app_iff_uniform` turns "the step derivative is infinitely close to `g(t, y t)`
  on `*[0, 1]`" into uniform closeness along the ultrafilter. The remaining work is finite and
  standard. Define the node recursion and the step function `G_n`; prove
  `Y_n t = y₀ + ∫₀ᵗ G_n`, which needs the integral of a step function over adjacent intervals;
  prove measurability and a uniform bound for `G_n`. Then finish with the fundamental theorem
  of calculus. The estimate is a few hundred lines of ordinary Lean. Continuity of `g` gives
  existence only, not uniqueness or a rate.
- **Dini's theorem**: not done. The nonstandard proof needs `Near` arithmetic on internal reals
  (sums and order), which the library has only through representatives. It is a good next test
  of that interface.

## Known rough edges

- `std S` has type `Star U (Set α)`, so `(std S).deep` does not find the `InternalSet`
  namespace. Give the set a name of type `InternalSet U α` (as in `Tutorial/JordanStory.lean`)
  or apply the function explicitly. A one-field structure for internal sets would fix this, at
  the cost of a library-wide refactor.
- `star_saturate` recognizes internal sets syntactically: `InternalSet` values, `toSet`,
  `starSet`, and `internalSet`. A set of internal points that happens to equal an internal set
  must be rewritten first; the refusal message says so.
- Internal sets defined by internal formulas are still built from representatives
  (`ofSeq fun i ↦ {x | …}`), as in the continuity step of `exists_continuousOn_near`. This is the
  internal definition principle made explicit; a set-builder notation for internal predicates
  would hide it.

## Foundations, and what is not claimed

The model is the ultrapower `Filter.Germ`, in Lean's ordinary foundations, with only
`propext`, `Classical.choice`, and `Quot.sound`. No IST axioms are added. An axiomatic
experiment would have to live in a separate library with its trust assumptions stated. Adding a
standardness predicate on Lean's `ℕ` with an unlimited element contradicts Lean's induction, so
such an experiment needs an encoded object theory or a separate nonstandard carrier. This
tutorial makes no claim about Sanders-style extraction of constructive content, and none about
the brachistochrone.