Sphericity’s Dividends

P-1 · todo/lean/070 · leg-4 program · kernel-checked, promoted 2026-07-17 (3063c0b)

The Grand Tour proved that when you delete a circle $c$ from a spherical arrangement, the traversal of $c$ becomes a gate walk on the parent map that survives the deletion — but it proved this only after assuming three geometric facts it could not yet derive. This round derives all three from sphericity itself, so a spherical census map now satisfies the Grand Tour’s hypothesis with no hand-supplied geometric field.

What the Grand Tour assumed

M-C packaged the well-formedness of a tour into a structure TourOK, and the well-formedness of a deletion into DeleteOK. Four of TourOK’s fields are pure period bookkeeping: that the tour has positive length $L$, starts on $c$, closes after $L$ splice steps, and visits $L$ distinct darts. Those define the walk. Three further fields were something else entirely — each carried in the source with the same apology, “geometrically expected from sphericity, but not derived from it here”:

• two_sided — the tour of $c$ never meets its own twin. The traversal is one bank of a two-sided curve, not a Möbius-like double cover.
• cover — the tour together with its twin image covers all of $c$’s darts. The label $c$ names a single closed curve.
• twinKNe (on DeleteOK, inherited from circle deletion, M-A) — no fused run of the deletion closes back onto its own starting dart. Fused arcs have two distinct ends.

These were decidable fields: a particular census map could pay for each with a per-map decide. But paying is not proving, and a hypothesis you always discharge by computation is still a hypothesis. P-1 removes all three from the caller’s hands.

What sphericity buys: the side function

Sphericity, in this tree, is three combinatorial conditions on a dart map $M$: it is DartConnected, its crossings are ProperCrossings (every vertex is a genuine transversal crossing of two circles), and its Euler characteristic is $\chi = 2$. From exactly this, the promoted stack manufactures the one object every argument below runs on. First isCut_of_spherical certifies that each circle cuts the sphere; then sideFn_exists promotes that cut to a side function

$$\sigma_i : \operatorname{Face} \longrightarrow \mathbb{Z}/2$$

for the chosen circle $i$, a two-colouring of the faces that flips exactly when you step across a dart of circle $i$ and stays put across every other dart. Read at the corner faces of a single dart, $\sigma$ obeys two step laws, both shape-free — ProperCrossings does not enter here, only later.

The twin flip. Crossing from a dart to its twin crosses the dart’s own arc, so $\sigma$ moves by the indicator of “this dart’s circle is $i$” (sideFn_face_dartTwin):

$$\sigma_i\!\big(\operatorname{face}(\operatorname{twin} d)\big) \;=\; \sigma_i\!\big(\operatorname{face} d\big) \;+\; \big[\operatorname{circ} d = i\big].$$

The splice step. One splice step $\operatorname{cont} = \operatorname{twin}\circ\operatorname{rot}^2$ crosses exactly the crossed strand’s arc, so $\sigma$ moves by the indicator that the strand crossed at that vertex lies on $i$ (sideFn_face_cont). These two laws are the whole engine; the three dividends are three ways of reading them.

Two-sidedness, from the flip

Walk the tour of $c$. Every splice step passes straight through a vertex, and by the ProperCrossings alternation the strand it crosses there belongs to another circle, never to $c$ itself. So the splice-step indicator for $i = c$ is always zero, and $\sigma_c$ is constant along the entire tour (sideFn_face_tour): every iterate $\operatorname{cont}^{m}(d_0)$ lands on a face with the same $\sigma_c$ as $d_0$.

A twin dart of a tour dart, by contrast, sits on the flipped side: at a $c$-dart the twin-flip indicator is $1$, so its face carries $\sigma_c(\operatorname{face} d_0) + 1$. If some tour dart equalled the twin of some tour dart, reading $\sigma_c$ on both sides of that equation would force

$$\sigma_c f \;=\; \sigma_c f + 1 \qquad\text{in } \mathbb{Z}/2,$$

which is false. That is the entire proof, and it holds for every pair of steps $j, k$ — no “within one period” window is needed, because the side value does not care how far around the tour you have walked.

theorem tour_two_sided_of_spherical (hconn : M.DartConnected) (hp : M.ProperCrossings)
    (heuler : M.eulerChar = 2) {d₀ : Arc × Bool} (hd₀ : M.circ d₀.1 = c) (j k : ℕ) :
    (M.cont)^[j] d₀ ≠ dartTwin ((M.cont)^[k] d₀) := by
  obtain ⟨σ, hσ⟩ := M.toArrMap.sideFn_exists (M.toArrMap_connected hconn) c
    (M.isCut_of_spherical hconn hp heuler c) (M.face d₀)
  intro hjk
  have h1 : σ (M.face ((M.cont)^[j] d₀)) = σ (M.face d₀) :=
    M.sideFn_face_tour c hp hσ hd₀ j
  have h2 : σ (M.face (dartTwin ((M.cont)^[k] d₀))) = σ (M.face d₀) + 1 := by
    rw [M.sideFn_face_dartTwin hσ, if_pos ((M.circ_cont_iter hp d₀ k).trans hd₀),
      M.sideFn_face_tour c hp hσ hd₀ k]
  rw [hjk, h2] at h1
  exact (by decide : ∀ x : ZMod 2, x + 1 ≠ x) _ h1

