the Watershed

M-A · todo/lean/070 · leg-4 program, round 2 · kernel-checked, promoted 2026-07-17 (f489419)

Erase one circle from an arrangement and every circle that used to cross it doesn’t stop at the erased crossing — it keeps going straight through, the way a road keeps going once you tear down the fence that used to cut across it. Do that at every one of the erased circle’s crossings, and the faces that circle used to keep apart on either side flow together into single, larger faces. That flowing-together is where this essay gets its name. But the round actually proves two things at once, under one argument, and the quieter one is just as real: while the faces are busy merging, the sphere’s Euler characteristic — the plain count $\chi = V - E + F$ — never notices. It stays exactly 2, the whole way through.

This project calls the quiet half the Bookkeeper and the loud half the Watershed. Both are theorems about deleteCircle, the Lean surgery that removes one circle c from a DartMap — the census’s combinatorial model of a circle arrangement — by splicing each crossed circle’s two arc-ends together at every vertex c used to own.

The two results, by hand

Let $M$ be a spherical map ($\chi(M) = 2$) and $c$ one of its circles, crossing others at $D$ vertices — so $c$ itself is cut into $D$ arcs by those $D$ crossings. Write $M' = M \setminus c$ for the deleted map. Deletion’s bookkeeping is blunt: the $D$ vertices vanish ($V' = V - D$), and the arcs drop by $2D$ — $c$’s own $D$ arcs, plus one more per fusion, since each deleted vertex welds two arcs of the crossed circle into one ($E' = E - 2D$). Faces merge along $c$, dropping by $D$ ($F' = F - D$). Add it up and the drops cancel exactly:

