the Grand Tour

M-C · todo/lean/070 · leg-4 program, round 3 · kernel-checked, promoted 2026-07-17 (0813296)

There is a way to count the circle arrangements on a sphere that never once consults an outside table. You start from the smaller arrangements and you walk. Take an arrangement, delete one of its circles, and write down the trail that the deleted circle used to trace through everything that remains. If every arrangement leaves such a trail, and every legal trail rebuilds exactly one arrangement, then the whole census is nothing but the set of legal trails over the smaller census — enumerable by a walk, with nothing external to check it against. That is the promise of L4-conn, this project’s one completeness route that leans on no published count. The Grand Tour proves the first half of it: the trail exists, and it is a walk.

Fix the vocabulary once. Let $M$ be the arrangement with the deleted circle $c$ still in it — the child — and let $M'$ be $M$ with $c$ removed, the parent (in the Lean, M.deleteCircle c h). L4-conn wants to enumerate children by walking their parents. M-C takes one child and extracts, from the way $c$ threaded through it, a closed walk over the parent. It does not yet rebuild the child, and it does not yet claim the walk finds every child; those are later rounds, named at the end.

Deleting a circle, and the splice

Deletion is the previous round’s surgery (M-A, “the Watershed”). Erase $c$ and every circle that used to cross it keeps going straight through the vanished crossing: its two arc-ends, once stopped at that vertex, splice into a single longer arc. The census models an arrangement as a DartMap — each arc carries two darts, one per end — and the splice is a single permutation of darts,

$$\mathrm{cont} \;=\; \mathrm{twin} \circ \mathrm{rot}^2$$

read right to left at a crossing vertex. A vertex where $c$ meets another circle is a proper degree-4 crossing: four darts sit around it in a rotational cycle, alternating $c$, other, $c$, other. The rotation $\mathrm{rot}^2$ advances two steps, carrying a $c$-dart to the opposite $c$-dart at that same vertex — the continuation of $c$ straight across the crossing — and $\mathrm{twin}$ then flips to the far end of that next arc. Do it again and you have marched one more arc along $c$. The splice is exactly “follow $c$ to its next crossing.”

The tour

The tour is the splice, iterated. Starting from a dart $d_0$ of $c$, the dart the tour stands on at step $k$ is $\mathrm{cont}^{[k]}(d_0)$ — and because the splice never leaves $c$, the whole tour stays on $c$, walking its arcs one per step in one direction. On a real census map this is nothing exotic: it is the decoder’s own circle-traversal run backwards. After $L$ steps it closes back to $d_0$, and $L$ is the walk’s period.

Two facts about that closed loop are assumed here rather than derived, packaged in a hypothesis called TourOK: the loop never meets its own twin (it is one direction of a two-sided traversal, not a Möbius-like double cover), and together with its twin image it covers every dart of $c$ (so $c$ is a single closed curve). These are the honest combinatorial residue of “$c$ is one embedded pseudocircle” — exactly the decoder’s single-cycle guard — and they are decidable, discharged by the kernel on every control, but not yet proved to follow from sphericity. That derivation is a named later round; nothing here pretends otherwise.

Zero or two

Walk $c$ once around and count its crossings with some other circle $i$. The answer is always $0$ or $2$, and the reason is a genuine involution, not a counting trick. The two darts of $c$ at a $\{c, i\}$ crossing vertex are swapped by $\mathrm{rot}^2$ — the very map at the heart of the splice. It is fixed-point-free at a degree-4 vertex ($\mathrm{rot}^4 d = d$ but $\mathrm{rot}^2 d \ne d$), and it lands one of each pair inside the tour’s orbit and the other in the orbit’s twin image. So the tour sees exactly one $c$-dart per crossing vertex: it crosses $i$ once for each vertex where $c$ and $i$ meet.

The pseudocircle pair axiom says two circles meet in $0$ or $2$ vertices — at the dart level, $0$ or $4$ darts — and that turns “once per vertex” into

$$\#\{\,k < L : c \text{ crosses } i \text{ at step } k\,\} \;\in\; \{0, 2\}$$

This is the hypothesis the essay calls pairs-meet-twice, and one of the two kill-checks below is a real spherical map that drops it and watches this count go to $4$.