The two haves are the two banks: the tour side (h1) and the flipped side (h2). Their collision is a contradiction in $\mathbb{Z}/2$, discharged by a one-line decide.

The same flip, for twinKNe

The deletion of $c$ fuses each pair of arcs that met $c$ into a single run. DeleteOK.twinKNe asks that no such run be Möbius-like — that a fused run never resolves back onto its own starting dart. This is the two-sidedness argument again, run along the fused circle $i = \operatorname{circ} d$ rather than along $c$. Every step a fused run absorbs is a step across $c$ itself, and $c \ne i$, so $\sigma_i$ is constant along the run (sideFn_face_resolveFuel); meanwhile $\operatorname{twin} d$ sits on the flipped side of $i$. So $\operatorname{resolve} c\,(\operatorname{twin} d) \ne d$. The constancy law is stated in fuel form, which means it covers runs that never terminate — so the theorem needs neither the Kept guard nor DeleteOK.resolves, and it retires the field M-A had carried since the circle-deletion round.

Cover, and an honest consolidation

The third field is different in kind, and this is the part the essay must not overstate. cover is derived not from sphericity but from CircleFaithful, the decoder’s S1 axiom that one label names one closed curve. The bridge is arithmetic on the rotation. The splice undoes the decoder’s traversal successor $\sigma = \operatorname{rot}^2\!\circ\operatorname{twin}$ — on a degree-4 map $\operatorname{rot}^4 = 1$, so $\operatorname{cont} = \sigma^{-1}$ as permutations (contEquiv_eq_sigmaPerm_inv). Splice orbits are $\sigma$-orbits. CircleFaithful’s forward direction says every dart of $c$ lies in the $\sigma$-orbit of $d_0$ or of its twin; convert those to splice orbits, reduce the exponent modulo the period $L$, and it lands on an iterate below $L$.

Here is the honesty. The forward direction of CircleFaithful, restricted to $c$, is content-coextensive with cover — it says the same thing. So P-1 does not derive cover from something strictly weaker. It consolidates cover into the standing S1 decoder axiom: a property that is already required, sits upstream of the tour machinery (it is defined from $\operatorname{circ}$, $\sigma$, and $\operatorname{twin}$ alone), is independently consumed by the decoder, and is discharged on census maps by decide. That is a genuine un-conditionalization, not a derivation from nothing: cover stops being a bespoke tour hypothesis and becomes a consequence of a decoder property the pipeline already pays for. The firewalled cold review confirmed this reading — that CircleFaithful is genuinely upstream, not cover under a new name.

theorem tour_cover_of_faithful (hp : M.ProperCrossings) (hfaith : M.CircleFaithful)
    {d₀ : Arc × Bool} {L : ℕ} (hd₀ : M.circ d₀.1 = c) (pos : 0 < L)
    (closes : (M.cont)^[L] d₀ = d₀) :
    ∀ e : Arc × Bool, M.circ e.1 = c →
      ∃ k, k < L ∧ ((M.cont)^[k] d₀ = e ∨ dartTwin ((M.cont)^[k] d₀) = e) := by
  intro e hce
  have hreach : ∀ x : Arc × Bool, M.sigmaPerm.SameCycle d₀ x →
      ∃ k, k < L ∧ (M.cont)^[k] d₀ = x := by
    intro x hx
    have hx' : M.contEquiv.SameCycle d₀ x := by
      rw [M.contEquiv_eq_sigmaPerm_inv hp]
      exact Equiv.Perm.sameCycle_inv.mpr hx
    obtain ⟨z, hz⟩ := hx'
    obtain ⟨k, hk, hke⟩ := M.exists_iterate_lt_of_zpow pos closes z
    exact ⟨k, hk, by rw [hke, hz]⟩
  rcases (hfaith d₀ e).mp (hd₀.trans hce.symm) with h | h
  · obtain ⟨k, hk, hke⟩ := hreach e h
    exact ⟨k, hk, Or.inl hke⟩
  · obtain ⟨k, hk, hke⟩ := hreach (dartTwin e) h
    refine ⟨k, hk, Or.inr ?_⟩
    rw [hke, dartTwin_dartTwin]

hreach is the bridge: same $\sigma$-cycle becomes same splice-cycle via $\operatorname{cont} = \sigma^{-1}$, then the exponent is squeezed below $L$. The final rcases is the two cases of CircleFaithful — the dart, or its twin.

The constructors that un-condition M-C