$$\chi(M') = (V - D) - (E - 2D) + (F - D) = V - E + F = \chi(M) = 2$$

The Bookkeeper is that sentence made a theorem, given one honest proviso: $M'$ itself has to still be one connected piece. Sphericity of the input never does more work than supplying the single number $\chi(M) = 2$; nothing about the input’s own connectivity is needed anywhere in the argument.

The Watershed names the correspondence underneath that arithmetic: a surjection $\text{facePush} : \text{Face}(M) \to \text{Face}(M')$, and its fibers are exactly the classes of $M$’s faces you can reach from one another by crossing $c$’s arcs — $F \sim G$ generated by “$F$ and $G$ are the two faces on either side of one of $c$’s arcs.” Two faces of the original arrangement land on the same face of the deleted one exactly when the deleted circle used to be the only thing standing between them.

Why the obvious proof is wrong

There is a tempting one-line proof of the Bookkeeper that this round deliberately does not take. It goes: c has D crossings; erasing each one merges exactly one pair of faces; so F drops by exactly D, full stop. It sounds like something you could verify by walking around $c$ once and tallying. It is false, and finding out why is the actual content of this round.

The tally silently assumes that none of those $D$ local merges ever repeats work — that you can never reach one face from another two different ways by crossing two different arcs of $c$. Formally: build a graph whose vertices are $M$’s faces and whose $D$ edges are $c$’s arcs, each edge joining the two faces it separates. The naive count “F drops by exactly D” is exactly as true as that graph having no cycle — being a forest. On a sphere with a connected complement, it is a forest, and the naive count happens to be right. But the equivalence itself doesn’t know that: on a map with a handle (a route back around through the missing genus), or one that comes apart into separate pieces once $c$ is gone, the same graph can carry a cycle, and the tally silently over-predicts how many faces actually vanish. This round makes the disconnection case a kernel fact, not an assertion: a five-circle map with two lens pairs joined only through one shared circle deletes to $\chi' = 4$ — two disjoint spheres, not one — and, on that same map, the deleted map has more surviving faces than merge classes, so facePush is provably surjective there but cannot possibly be injective.

So the module does not count locally at all. It proves both results at once with a squeeze:

$$\#\text{classes} \;\le\; F' \;\le\; F - D \;\le\; \#\text{classes}$$

The left step is $\bar\psi$’s surjectivity — every merge class is hit by some face of the deleted map — and it needs no hypothesis at all: it holds even when the deletion disconnects. The right step is pure linear algebra over $\mathbb{F}_2$: functions constant on merge classes are exactly the kernel of a difference map over $c$’s $D$ arcs, so rank–nullity bounds the class count below by $F - D$, again unconditionally. The middle step is the only place anything geometric gets consumed — eulerChar_le_two, Euler’s inequality that a connected map’s $\chi$ never exceeds 2 (genus is never negative), applied to the deleted map itself. That is the one and only step that needs $M'$ connected. Once it holds, all three quantities in the squeeze collapse to one number: $\bar\psi$ is a bijection (the Watershed), and $\chi(M') = 2$ falls out as a corollary (the Bookkeeper) — the face-drop is derived, not assumed.

An adversarial cold review checked this squeeze does not smuggle sphericity in through a side door: all eight building blocks behind eulerChar_le_two were confirmed to carry no sphericity hypothesis of their own, so the inequality really is genus $\ge 0$ for any connected map, full stop — not sphericity in disguise. The review also reproduced the chain-to-lens control from scratch, confirmed MergeStep is the right reading of “adjacent across $c$,” and watched both kill-checks fire in the kernel.

The statement of record

This is the Lean, unmodified, from A250001/CircleDeletion.lean. First the domain the surgery is allowed to run on — note which field is a hypothesis, not a derived fact:

structure DeleteOK [Fintype Arc] : Prop where
  /-- Every vertex is a proper degree-4 crossing of two distinct circles. -/
  proper : M.ProperCrossings
  /-- Every non-`c` dart resolves to a kept dart: no free loops. -/
  resolves : ∀ d : Arc × Bool, M.circ d.1 ≠ c → M.Kept c (M.resolve c d)
  /-- No fused run returns to its own starting dart: fused arcs have two distinct ends. -/
  twinKNe : ∀ d : Arc × Bool, M.Kept c d → M.resolve c (dartTwin d) ≠ d

Decoded: resolves rules out a circle whose only crossings were all with c — delete c and it would be left as a closed curve with no crossings at all, which a DartMap simply cannot represent. twinKNe rules out a fused run that loops back onto its own start — a Möbius-like one-sided circle. It is geometrically expected to be impossible whenever $\chi = 2$, but that derivation is not proved here; it stands as an honest, decidable hypothesis field, discharged by decide on every concrete control.

Euler’s inequality — the squeeze’s one geometric step, and the only place connectivity of the deleted map is consumed:

theorem eulerChar_le_two [Nonempty Arc] [Fintype M.Vertex] [Fintype M.Face]
    (hconn : M.DartConnected) : M.eulerChar ≤ 2 := by
  -- assembled from IsCutFromSphere.lean's 𝔽₂ machinery: the vertex-chain span
  -- sits inside the cycle space with dimension V − 1; the cycle space itself
  -- has dimension E − F + 1. So V − 1 ≤ E − F + 1, i.e. χ ≤ 2. No sphericity
  -- hypothesis anywhere in the chain.

The Bookkeeper:

theorem eulerChar_deleteCircle (h : M.DeleteOK c) (heuler : M.eulerChar = 2)
    (hM : (M.deleteCircle c h).DartConnected) :
    (M.deleteCircle c h).eulerChar = 2

Decoded: given a legal deletion (h), a spherical input (heuler), and a connected result (hM), the result is spherical too. That third hypothesis is the honest price of admission — deletion does not, in general, preserve connectivity, and this file kernel-refutes the claim that it does (a five-circle map whose one shared circle is the only thing joining two otherwise-disjoint lens pairs; delete it and $\chi'$ jumps to 4).

The Watershed, assembled from its three parts:

noncomputable def facePush (h : M.DeleteOK c) (heuler : M.eulerChar = 2)
    (hM : (M.deleteCircle c h).DartConnected) :
    M.Face → (M.deleteCircle c h).Face := fun F =>
  (Equiv.ofBijective _ ((M.faceClassOfDeleted_bijective_and_card c h heuler hM).1)).symm
    (M.mergeClass c F)

theorem facePush_surjective (h : M.DeleteOK c) (heuler : M.eulerChar = 2)
    (hM : (M.deleteCircle c h).DartConnected) :
    Function.Surjective (M.facePush c h heuler hM)

theorem facePush_eq_iff (h : M.DeleteOK c) (heuler : M.eulerChar = 2)
    (hM : (M.deleteCircle c h).DartConnected) (F G : M.Face) :
    M.facePush c h heuler hM F = M.facePush c h heuler hM G
      ↔ Relation.EqvGen (M.MergeStep c) F G

Decoded: facePush sends every face of the original map to a face of the deleted one; facePush_surjective says every deleted-map face is hit; facePush_eq_iff says two original faces land on the same deleted-map face exactly when they are joined by a chain of “adjacent across one of $c$’s arcs” steps — Relation.EqvGen being the equivalence relation generated by that one adjacency step. Non-vacuously exercised: deleting one circle from a three-circle chain fuses three of the crossed circle’s arcs into one, kernel-verified isomorphic to the two-circle lens, and two provably distinct faces of the chain are shown to land on the same face of the result.

Why it matters

M-A is infrastructure for L4-conn, the leg-4 program’s crossing-insertion completeness statement over connected arrangements — the one completeness route for this census that does not lean on Felsner–Scheucher’s published count at all. That independence matters twice over: A288568 stops at n=6, so anything at n=7 has no external count to check against, and L4-conn is the only route that proves completeness by construction, one insertion at a time, rather than by tallying against an outside source. deleteCircle is the machinery that lets the program walk a census type backward, one non-cut circle at a time, to a smaller connected parent it can induct on — and the Bookkeeper is what certifies that parent is still a genuine spherical arrangement, not an artifact of the surgery. The Watershed’s face correspondence is what the next round, M-C, “the Grand Tour,” will walk: extracting the gate sequence that c’s crossings trace out, using exactly the fact that consecutive crossings’ faces land on the same parent face.

Read the scope honestly: L4-conn itself is not proved anywhere in this repository yet. M-A is one building-block lemma in a scoped, multi-round program (todo/lean/070 names the whole decomposition, M-A through M-H); the assembled completeness theorem is several rounds away and depends on infrastructure — the gate-sequence extraction, the realization determinism, the non-cut-circle existence bridge — that has not been built.

What’s proved, and what isn’t

Proved, kernel-checked, standard axioms only: given a legal deletion and a spherical input whose deletion happens to stay connected, the deleted map is spherical (the Bookkeeper) and its faces are exactly the original faces merged along the deleted circle’s arcs (the Watershed) — by one non-circular squeeze, not by an unsound local count. The connectivity-can-fail fact (M-A4) is itself kernel-checked: an explicit five-circle map witnesses deletion falling apart, with $\chi' = 4$.

Open seams, named rather than glossed:

• DeleteOK.twinKNe. No Möbius-like, one-sided fused run is excluded as a decidable hypothesis field, not a derived fact. It is geometrically expected to follow from $\chi = 2$ on every genuine census map, but that derivation is not proved here — a named later-round cleanup.
• Model faithfulness. The whole construction is DartMap-faithful: the crossing-only, single-cluster fragment this project’s census keyer already models. MergeStep’s reading of “adjacent across $c$” rests on territory-nesting facts that stay fenced at Sd2, the un-formalizable topological-reading layer this program enters once and never re-derives.
• M-A5, deferred. That a non-cut circle actually exists to delete — wiring the already-kernel-checked graph fact in ConnectedDescent.lean to DartConnected — is named and left for a later round.
• L4-conn itself. The completeness statement this whole program serves is not proved anywhere yet. M-A is a load-bearing piece of a scoped, multi-month infrastructure build, not a shortcut to the finish line.

None of this is a defect in M-A. It is the honest shape of infrastructure: two results, proved together, by an argument disciplined enough to catch its own most tempting shortcut before it became a bug.