Take a real arrangement of circles — an actual picture, drawn with an actual compass — and lift one circle away. What’s left is still a real arrangement of circles: nobody had to redraw anything, because a sub-picture of a real picture is automatically a real picture of the sub-picture. That sentence sounds almost too obvious to bother stating. It earns its keep the moment you run it backward: if what’s left can’t be a real picture of circles — if some five-circle piece is provably impossible to draw — then the six-circle whole it came from can’t be real either. A broken piece breaks everything built on top of it.
That’s the Curse. It’s the contrapositive of a projection fact so simple it is almost not worth calling a theorem — restriction of a realizable system is realizable — and yet, run in the refuting direction, it turns one impossible five-circle picture into a certificate against every six-circle candidate that contains it. This project’s n=6 census has 626,020 candidate circle arrangements sitting in a file, most never checked against real geometry at all. Each one has six circles, so it has exactly six ways to delete one and look at what’s left — six five-circle sub-arrangements per candidate. Three specific five-circle types are already known, kernel-certified, non-realizable. Delete each of the six circles from every one of the 626,020 candidates, key what remains, and ask: does any of those six deletions land on one of the three cursed types? If so, the candidate is non-realizable by inheritance, with no new solver run and no new certificate built for it — just a combinatorial embedding check against a basis someone already proved impossible.
Write for “ is a subsystem of ”: there’s a way to restrict any assignment that satisfies ’s constraints down to one that satisfies ’s. (Concretely, at n=6, is a candidate and is one of its six one-circle deletions — but the lemma below never mentions circles; it’s stated at the level of constraint systems, and the circle-deletion reading is a separate obligation, taken up below.) Realizability transfers down along : a feasible point for restricts to a feasible point for , so realizable realizable. The Curse is the contrapositive, and it is exactly that cheap:
The payoff is what happens when you fix and let range: the set of every with is ’s up-set, and one refutation of refutes the whole up-set at once. A single Farkas certificate, proved once, doesn’t just kill one candidate — it kills everything that contains that candidate as a piece, for as long as the containment holds. That’s the multiplication the sweep below is built to exploit.
This is the Lean, unmodified, from A250001/HereditaryClosure.lean. First the honest, minimal shape of “ is a subsystem of ” — no claim yet that this has anything to do with circles:
structure IsSubsystem (T' T : SphereType K) where
/-- restriction of an assignment for `T` to an assignment for `T'` -/
res : (Fin T.N → K) → (Fin T'.N → K)
/-- `res` carries `T`-feasible points to `T'`-feasible points -/
pull : ∀ x, Feasible T x → Feasible T' (res x)Then heredity — the Curse itself, its contrapositive form:
theorem not_Realizable_of_subsystem {T' T : SphereType K} (H : IsSubsystem T' T)
(h : ¬ Realizable T') : ¬ Realizable T :=
fun hT => h (Realizable_of_subsystem H hT)And the composition that does the actual refuting work — a pinned Positivstellensatz certificate for , lifted through the subsystem relation, closes off with no fresh certificate of its own:
theorem not_Realizable_of_refuted_subsystem [IsStrictOrderedRing K]
{T' T : SphereType K} (H : IsSubsystem T' T) (cert : PositivCert K T')
(hc : refutesType T' cert) : ¬ Realizable T :=
not_Realizable_of_subsystem H (positivstellensatz_sound T' cert hc)Decoded: give the lemma a subsystem witness H and a refuting certificate cert for the SMALLER type T', and it hands back non-realizability for the BIGGER type T — the whole three-step argument (projection, then heredity, then composing with the already-promoted Positivstellensatz soundness theorem) collapsed into one call. Two controls in the file make sure IsSubsystem is doing real work rather than being vacuously true: a positive control where a genuine realization really does restrict, and a negative control (neg_no_subsystem) where realizability provably does NOT transfer between a realizable base and an unrealizable target — showing no IsSubsystem relation can exist there, which is exactly what the pull hypothesis is for.
src/hereditary_sweep.py runs the check the hand-math promises, over both halves of the n=6 census: 609,423 connected candidates plus 16,597 disconnected ones, 626,020 total. For each candidate it deletes each of the six circles in turn — map_deletion.delete_circle, described in the module’s own docstring as “the COMBINATORIAL map surgery (arcs re-spliced, faces merged, clusters/nesting rebuilt), never a geometric operation” — keys the resulting five-circle sub-arrangement (mapkey.sphere_key), and tests membership in the refuted n=5 basis: three kernel-certified sphere types, at affine masses 5, 6, and 11, plus a fourth (mass 4, eight crossing pairs) tracked separately because it is non-realizable only by a mass-arithmetic elimination argument, not yet a certificate.
not_Realizable_of_subsystem) hands non-realizability straight back up to T — no new certificate built for T itself.The module cross-examines its own output twice before trusting it. First, a known-cases check: the disconnected half of the census already carries an independently-derived realizable/non-realizable mark on every one of its 16,597 types, built by a completely different instrument (L3, component realizability) that never calls map_deletion at all. The sweep’s own refuted set, restricted to that half, has to reproduce that mark exactly — and it does, symmetric difference zero. Second, a realized-never-flagged check: every key in the 297,425 realized-witness files is tested against the sweep’s refuted set, and a hit there would be a contradiction — proof that something in the chain is broken, not a statistic to report. Zero hits.
The result: 4,238 of the 626,020 candidates (4,216 connected + 22 disconnected) are refuted through the kernel-certified basis alone. A further 440 are refuted only by additionally invoking the open mass-4 leg, and the module keeps that count in a separate bucket rather than folding it in. With L(6) = 297,425 realized witnesses already on the books, the certified movement is:
Note what that arithmetic quietly refuses to do: the upper bound subtracts the 4,238, not the 4,678 that includes the conditional 440. The bracket is built entirely from the leg that has a certificate behind it.
One texture worth naming: the per-circle hit counts (the “canaries”) sum higher than the candidate counts — 1,091 hits route through the mass-5 type, 1,360 through mass-6, 2,160 through mass-11, 529 through the open mass-4 type, for 5,140 total hits against 4,678 distinct refuted candidates. That gap isn’t noise; some candidates are cursed more than once over, hitting the basis through two or more of their six deletions independently. A stronger sentence than the headline count implies, not a weaker one.
This is not “4,238 kernel-certified n=6 types,” and getting that wrong is the single easiest way to misquote this result. The honest chain has three links, weakest first:
delete_circle computes from the abstract map alone. That equivalence is measured — 684 + 5,715 deletion rows across every n≤4 and n=5 census witness, 0 mismatches between delete_circle’s output and independent geometric ground truth — but only up through n=5, because no n=6 geometric ground truth exists to check most candidates against; producing that ground truth is the whole reason the refutation leg exists in the first place. delete_circle is level-independent code, written once for every , not a fresh routine per level, so applying it at n=6 is extrapolating a primitive measured true everywhere it COULD be measured — not the same thing as fresh n=6 evidence, and the module’s own docstring insists on flagging it precisely that way.sorry, standard axioms only, gated by this project’s own trusted-base sweep.The Lean/Python split is the crux, and it deserves to be read as the actual mathematical content of this result rather than a disclaimer bolted onto it. Lean proves a subsystem inherits non-realizability — that’s not_Realizable_of_subsystem, kernel-checked, unconditional given an IsSubsystem witness. The separate claim — circle deletion actually produces a subsystem, the “sub-map embedding certificate” that lets a candidate’s six-circle constraint system and its five-circle deletion stand in the IsSubsystem relation at all — is discharged entirely outside Lean, by the Python checker. Nothing in HereditaryClosure.lean proves deletion implies subsystem; IsSubsystem is a NAMED HYPOTHESIS in every theorem that uses it, never a conclusion the file derives from delete_circle. So a census-type refutation that runs through this route is kernel(conditional) + Python(hypothesis) — never a pure kernel fact, and every one of the 4,238 numbers above inherits that shape.
The 440 additional candidates carry one more conditional layer on top: they refute only via the mass-4, eight-crossing-pairs n=5 type, whose non-realizability currently rests on a mass-arithmetic elimination argument (the unique 4-subset of a published mass multiset matching Felsner–Scheucher’s non-realizable count), not a certificate — todo/refuter/010 is still open. The sweep tracks this bucket separately by design and never merges it into the 4,238 silently.
The 323,917 candidates that are neither realized nor refuted — the residue — are dominated by types the realization sampler simply hasn’t reached yet (280,878 of 609,423 connected candidates have been sampled), not by types that were checked and came back inconclusive. Reading that number as an estimate of how many candidates will eventually turn out non-realizable would be a category error; it measures unexplored territory, not a refutation target.
And the sweep itself is a REVIEWABLE artifact, not an object of record: it writes only under scratch/relay/hereditary/, never touches a tracked census file, and its refuted key list is meant to regenerate from the census plus the basis on demand rather than being trusted as stored ground truth. It earned that grade honestly — the two validation checks folded into its own run, plus an adversarial cold review that re-derived the basis independently and hand-verified all 4,678 emitted entries, zero spurious — but “reviewable and validated” is still a rung below “kernel-checked,” and the label says so on purpose.
This is the first time anything has been certified off the TOP of a(6)’s bracket. Every prior number in this project’s Status line moved the lower bound — another realized witness, another certified circle picture. The upper bound, until round 050, was just the raw candidate count, 626,020, an artifact of how many combinatorial types exist at all rather than a statement about how many could possibly be real. 4,238 out of 626,020 is small in absolute terms — a bit over half a percent — but the economics behind it are the interesting part: one kernel-checked lemma, cheap to state, multiplies one refuting certificate across its entire up-set, for free, forever. Every future minimal non-realizable type this project's refuter finds at n=6 gets to fire this same projection argument against everything built on top of it, at no marginal Lean cost. That’s a fundamentally different scaling story than the realization leg’s witness-by-witness accumulation.
It’s also where this project’s discipline about human-readable certificates lives most visibly. A Farkas dual or an SOS witness is something a person can read line by line and check by hand, in a way an exact-rational coordinate witness generally isn’t. The refutation leg is smaller so far — 4,238 against 297,425 — but it’s the leg where “trust the label, not the location” gets exercised the hardest, because every number in it arrives wearing an explicit, named seam rather than a clean claim. That honesty is not a caveat attached to the result. Stating the seam precisely — kernel-checked heredity, audited-emission basis, extrapolated containment, Python-discharged hypothesis — is the result, as much as the count 4,238 is.
What’s left, named rather than glossed: the 323,917-candidate residue needs rung-1-and-later certificates — new minimal n=6 obstructions, found and kernel-checked the way final_poly found the n=5 basis — then re-propagation through this same Curse; and the canary hit-set (the tripwire types this round already computed) still needs wiring into the census pipeline as must-never-realize sentinels, a separate round. There is also a horizon on the whole approach worth stating rather than hiding: Felsner–Scheucher’s Corollary 12 gives infinite families of minimal non-circularizable arrangements, so hereditary refutation from a finite basis weakens as grows. Fine for now — the project’s horizon is n=6 and n=7, not asymptotics.