The deliverable is deliberately non-invasive. TourOK and DeleteOK keep their fields, so every decide-built control already in the tree still type-checks unchanged. What changes is how the geometric fields get filled. TourOK.of_spherical builds a full TourOK from the four period fields plus sphericity plus faithfulness, deriving two_sided and cover; deleteOK_of_spherical builds a DeleteOK from its combinatorial guards plus sphericity, deriving twinKNe.

theorem TourOK.of_spherical {Arc Circle : Type*} [DecidableEq Circle] [Fintype Arc]
    [DecidableEq Arc] {M : DartMap Arc Circle} {c : Circle}
    (hconn : M.DartConnected) (hp : M.ProperCrossings) (heuler : M.eulerChar = 2)
    (hfaith : M.CircleFaithful) {d₀ : Arc × Bool} {L : ℕ}
    (pos : 0 < L) (onC : M.circ d₀.1 = c) (closes : (M.cont)^[L] d₀ = d₀)
    (inj : ∀ j, j < L → ∀ k, k < L → (M.cont)^[j] d₀ = (M.cont)^[k] d₀ → j = k) :
    M.TourOK c d₀ L :=
  ⟨pos, onC, closes, inj,
    fun j _ k _ => M.tour_two_sided_of_spherical c hconn hp heuler onC j k,
    M.tour_cover_of_faithful c hp hfaith onC pos closes⟩

The anonymous constructor’s last two slots are the two dividends. Everything a caller supplies — connectivity, properness, $\chi = 2$, faithfulness, and the period data — is a decidable decoder guard on a census map. To prove the constructors bite, the M-A and M-C control packages are rebuilt through them (threeChain_tourOK_derived, threeChain_deleteOK_derived) on the real three-chain lens geometry, with threeChain_circleFaithful a genuine decide — so the theorems run end to end on a geometry-read map and cannot pass vacuously.

Sufficient, never necessary

The two-sidedness theorems claim only that sphericity suffices. They never claim it is necessary, and the source is careful about the difference. The connectivity and Euler hypotheses enter exactly once, through isCut_of_spherical, and no kill-check deleting them is offered — none is expected to exist. A dart map is a rotation system, a rotation system always presents an orientable surface, and an embedded closed curve on an orientable surface is two-sided at every genus.

The prose evidence, fenced as prose and not kernel: an exhaustive sweep of every ProperCrossings rotation system on three or fewer vertices under its finest circle labelling — 109,764 maps, including surfaces of $\chi = 0$ and $\chi = -2$ — found no violation of either two-sidedness conclusion. Both conclusions are labelling-robust (cont never reads the circle labels, and a fused run follows one strand whatever the labels), which is exactly what the orientability reading predicts. A $\chi$-free combinatorial proof would need orientation-transport machinery this tree does not carry, and every census map is spherical, so the stronger statement would buy the program nothing.

Where faithfulness is load-bearing

cover is the opposite case: its hypothesis is necessary, and there is a kernel kill-check to prove it. The quad is a real spherical map — two geometric circles $B_1$ and $B_2$ that share the single label $1$. It is dart-connected, proper, and has $\chi = 2$: fully spherical. But it is not CircleFaithful, because label $1$ names two closed curves, not one. The label-$1$ tour launched from a $B_1$ dart closes with period $4$ and never once reaches a dart of $B_2$.

So tour_cover_without_faithful_is_false is a kernel theorem: strike hfaith from tour_cover_of_faithful, keep everything else including full sphericity, and the statement is false on the quad. That is the precise line between the two kinds of dividend. Two-sidedness comes free from the surface being a sphere; cover needs the extra, decidable promise that a label is a curve.

What’s proved, and what isn’t

Proved. All three geometric fields the Grand Tour carried are discharged. two_sided and twinKNe are derived from sphericity through the side function; cover is consolidated into the standing CircleFaithful S1 axiom, which census maps satisfy by decide. Through the constructors, a spherical census map satisfies TourOK and DeleteOK with no geometric field supplied by hand — M-C is un-conditioned on the maps the program actually enumerates.

The fences, stated plainly. cover is consolidated, not derived from nothing — it rests on a decoder axiom of the same content, chosen because that axiom is already required and independently checked. A $\chi$-free proof of two-sidedness is deliberately not attempted; it would need orientation-transport the tree lacks and would buy nothing, since census maps are spherical. The pairs-meet-twice condition hpairs is left where it belongs, as a genuine pseudocircle axiom the spherical quad violates — not a sphericity consequence. And the S2 fence — that a dart map’s faces are the regions of a sphere arrangement — is the program’s single classical citation and is never entered here.

The module is firewalled-Opus cold-review CONFIRMED on standard axioms only (propext, Classical.choice, Quot.sound); every check is a kernel decide, with no native_decide and no sorry. The Grand Tour flagged three open conditions. This is the note that closes them.