A decoder that rejects nothing is not doing its job, but a decoder that never lies is a different and much stronger claim. mapkey.map_from_key runs a battery of cheap, mechanical checks against the raw bytes of a candidate key — degree-4 vertices, exactly two circles crossing at each one, a containment table that doesn’t obviously contradict itself — and if the bytes pass, it hands back a decoded arrangement. Sd asks the question those checks were never designed to answer by themselves: when a key passes every one of them, is the object handed back a genuine disconnected pseudocircle sphere-type, or could the checks have been satisfied by a phantom — a combinatorial description that clears every test on paper and corresponds to no real geometry at all?
the Ledger, the round immediately before this one, answered a different question. It counted: conditional on six named facts, the emitted key set and the true type set come out the same size. Counting is worthless if some of what got counted was never real to begin with — soundness is completeness’s silent partner, and this round is where the disconnected-keyer campaign finally writes down, in the kernel, what passing the decoder’s checks actually buys.
Recall the vocabulary. Most of this project’s arrangements are one connected tangle of crossing circles. A composite is what is left over: several such tangles — clusters, each connected, some possibly a single circle with no crossings at all (a bare cluster) — sitting together on one sphere, some nested inside a face of another. The nesting forest records which cluster sits inside which face of which other: a parent pointer per cluster, the clusters nested inside nothing called roots. The table is laminar when that containment relation has no cycles — no cluster, directly or through a chain of others, ends up inside itself.
lensBare control — cluster 1, a bare circle C, sits truly inside one bounded face of cluster 0, the lens A,B. The parent pointer runs one way, up to a root, and the gate’s reachability sweep finds it. Right: cyc2, D-B’s mutual-containment control — two real lens clusters, each individually a genuine 2-circle crossing, drawn apart because there is nowhere to draw them together. locFace claims cluster 0 sits inside a bounded face of cluster 1 and cluster 1 sits inside a bounded face of cluster 0. No sphere has a face of A that contains a face of B which contains a face of A again; the claim is not a nesting, it is a cycle. All four circle-pairs were checked numerically before this was drawn: each cluster’s own two circles cross with a positive margin, and the two clusters never touch (smallest cross-cluster gap 18 units against a radius of 27).Strip the Lean down to English. A DecoderCheckedComposite bundles exactly what survives the decoder’s mechanical checks on one candidate: the composite is well-formed (D-A — every crossing cluster is internally connected, the bare-circle sentinels are consistent), it passes the laminarity gate (D-B — the NonLaminarError check does not fire), it is forest-faithful (D-G’s fence, taken up below), and every crossing cluster individually passes the decoder’s own check list, has Euler characteristic , and is circle-faithful with a surjective label map. A PseudocircleComposite is the honest conclusion: a genuine combinatorial disconnected pseudocircle skeleton. Every crossing cluster really does have proper degree-4 crossings of two distinct circles, and every one of its circles really does cut its own sphere in two — separates it into a genuine inside and outside, the property named IsCut. And, independently, the nesting really is a well-formed laminar forest whose containment relation coincides exactly with ancestry in that forest: no cluster’s stated position and its actual forest position can disagree.
That is Sd1, and every step of its proof is reuse, not new geometry. The per-cluster half — proper crossings, and every circle a cut — comes from two already-promoted lemmas doing exactly what they did for the connected census: properCrossings_of_decoderChecks (L-A) turns the decoder’s check list into ProperCrossings, and isCut_of_spherical turns ProperCrossings plus connectivity plus into IsCut — the same derivation the connected campaign’s S1 used, run once per cluster instead of once for the whole map. The inter-cluster half — the laminar forest and its ancestry correspondence — is D-B’s reachability equivalence and D-G’s ForestFaithful fence, carried straight through. Nothing here is new mathematics; the file’s own docstring calls it correctly: assembly of promoted machinery.
cyc2 is a two-cluster composite, both clusters the promoted packedLens (a real 2-circle crossing), with the containment table set to locFace[0][1] = face 2 and locFace[1][0] = face 2. Read literally: cluster 0 sits in a bounded face of cluster 1, and cluster 1 sits in a bounded face of cluster 0. That is not a description of anything a sphere can hold. Containment among disjoint territories is a strict order — if 0’s territory sits inside a piece of 1’s, then 1’s territory is strictly bigger, and nothing bigger fits inside something strictly smaller. cyc2 is exactly the two-cluster case of the round brief’s “X inside Y, Y inside X” — the smallest possible phantom.
def cyc2 : CompositeMap where
numClusters := 2
node := ![.cluster packedLens 0, .cluster packedLens 0]
locFace := ![![.face 0, .face 2], ![.face 2, .face 0]]Decoded: two lens clusters, each claiming to sit in a bounded face (face 2, not the outer face face 0) of the other. Both clusters individually pass every per-cluster check — they are the same promoted packedLens the positive control uses — so nothing about either cluster’s own geometry is at fault. The fault is entirely in what the table claims about how they sit together.
D-B’s gate catches this specific claim: the parent scan finds parent(0) = some 1 and parent(1) = some 0, a two-step loop with no root, so the reachability sweep the gate runs (reachCount) finds zero of the two clusters reachable and rejects the table. That much is the gate doing its job. But cyc2 earns its place in this file for a sharper reason: it is well-formed (D-A’s connectivity and sentinel checks pass), it is ForestFaithful — vacuously, because a two-cycle makes every cluster its own ancestor and D-G’s fence has nothing left to check — and both clusters individually pass DecoderChecks and . Every hypothesis of Sd1 except laminarity holds on cyc2, and laminarity still fails. So the four other conditions cannot be made to imply it; if the theorem tried to derive Laminar from well-formedness, forest-faithfulness, and the per-cluster checks alone, cyc2 would refute it in the kernel.
theorem sd_without_laminarity_is_false :
¬ (∀ (C : CompositeMap), C.WellFormed → C.ForestFaithful →
(∀ (X : Fin C.numClusters) (P : PackedMap) (of : ℕ),
C.node X = .cluster P of → P.map.DecoderChecks) →
(∀ (X : Fin C.numClusters) (P : PackedMap) (of : ℕ),
C.node X = .cluster P of → P.map.eulerChar = 2) →
C.Laminar) :=
fun h => cyc2_not_laminar
(h cyc2 cyc2_wellFormed cyc2_forestFaithful cyc2_checks cyc2_euler)Decoded: cyc2 is handed to the universally-quantified statement as the witness. It satisfies every named hypothesis (cyc2_wellFormed, cyc2_forestFaithful, cyc2_checks, cyc2_euler, all separately proved), so the statement would force cyc2.Laminar — and cyc2_not_laminar is sitting there, kernel-proved, to contradict it.
So pseudocircleComposite_of_decoderChecked does not try to be clever about laminarity: DecoderCheckedComposite carries C.Laminar as its own field, taken directly from whatever the real decoder’s gate decided, never reconstructed from the rest. The same discipline covers ForestFaithful, for a reason that runs the other direction: D-B’s own forward-flag showed the gate decides parent-graph acyclicity, which is strictly weaker than true acyclicity of the containment relation on adversarial tables — insideCyclicPass, the Boomerang’s Liar’s Key, is a four-cluster table that is genuinely containment-cyclic yet still passes the gate. ForestFaithful and Laminar turn out to be independent of each other in both directions: insideCyclicPass passes the gate but fails the fence, and cyc2 fails the gate but passes the fence vacuously. Neither hypothesis can be dropped in favor of the other, and Sd1 takes both, honestly, exactly where D-G left them.
PseudocircleComposite is a genuine step forward — every crossing cluster has proper crossings and cuts, and the nesting is a well-formed laminar forest — but it is still a statement about combinatorics: vertices, arcs, a parent table. It says nothing yet about whether that combinatorial description is actually realized by circles drawn on an actual sphere, uniquely up to homeomorphism and reflection. That correspondence is L2’s Theorem A, the disk lemma (FaceClosuresAreDisks) both earlier attempts at L2 missed, and it is exactly the kind of fact Mathlib has no vocabulary for: no surfaces, no embeddings, no genus. The same wall isCut_of_spherical ran into and got around by consuming only the number in place of the topology — not this time. There is no numeric proxy for “this combinatorial forest is a genuine nested arrangement of disks on a sphere.”
So it is threaded as a hypothesis, named h_disk, and never discharged:
Read that literally: it is close to a tautology — and ( implies the type membership) together give the type membership, which is modus ponens with extra steps. That triviality is the honest point. All of the theorem’s force is in what counts as evidence for each conjunct: is pseudocircleComposite_of_decoderChecked, proved in the kernel from Sd1. is supplied from outside, never proved, at every call site. The “∈ T_d” half of the statement of record is entirely — Sd1 contributes nothing to it beyond being the thing is a hypothesis about.
One more thing has to be true before any of the above ever fires on real data: that a specific line of bytes in candidates6_disconnected.keys really does decode to a DecoderCheckedComposite in the first place — the decode succeeds, re-keying the result returns the identical bytes (canonicity), the result is genuinely multi-cluster, and it is built on six circles. That is Sd3, checked outside Lean by build_candidates6_disconnected.verify_object over all 16,597 disconnected keys. It supplies the hypothesis Sd1 consumes; nothing about it is provable in the trusted base at this scale — there is no native_decide here, so 16,597 individual per-key facts stay a Python gate, exactly as the connected campaign’s S3 and D-H’s Gd3 did before it.
DecoderCheckedComposite per key. Sd1 (solid arrow) is the kernel-checked step: pure assembly, no topology. Sd2 (dashed arrow) is h_disk — named, never proved, the entire load of the conclusion’s type-membership half.the Ledger’s statement of record takes hmem — every decoded key names a genuine member of — as one of six typed hypotheses, entered on faith. Sd is the round that makes that entry honest, per key:
theorem typeOf_mem_of_sd {PC : PackedComposite} (hdc : DecoderCheckedComposite PC.C)
{Td : Finset CompositeSphereType}
(h_disk : PseudocircleComposite PC.C → PC.typeOf ∈ Td) :
PC.typeOf ∈ Td :=
h_disk (pseudocircleComposite_of_decoderChecked hdc)Decoded: given a decoder-checked composite and the topological fence for its own type, Sd1 fires and h_disk closes the goal. This is a forward implication into D-H’s seam, never the other direction — it does not invoke composite_census_complete. Sd uses D-H’s definitions (the composite sphere-type, the packed-composite bundle) but never D-H’s theorem, so the dependency runs one way: Sd hands D-H a reason to trust hmem, not the other way around — no circularity.
Worth being precise about what “discharges the seam” means here, because it is easy to overread. typeOf_mem_of_sd does not remove h_disk from the picture — it still has to be supplied, per key, exactly as before. What changes is that the OTHER half of hmem, the combinatorial genuineness that used to be asserted wholesale, is now a kernel-checked consequence of decoder-checking rather than a second unexamined assumption riding alongside the topological one. hmem used to be one opaque fact; it is now one honest, un-formalizable fact (h_disk) plus one proved fact (Sd1). That is real progress, and it is exactly the progress this round claims — no more, no less.
The conclusion predicate, in full — the combinatorial skeleton Sd1 hands back:
structure PseudocircleComposite (C : CompositeMap) : Prop where
proper : ∀ (X : Fin C.numClusters) (P : PackedMap) (of : ℕ),
C.node X = .cluster P of → P.map.ProperCrossings
cut : ∀ (X : Fin C.numClusters) (P : PackedMap) (of : ℕ),
C.node X = .cluster P of → ∀ i : P.Circle, P.map.toArrMap.IsCut i
sentinels : C.SentinelsConsistent
laminar : C.Laminar
reaches : ∀ X, ReachesRoot C.parent X
forestFaithful : C.ForestFaithful
inside_ancestor : ∀ {X Y : Fin C.numClusters}, X ≠ Y → (C.Inside X Y ↔ C.Ancestor X Y)
faithful : ∀ (X : Fin C.numClusters) (P : PackedMap) (of : ℕ),
C.node X = .cluster P of → P.map.CircleFaithful ∧ Function.Surjective P.map.circDecoded: eight fields, none of them new vocabulary — ProperCrossings/IsCut from the L-A/isCut_of_spherical stack, Laminar/ReachesRoot from D-B, ForestFaithful/Inside↔Ancestor from D-G. The record never reads circ directly — the connected campaign’s honest K2 correction, carried here per cluster rather than once.
And Sd1 itself — the assembly, field by field:
theorem pseudocircleComposite_of_decoderChecked {C : CompositeMap}
(h : DecoderCheckedComposite C) : PseudocircleComposite C where
proper := fun X P of hX => properCrossings_of_decoderChecks P.map (h.checks X P of hX)
cut := by
intro X P of hX i
have hconn : P.map.DartConnected := by
have hc := h.wf.clusters_connected X
rw [hX] at hc; exact hc
intro f w
exact isCut_of_spherical P.map hconn
(properCrossings_of_decoderChecks P.map (h.checks X P of hX))
(h.euler X P of hX) i w
sentinels := h.wf.sentinels
laminar := h.lam
reaches := (C.laminar_iff_forall_reachesRoot).mp h.lam
forestFaithful := h.ff
inside_ancestor := fun {X Y} hne => C.inside_iff_ancestor h.ff hne
faithful := h.faithfulDecoded: every field is either handed straight through from the hypothesis bundle (sentinels, laminar, forestFaithful, faithful) or built by one promoted lemma call (proper, cut from L-A + isCut_of_spherical; reaches, inside_ancestor from D-B/D-G’s equivalences). No case split, no induction, no new construction — the shape of a pure assembly theorem.
The statement of record, threading h_disk at the exact seam where the meaning of enters:
theorem sd_statement_of_record {C : CompositeMap} (hdc : DecoderCheckedComposite C)
{Td : Finset CompositeSphereType}
(h_disk : PseudocircleComposite C → C.stypeOf ∈ Td) :
PseudocircleComposite C ∧ C.stypeOf ∈ Td :=
⟨pseudocircleComposite_of_decoderChecked hdc,
h_disk (pseudocircleComposite_of_decoderChecked hdc)⟩Decoded: the left conjunct is Sd1, unconditional. The right conjunct applies the SAME Sd1 result to the supplied h_disk. There is exactly one proof of PseudocircleComposite C in this theorem, used twice — not two independent derivations, which matters for honesty: nothing about the topological conjunct is proved separately from the combinatorial one, it is the combinatorial one, handed to an un-discharged hypothesis.
the Ledger and No Phantoms are the campaign’s two capstones, and they answer different questions about the same emitted key set. the Ledger asks whether the count is right — whether dedupe neither fuses two real types together nor drops one on the floor. No Phantoms asks whether the things being counted are real at all. A count that is exactly right over a set of hallucinations would still be worthless; a soundness guarantee over a set that misses half the true types would still be incomplete. The two rounds are logically independent — No Phantoms proves nothing about hkeyInj, the Ledger’s own still-open no-overcount debt, and closing that debt is not this round’s job — but together they are what makes the phrase “16,597 disconnected sphere-types” mean something more than “16,597 keys a program happened to print.”
It also closes the loop the Boomerang opened. D-G’s forward-flag named “the Sd decoder-soundness reading of decodeKeyToks” as a follow-on it was deliberately leaving for later. This is that follow-on, and it turned out to be exactly as cheap as the scoping document predicted — a short assembly round, not a new proof core — because every piece of machinery it needed (L-A, isCut_of_spherical, D-B’s reachability equivalence, D-G’s ForestFaithful fence) already existed, kernel-checked, from earlier rounds that were solving other problems. The cheapness is itself a data point: it means the connected campaign’s single-cluster substrate really was built general enough to answer a question about composites nobody was specifically asking when it was written.
Proved, kernel-checked on standard axioms only (5 #print axioms gates in Tests.lean plus the whole-environment sweep; firewalled adversarial cold review, 8505 jobs green, verdict STANDS — no errata, no caveats, no soundness bug found): pseudocircleComposite_of_decoderChecked (Sd1, the combinatorial skeleton, unconditional); sd_without_laminarity_is_false, the kill-check pinning laminarity as load-bearing and non-derivable; lensBare_pseudocircle, confirming Sd1 fires non-vacuously on a real decoder-checked composite; sd_statement_of_record and typeOf_mem_of_sd, threading h_disk honestly at the seam D-H consumes. The reviewer independently confirmed the new per-cluster Fintype instances (needed for eulerChar and IsCut to even typecheck per cluster) are canonical — the same @Quotient.fintype construction the connected campaign’s lens/torus controls use by hand, here derived once for every packed cluster — and cross-checked their cardinalities against packedLens_eulerChar := by decide.
Not proved — named, not hidden. (Sd2): the topological correspondence between a laminar combinatorial skeleton and a genuine embedded sphere arrangement, L2’s Theorem A, blocked by the same absence of surfaces and embeddings in Mathlib that fenced the connected campaign’s S2. It is never proved anywhere in this repository; it is supplied at every call site, and the entire type-membership half of the statement of record rests on it. Sd3: the per-datum decode/re-key/shape check over the 16,597 disconnected keys, a Python gate outside the trusted base. Gd1/Gd2: that a census key’s bytes are a given CompositeMap, and that CPython computes the modeled decoder checks — gateable only, as everywhere in this campaign.
None of this makes the round smaller than it is. What Sd proves is precisely the combinatorial half of soundness, no more: given that a key really did pass the decoder’s checks (Sd3’s job) and given that the resulting skeleton really is a genuine sphere arrangement (Sd2’s honest, un-formalizable fence), the skeleton itself is exactly what the checks promised — proper crossings, genuine cuts, a laminar nesting that means what it says. cyc2 is the reminder of why that combinatorial half was worth stating carefully rather than waved through: a table can satisfy every check this project can run outside topology and still describe nothing that exists. Sd1 is the guarantee that once laminarity and forest-faithfulness are honestly checked — not assumed, not derived from cheaper facts that don’t entail them — nothing else in the combinatorics can smuggle a phantom past it.