Leg-4 wants to prove that the census is complete: every connected single-cluster spherical arrangement of pseudocircles is one the enumerator actually emits, with nothing missed. The route this file assembles avoids the FreeSet count entirely and reaches completeness by descent: delete one circle, land on a smaller arrangement, and lean on the claim already established for the smaller one. That is an induction on the number of circles, and this note is about the induction skeleton — now stated over the real census vocabulary and swept by the trusted test base, but still conditional on two named open seams. It is a milestone, not the leg-4 QED.
Fix a child arrangement with circles. Choose one of its circles — call it c — and delete it. Deletion, , is M-A’s deleteCircle: erase the circle, splice the arcs that its removal orphans, and keep the rest of the arrangement intact. If the circle you deleted was non-cut — if erasing it does not sever the rest into pieces — the parent is again a connected single-cluster arrangement, now with circles. That is the descent: circles to .
scratch/atlas-connected-completeness/geometry_check.py: centres sit on an equilateral triangle of side 50 with radius 45, every pairwise centre-distance is 50 (a proper two-point crossing needs it under 90), the six crossings are the coordinates the dots are drawn at and are pairwise distinct, V − E + F = 6 − 12 + 8 = 2 confirms the spherical embedding, and deleting c provably leaves a b connected.The engine of the step is a single theorem, child_walk_reduction, and it carries no seam — it is pure glue between two already-promoted results, on the standard axioms alone. Given a spherical child () whose deletion of c stays connected, a well-formed tour of c (TourOK), and the pseudocircle pairs law (each circle meets c in zero or two crossings):
grand_tour) extracts from the tour of c a closed gate walk on the parent — a combinatorial trace that survives the deletion; andrealization_determinism) reassembles that walk data — its length, its sided gate sequence, and the position vector posW read off the child — back into a map that is DartIso to the child itself.Put together, every spherical single-cluster child equals, up to isomorphism, the walk-assembly over its connected parent:
This is the faithfulness half of the enumeration: the child is reconstructible from parent-plus-walk, so nothing about the child is lost in the descent. The geometric side-conditions cost a census map nothing beyond its decoder guards — P-1 (“Sphericity’s Dividends”) already derives TourOK’s two-sidedness and cover, and DeleteOK’s twinKNe, from sphericity and faithfulness, so a spherical census map satisfies the hypotheses with no hand-supplied field. M-A supplies the deletion and its Euler bookkeeping. The core is where leg-4 is genuinely solid.
Completeness at a level is one clean predicate: Complete k says every connected single-cluster spherical type with exactly circles is emitted. The step is complete_step:
The proof of the step reads exactly as the picture: take a child at level ; its recorded parent sits at level and is emitted by the induction hypothesis; the forward core exhibits as the walk-assembly over that parent; so the seam (below) emits . The statement of record, connected_completeness, wraps this in strong induction on , with a finite base hbase for — the one-and-two-circle arrangements (lens and vesica), checked at assembly level rather than descended into. No FreeSet cardinality and no |T| hypothesis enters anywhere: the count is replaced by the by-construction descent.
The honest weight of this integration is one word: whose types. The first pass of M-H rebuilt a local iso-or-mirror quotient of its own, because the pre-fix M-E re-used names (crossAt, mirrorIso) that collided in the shared namespace with 060’s census machinery, so the two files could not be imported together. A pure rename on develop removed the collision, and this file now imports A250001.CensusComplete and reuses 060’s real PackedMap, IsoOrMirror, SphereType, and — the very quotient the connected count-match (census_count_match) is proved over. So Emitted : SphereType → Prop ranges over the same “types” the census keys, and connected_completeness is a statement about the census, not a self-contained reassembly that would have to be re-glued to it later. The full build is green (lake build A250001 A250001.Tests, 8512 jobs) with M-H swept into the trusted Tests base, on axioms [propext, Classical.choice, Quot.sound] only.
One structural wrinkle had to be handled honestly. 060’s PackedMap bundles a Fintype and a DecidableEq on its arc carrier but no linear order — while the forward core (deleteCircle, tourGate, posW) needs [LinearOrder Arc] to talk about dart order. The bridge is packedLinOrd: a canonical order pulled back from Fin n via the bundled finiteness. The subtlety is that a LinearOrder in Lean carries its own DecidableEq (through toDecidableEq), and if that derived equality were a different term from the census’s decEqArc, the geometry’s notion of “equal arcs” and the key’s notion would fork — a genuine instance diamond, and the kind of thing that lets two theorems quietly be about two different objects. The fix is to override the field so it is defeq to the census one:
with compare likewise pinned to compareOfLessAndEq (rfl) so the override still assembles a coherent order. The cold review confirmed this diamond genuinely collapses at defeq. Because the completeness statement is itself DecidableEq-agnostic (SphereType, , and DartIso do not depend on which order stands in for Fin n’s native one), which order is chosen is immaterial to what is proved — but the pin is what keeps the geometry and the key provably talking about the same arcs.
This is the part that must not be buried. connected_completeness is not closed inside Lean. Two steps of the argument have no producer anywhere in the tree, and both are taken as named explicit hypotheses of the theorem — not sorry, not an axiom, not a weakening to vacuity, but honest inputs the theorem is conditional on.
Seam)That the region-walk DFS actually emits the gate walk M-E reassembles (G-W2), and that the keyer keys that emission into the census’s emitted set (G-W4 = 060’s K1 + G3). In Lean terms:
There is no Lean model of “the emitted set” or “the DFS,” so this is a hypothesis of the theorem, discharged nowhere here. It is the fundamentally external seam.
ReductionData.hparConn)That deleting a non-cut circle leaves the parent DartConnected — the very fact the figure’s right panel asserts. CrossingGraphBridge.lean (M-A5) explicitly fences the missing bridge lemma (that the crossing graph of the deletion is the induced subgraph) as “M-H, not M-A5,” so exists_noncut_vertex cannot yet be threaded through to a connected deletion. It is carried per child as a field of ReductionData.
Everything else in ReductionData — the deletion’s well-formedness, the tour, the pairs law, the parent’s connectedness and one-fewer-circle count — is the decoder-guard and pseudocircle-axiom surface the census re-verifies per key, or is P-1-derivable. Only these two are open.
Proved. The forward core child_walk_reduction is unconditional glue of M-C and M-E on the standard axioms: every spherical single-cluster child is the walk-assembly over its connected parent. The induction is correctly assembled — complete_step and connected_completeness hold as stated, over 060’s real SphereType, with the order diamond collapsed at defeq, swept into the Tests base, full build green, firewalled cold-review CONFIRMED on standard axioms only.
Not proved. The theorem is conditional. Discharge nothing and it says: given the enumeration/keyer Seam, given per-child hparConn, and given the finite base, the descent runs to every level. Both seams are real, external, and open — the DFS-emits-and-keys promise and the non-cut-deletion-stays-connected bridge. This is the induction skeleton standing up under the census vocabulary and the trusted sweep, which is a genuine milestone; it is not a closure of leg-4. The two seams are where the remaining work lives.