# Deep points: the scenes as text

This is the static, text-only version of `index.html`. Every scene is a **finite
illustration**: a computation at the resolution stated in the page. The theorem is proved in
Lean (`Reeken.jordanCurveTheorem`); no picture proves it. Each scene lists the checked
declarations that carry the corresponding step of the proof.
`scripts/check-animation.py` verifies that this file mentions every scene and declaration.

## 1. Sampling is not enough

A spiral-shaped simple closed curve has, in its outside, a thin spiral corridor between
consecutive turns. A polygon through n equally spaced points of the curve jumps across turns
for small n: it crosses itself, and a point in the corridor tests as inside. Closeness at one
scale says nothing about thinner corridors, so the proof controls every scale at once.

- `Reeken.NSA.exists_initial_polygon` — uniform samples give an internal polygon with
  infinitesimal edges and exact shadow.
- `Reeken.NSA.polygon_approximates_at_every_scale` — two-sided approximation at every
  standard scale.

## 2. Cutting loops, and what it costs

A short chord joins two vertices no farther apart than the longest edge. If it spans at most
half the parameter circle, the vertices between its ends are deleted; otherwise only the block
between its ends is kept. Each surgery keeps the vertices on the curve in order with parameter
gaps at most one half, lowers the vertex count, and never lengthens the longest edge. The
crossing count can go up; the vertex count always goes down. The result is eventually simple,
but at a finite level surgery can also delete real features: from levels 24 and 64 the
polygon collapses to a triangle, and from level 256, whose longest edge is wider than the
corridor, it ends far from the curve. From level 512 it still follows the curve. An
infinitesimal level is finer than every standard feature, which is why Lean needs infinitesimal
edges and an unlimited vertex count before concluding simplicity. Lean takes a polygon of
minimal vertex count instead of iterating; in the hyperfinite reading, termination is internal
induction, not external well-foundedness of the hypernaturals.

- `Reeken.Geometry.InscribedPolygon.exists_reduction_of_short_chord`
- `Reeken.Geometry.InscribedPolygon.exists_minimal`
- `Reeken.Geometry.InscribedPolygon.Minimal.no_short_chord`
- `Reeken.Geometry.InscribedPolygon.Minimal.simple`
- `Reeken.NSA.vertex_count_unlimited`
- `Reeken.NSA.exists_simple_replacement`

## 3. One internal polygon, exactly the curve as its shadow

The simple polygons of all finite levels form one internal object, the class of the sequence
modulo a free ultrafilter. One positive infinitesimal bounds its distance to the curve in both
directions, and its shadow, the set of standard points infinitely close to it, equals the
curve. No finite level is the internal polygon. The extension `*K` of a set is not the union
of the monads of its standard points.

- `Reeken.NSA.exists_simple_polygon`
- `Reeken.NSA.polygon_infinitesimal_hausdorff`
- `Reeken.NSA.shadow_polygon`

## 4. Deep points keep their side

A standard point is deep in a region when its whole monad lies in it. The picture compares a
finite grid with a reference polyline outside a band chosen from sampled distances and
sampled parametric deviation. Red marks disagreement; grey marks the sampled band. The
sampled maximum is not a certified bound on the continuous supremum, and the band need not
shrink monotonically with the level. Tests check the displayed finite comparisons, not all
unsampled points or every finer level. Genuine uniform approximation and monad containment
are established by the linked Lean lemmas. Internal membership alone does not imply deepness.

- `Reeken.NSA.InternalSet.isDeep_of_ball_subset`
- `Reeken.NSA.InternalSet.IsDeep.of_near`
- `Reeken.NSA.InternalSet.Separates.standard_part_mem_deep`
- `Reeken.NSA.InternalSet.mem_shadow_iff_internal_ball` — where saturation enters.
- `Reeken.NSA.standardRegions_union`

## 5. Two colours are not yet a theorem

Transfer gives two disjoint open deep regions covering everything off the curve, but it
accepts a split with an empty side too (compiled example in `Tutorial/JordanStory.lean`).
Section 3 of the published paper supplies the geometry: near a curve point, a connector on
the chosen side joins the two arcs of the polygon, and a balanced point on it is a standard
distance from both. Its standard part is deep and near the curve point. The picture finds the
connector on a square ring; Lean uses actual clipped polygonal cells. The printed paper writes
a difference where equality of the two distances is meant (`docs/source-map.md`).

- `Reeken.NSA.InternalSet.Separates.deep_union`
- `Reeken.NSA.InternalSet.compact_separation_from_common_shadow`
- `Reeken.NSA.InternalSet.not_exists_near_iff`
- `Reeken.NSA.exists_deep_point_of_connectors`
- `Reeken.NSA.ball_inter_deep_nonempty`
- `Reeken.NSA.frontier_standardInside`
- `Reeken.NSA.frontier_standardOutside`

## 6. A whole compact loop inside one finite polygon

A self-crossing loop inside the curve lies, all of it, inside one finite polygon whose closed
inside stays in the standard inside. That polygon is contracted ear by ear down to a
triangle. Enclosure alone is not a null homotopy; Lean's ears come from an internal diagonal
of minimal span, and the deformations are explicit.

- `Reeken.NSA.exists_internal_inner_polygon`
- `Reeken.NSA.exists_closed_polygon_inside_of_isCompact`
- `Reeken.Geometry.exists_internal_ear`
- `Reeken.Geometry.contractibleSpace_closed_inside`
- `Reeken.NSA.isSimplyConnected_standardInside`

## 7. A second use: countably many wishes, one point

Nested closed sets in a compact set have moving stage witnesses; one internal point realizes
every stage, and its standard part lies in every set. Over a principal ultrafilter the sets
`*[k, ∞)` have no common point; for the external sets of standard naturals above `k` the
tactic `star_saturate` refuses with an explanation, and a theorem shows the refusal is
necessary.

- `Reeken.NSA.InternalSet.countable_saturation`
- `Reeken.NSA.starSaturate` — the `star_saturate` tactic.
- `Reeken.NSA.InternalSet.not_exists_forall_mem_Ici_pure`
- `Reeken.NSA.InternalSet.not_exists_forall_mem_standard_above`
- `Reeken.NSA.compact_standard_part`
- `Reeken.NSA.closed_standard_part`
- `Tutorial.NestedCompact.nested_compact_intersection`

## 8. Same machinery, new theorem: Arzelà–Ascoli

For an infinite index, a bounded equicontinuous sequence gives one S-continuous internal
function. Its continuous shadow is a uniform limit of a subsequence. The picture uses
`sin(x + n)` and a subsequence found by finite search (44, 333, 710, 103993); the
ultrafilter's own choice of limit is not computable.

- `Reeken.NSA.exists_continuousOn_near`
- `Reeken.NSA.forall_near_app_iff_uniform`
- `Tutorial.ArzelaAscoli.arzela_ascoli`

## 9. The theorem

For every continuous injective map of the unit circle into the plane, two nonempty, open,
disjoint, path-connected regions cover the complement of the curve; the inside is bounded and
simply connected, the outside is unbounded, and the curve is the frontier of each. The finite
polygonal theorem the paper assumes is proved too, through attributed finite code from Álvaro
Begué's schoenflies-lean. The proof uses only `propext`, `Classical.choice`, `Quot.sound`.

- `Reeken.jordanCurveTheorem`