The chain step is the gate property

Now the heart of it. Between crossing $k$ and crossing $k$+1 the tour runs along one arc of $c$. That arc has two shores — two faces of the child, one on each side. The departure corner as the tour leaves crossing $k$ is $\mathrm{face}(\mathrm{rot}\, d)$; the approach corner as it arrives at the next crossing is $\mathrm{face}(\mathrm{rot}^3 d')$, with $c$’s next dart $\mathrm{cont}^{[k+1]}(d_0)$. Two corner identities make these the two shores of the traversed arc, and a single merge step across that arc — an arc of $c$, the kind that vanishes on deletion — joins them into one class of the parent. Departure of one crossing, approach of the next: same parent face.

That merged-class equation becomes an equation of actual parent faces by cancelling the Watershed’s face correspondence, which is a bijection exactly when the child is spherical and the parent connected. What comes out the other side is the gate property:

$$\mathrm{face}(w(k+1)) \;=\; \mathrm{face}(\mathrm{twin}\, w(k))$$

where $w(k)$ is the parent half-edge the tour crosses at step $k$. Read aloud: the next crossing borders the face the walk just landed in. This is the whole content of a gate walk, and it is precisely the emit-test the Python walk-enumerator runs. It is also the one and only place the proof spends child sphericity and parent connectivity — the disconnector kill-check below drops connectivity and watches this equation fail.

How long the walk is

Because every crossed circle contributes exactly two crossings, the period is even, and it counts crossed circles two at a time:

$$L \;=\; 2 \cdot \#\{\,\text{circles that } c \text{ crosses}\,\} \;\le\; 2(n-1)$$

The bound $L \le 2(n-1)$ is not separate arithmetic; it is the same length law plus the observation that the crossed circles never include $c$ itself, so at most $n-1$ of the arrangement’s $n$ circles can be crossed. A short walk when $c$ crosses little; never longer than twice the rest of the arrangement.

The statement of record

This is the Lean, unmodified, from A250001/GrandTour.lean. First the target predicate — what it means to be a closed gate walk of period $L$ over a map $M$. Note the last two fields: they are the “$0$ or $2$ per circle, at most twice per arc” discipline the tour delivers.

structure IsGateWalk {A C : Type*} [DecidableEq A] [DecidableEq C]
    (N : DartMap A C) (w : ℕ → A × Bool) (L : ℕ) : Prop where
  /-- The walk is nonempty. -/
  pos : 0 < L
  /-- The walk is periodic with period `L` -- the sequence is cyclic. -/
  periodic : ∀ k, w (k + L) = w k
  /-- The gate property: the next crossing borders the face this crossing landed in. -/
  gate : ∀ k, N.face (w (k + 1)) = N.face (dartTwin (w k))
  /-- Every circle is crossed 0 or 2 times per period. -/
  circle_pairs : ∀ i : C, ((Finset.range L).filter (fun k => N.circ (w k).1 = i)).card = 0 ∨
    ((Finset.range L).filter (fun k => N.circ (w k).1 = i)).card = 2
  /-- Every arc is crossed at most twice per period. -/
  arc_le_two : ∀ a : A, ((Finset.range L).filter (fun k => (w k).1 = a)).card ≤ 2

Decoded: a periodic sequence of parent half-edges, each next entry bordering the face the previous crossing landed in, every circle crossed twice or not at all, every arc used at most twice. It carries no realization data — no rotation vector, no reconstructed child. That is deliberate; rebuilding the child from the walk is the next round, M-E.

The traversal well-formedness package — every field decidable, and the two honest ones (two_sided, cover) flagged:

structure TourOK (M : DartMap Arc Circle) (c : Circle) (d₀ : Arc × Bool) (L : ℕ) : Prop where
  /-- The tour is nonempty. -/
  pos : 0 < L
  /-- The tour starts on circle `c`. -/
  onC : M.circ d₀.1 = c
  /-- The tour closes up after `L` steps. -/
  closes : (M.cont)^[L] d₀ = d₀
  /-- No repetition below the period. -/
  inj : ∀ j, j < L → ∀ k, k < L → (M.cont)^[j] d₀ = (M.cont)^[k] d₀ → j = k
  /-- The tour never meets its own twin: one direction of a two-sided traversal. -/
  two_sided : ∀ j, j < L → ∀ k, k < L → (M.cont)^[j] d₀ ≠ dartTwin ((M.cont)^[k] d₀)
  /-- The tour and its twin image cover all of `c`'s darts: `c` is a single closed curve. -/
  cover : ∀ e : Arc × Bool, M.circ e.1 = c →
    ∃ k, k < L ∧ ((M.cont)^[k] d₀ = e ∨ dartTwin ((M.cont)^[k] d₀) = e)

And M-C itself — the child’s hypotheses (legal deletion, sphericity $\chi(M) = 2$, connected parent), plus TourOK, plus pairs-meet-twice (hpairs: every $\{c, i\}$ met in $0$ or $4$ darts), yielding an IsGateWalk of the parent:

theorem grand_tour (h : M.DeleteOK c) (heuler : M.eulerChar = 2)
    (hM : (M.deleteCircle c h).DartConnected) {d₀ : Arc × Bool} {L : ℕ}
    (ht : M.TourOK c d₀ L)
    (hpairs : ∀ i : Circle, (Finset.univ.filter (fun e : Arc × Bool =>
        M.circ e.1 = c ∧ M.circ (M.rot e).1 = i)).card = 0 ∨
      (Finset.univ.filter (fun e : Arc × Bool =>
        M.circ e.1 = c ∧ M.circ (M.rot e).1 = i)).card = 4) :
    IsGateWalk (M.deleteCircle c h) (M.tourGate c h ht.onC) L := by
  -- circle_pairs from tour_circle_count (the rot² involution); the gate property
  -- from tourGate_step (the merge-chain step cancelled through the Watershed's
  -- bijectivity); periodicity and arc_le_two by Finset bookkeeping over the orbit.

Decoded: this is the extraction half of L4-conn made a theorem. Every combinatorial child yields walk data over its parent. It does not say a search enumerates that data (the Python seam G-W2), nor that reassembling the walk rebuilds the child (M-E). One extracted witness per child; no completeness of any kind is claimed.

Two hypotheses you can watch fail

Neither hpairs nor parent connectivity is decoration, and the module proves it the honest way: for each, a real spherical map that satisfies every other hypothesis and defeats the conclusion in the kernel.

The first is the quad: a ring (label 0), two beads both given label 1, and a satellite (label 2). It is spherical, its deletion is the connected chain bead–satellite–bead, and its tour is well-formed — but the ring crosses label 1 at four vertices, so pairs-meet-twice fails, and with it the walk: the tour crosses label 1 four times, and circle_pairs demands $0$ or $2$.

theorem grand_tour_without_pairs_is_false :
    ¬ (∀ (Arc Circle : Type) [DecidableEq Circle] [Fintype Arc] [LinearOrder Arc]
        (M : DartMap Arc Circle) (c : Circle) (h : M.DeleteOK c),
        M.eulerChar = 2 → (M.deleteCircle c h).DartConnected →
        ∀ (d₀ : Arc × Bool) (L : ℕ) (ht : M.TourOK c d₀ L),
        IsGateWalk (M.deleteCircle c h) (M.tourGate c h ht.onC) L) := by
  intro hall
  exact quad_not_gateWalk
    (hall (Fin 16) (Fin 3) quad 0 quad_deleteOK quad_eulerChar quadDel_dartConnected
      _ 4 quad_tourOK)

The second is the disconnector: five circles, two lens pairs joined only through a shared circle. Deleting the shared circle keeps pairs-meet-twice (it meets each of the other four in exactly two vertices) and a well-formed period-8 tour — but the parent falls apart into two separate lenses, and the gate property fails at step 2. Between its crossings of the left pair and the right pair, the deleted circle runs through a region whose two shores now lie on different spheres, so the faces the walk must match are not the same face at all. That is precisely the step where the Watershed’s bijectivity — hence connectivity — was spent.

theorem grand_tour_without_connected_is_false :
    ¬ (∀ (Arc Circle : Type) [DecidableEq Circle] [Fintype Arc] [LinearOrder Arc]
        (M : DartMap Arc Circle) (c : Circle) (h : M.DeleteOK c),
        M.eulerChar = 2 →
        ∀ (d₀ : Arc × Bool) (L : ℕ) (ht : M.TourOK c d₀ L),
        (∀ i : Circle, (Finset.univ.filter (fun e : Arc × Bool =>
            M.circ e.1 = c ∧ M.circ (M.rot e).1 = i)).card = 0 ∨
          (Finset.univ.filter (fun e : Arc × Bool =>
            M.circ e.1 = c ∧ M.circ (M.rot e).1 = i)).card = 4) →
        IsGateWalk (M.deleteCircle c h) (M.tourGate c h ht.onC) L) := by
  intro hall
  exact disconnector_not_gateWalk
    (hall (Fin 24) (Fin 5) disconnector 4 disconnector_deleteOK disconnector_eulerChar
      _ 8 disconnector_tourOK disconnector_pairs)

The chain, toured end to end

The figure’s three-circle chain is not a cartoon; it is the module’s live positive control, run through the theorem with every hypothesis discharged by the kernel. Circle 0 crosses only circle 1, at two vertices, so its tour has period $2$ and both steps cross circle 1:

theorem threeChain_grand_tour :
    IsGateWalk threeChainDel
      (threeChain.tourGate 0 threeChain_deleteOK threeChain_tourOK.onC) 2 :=
  threeChain.grand_tour 0 threeChain_deleteOK threeChain_eulerChar
    threeChainDel_dartConnected threeChain_tourOK threeChain_pairs

The payoff is the per-arc case. Deleting circle 0 fuses three of circle 1’s four arcs into a single parent arc, and both of the tour’s gate entries land on that one fused arc — so this walk exercises “an arc used twice,” not merely “a circle crossed twice”:

theorem threeChain_tour_same_arc :
    (threeChain.tourGate 0 threeChain_deleteOK threeChain_tourOK.onC 0).1 =
      (threeChain.tourGate 0 threeChain_deleteOK threeChain_tourOK.onC 1).1 := by
  decide

And an independent threeChain_gate_decide confirms the gate property at both steps by raw kernel computation, off the theorem’s proof path entirely — the same double-entry discipline the rest of the census uses. The control does not rest on the theorem being right; it checks the same number a second way.

What’s proved, and what isn’t

Proved, kernel-checked, standard axioms only (propext, Classical.choice, Quot.sound; every concrete check a kernel decide, no native_decide, no sorry): from a spherical child, a legal deletion with connected parent, a well-formed tour, and pairs-meet-twice, the tour’s gate sequence is a closed gate walk of the parent, of the length the crossing count dictates. Both load-bearing hypotheses are shown genuinely load-bearing by real maps that fail without them. The trust label is PROVED-about-model: this is gate-sequence extraction, and no more.

Open seams, named rather than glossed:

• Extraction only. M-C proves the trail exists and is a walk. That a search enumerates those walks is the Python seam G-W2; that a walk’s assembly rebuilds the child — and rebuilds exactly the one it came from — is M-E, the next round. Neither is attempted here, and no completeness claim of any kind is made.
• TourOK’s two_sided and cover. “$c$ is a single two-sided closed curve” is an extra hypothesis beyond the combinatorial core of L4-conn, assumed here as decidable fields. It is expected to follow from sphericity, and deriving it is the job of a later round, P-1, “Sphericity’s Dividends”; if that lands, these fields retire.
• IsGateWalk carries no realization data. The forward/rotation vector that would let one rebuild the child is deliberately omitted from the predicate, deferred to M-E.
• DeleteOK.twinKNe. The “no one-sided Möbius fused run” field is inherited from M-A as a decidable hypothesis, geometrically expected from $\chi = 2$ but not proved from it — the same P-1 target.

None of this is a defect in M-C. It is the honest shape of one increment in a multi-round infrastructure build: the deleted circle’s trail is now a theorem, a closed walk over the parent with every hypothesis either discharged or named — and firewalled cold review has watched both the walk and its two kill-checks fire in the kernel. The walk exists. Making it enumerate the census, and rebuild it, is the road ahead.