Throw a boomerang and it comes back — not a similar-looking stick, the same one: same shape, same weight, same curve. That is the whole content of K2d, the separation direction of the disconnected keyer. Hand an arrangement to the keyer and it hands back a fingerprint — a composite sphere key, the same string that D-F’s essay (“the Matryoshka”) explained how to build. Decode that fingerprint, and what comes back has to be the same nesting shape you started with, or its mirror image — not merely something that happens to hash the same, but the actual doll-within-doll structure, dolls possibly relabeled and the whole thing possibly flipped in a mirror, but the same dolls nested the same way. That is the throw-and-return this essay is named for.
D-F proved the safe half of this promise: two arrangements that really do nest alike can never drift apart under the fingerprinting sweep — sameness survives being taken apart and reassembled. This round proves the converse, and the converse is the harder direction for a reason that turns out to be interesting rather than merely laborious: the natural way to state it is false, and finding the honest qualifier that rescues it is this round’s actual result.
Recall from the Matryoshka: a nesting-respecting composite isomorphism — a bijection between two composites’ clusters that matches each cluster to an isomorphic one, carries containment, and carries the actual parent forest, not just raw containment. Obligation Kd’s separation direction, stated the way the scoping document first wrote it down, reads:
Read at face value — over the raw composite objects the model quantifies over, with no further qualifier — that sentence is false, and this round exhibits the counterexample rather than merely failing to prove it. The honest theorem carries an extra condition, attainment: each side’s sphere key has to be the one that comes from serializing it at its own default rooting (the ordinary horizon, no re-rooting sweep applied) — on the B side, in either orientation. Under that qualifier, the implication holds:
Take a lone bare circle sitting inside one face of a lens (two circles crossing at two points) — call this arrangement lensBare. Now consider the same physical sphere read the other way: the lens sitting inside the bare circle’s territory instead of the reverse — lensInBare. These aren’t two different spheres. They’re two different descriptions of one sphere, differing only in which face got declared the horizon — exactly the re-rooting gauge freedom D-F’s rooting sweep exists to absorb. Because the sphere key minimizes over every legal horizon, it correctly assigns lensBare and lensInBare the same key — the sweep is doing exactly its job, merging two views of one object.
But , the Matryoshka’s isomorphism, is a strictly default-gauge relation: it asks whether the two particular presentations handed to it nest the same way, not whether some re-rooting of them would. And at the default gauge, lensBare and lensInBare genuinely don’t nest the same way. A bare circle can’t contain itself, so whichever cluster is bare is forced into the “contained” index slot — and that forcing flips which cluster is labeled 0 and which is labeled 1 between the two presentations. lensBare has its cluster 1 inside cluster 0; lensInBare, after the forced index flip, has cluster 0 inside cluster 1. No bijection carries one containment relation onto the other’s: the round’s kernel-checked witness, lensBare_lensInBare_no_iso, proves exactly this by chasing the index flip through CompositeIso’s inside_iff field and finding it demands a fact that is decide-false.
lensBare (left): a lone bare circle C sits inside a face of the lens A,B — cluster 1 (the bare, contained cluster) inside cluster 0 (the lens). lensInBare (right): the identical sphere, re-rooted so the bare circle’s territory is drawn as the containing one — the forced index convention now makes it cluster 0, with the lens as cluster 1. Same sphere key by the rooting sweep; no bijection carries Inside(1,0) to Inside(0,1) directly, which is exactly why the separation direction needs the attainment qualifier.So the un-qualified separation sentence fails precisely on the re-rootings the whole rooting sweep exists to identify — not on some pathological edge case unrelated to the theorem’s own machinery, but on the exact phenomenon that machinery was built to handle. Pinning down the honest qualifier is the result. Attainment-at-default is not an arbitrary patch; it is exactly the property real census representatives already have: map_from_key’s verify step re-encodes a decoded key at the plain default rooting and demands the identical bytes back — Gd3’s per-key “canonical fixed point,” the same property every one of the 16,597 disconnected census keys is checked against. The hypothesis is non-vacuous by measurement, not merely by construction: the cold review confirmed 200 of 200 sampled real census keys satisfy attainment-at-default. The theorem asks of its inputs nothing the actual data doesn’t already provide.
A second honesty fence, flagged by the previous round and honored by this one. D-B proved that the NonLaminarError gate — the check that rejects a malformed nesting table before it’s ever serialized — decides parent-graph acyclicity, which is strictly weaker than acyclicity of the actual containment relation: a table can be genuinely cyclic in who-contains-whom and still pass the gate, because the gate only ever looks at the parent forest the scan happens to build, not at the containment relation the table was supposed to encode. A hostile key can therefore pass the laminarity gate while lying about containment.
Decode soundness must not assume “gate passed &implies; containment acyclic.” This round carries the honest fix as a named hypothesis, ForestFaithful: the table must be the one _build_locface would rebuild from its own parent forest — every non-ancestor cell reads the host’s outer selector, every ancestor cell inherits along the path. It is proved independent of the gate in both directions: D-B’s gate-passing, containment-cyclic table fails this fence outright, while a gate-rejected table can still satisfy it vacuously. Neither hypothesis subsumes the other, and the round-trip needs both — the fence is not a restatement of the gate wearing a new name, it is a genuinely separate fact the round proves has to be assumed.
One seam left open since round P4: the forest serializer runs on a fuel counter, and P4 never showed the fuel is always enough — only that if it is, the serialization is correct. This round closes it. The encoder is factored through an explicit parse tree (serAux_eq_print_toATree): the same recursion, restructured to keep its shape instead of collapsing straight to tokens. The pigeonhole that proves the fuel never runs out is the ancestor set — every child’s set of strict ancestors is exactly its parent’s plus the parent itself, one bigger every step down, and no cluster is its own ancestor on an acyclic table, so the ancestor-set size is bounded below the total cluster count. That inequality is exactly the fuel budget the recursion needs, and it survives every step of the descent by construction.
This is the Lean, unmodified. First the hypothesis package the separation core demands of one side (A250001/CompositeRoundTrip.lean):
structure DecodeReady (C : CompositeMap) (ce : Fin C.numClusters → ClusterEnc)
(bord : LinearOrder (List ℕ)) : Prop where
/-- D-A's well-formedness: per-cluster connectivity and sentinel consistency. -/
wf : C.WellFormed
/-- D-B's gate: the parent forest is acyclic. -/
lam : C.Laminar
/-- Part 1's fence: the table is its own forest rebuild. -/
ff : C.ForestFaithful
/-- The `ce` encs have the parseable shapes `_ceFromCore` emits. -/
shaped : EncShaped C ce
/-- Each crossing node's enc is its canonical body plus a mark (the Gd2 residue). -/
canonical : ∀ (X : Fin C.numClusters) (P : PackedMap) (of : ℕ), C.node X = .cluster P of →
∃ mark, (ce X).enc = (P.bodyRecord bord ++ [mark]).map .sym
/-- Per-cluster circle faithfulness and label surjectivity — the record never reads `circ`. -/
faithful : ∀ (X : Fin C.numClusters) (P : PackedMap) (of : ℕ), C.node X = .cluster P of →
P.map.CircleFaithful ∧ Function.Surjective P.map.circDecoded: wf/lam are D-A/D-B’s standing requirements; ff is the Liar’s Key fence above; shaped/canonical pin the census ce table to the shape the parser can actually re-read; faithful is the per-cluster honest correction the connected campaign already learned to demand — the record never reads which circle is which, so nothing downstream can conclude the decoded circles are faithful without being told so, per cluster.
The Liar’s Key fence itself, from part 1 (A250001/CompositeDecode.lean):
structure ForestFaithful : Prop where
/-- A non-ancestor host holds the guest in its outer face (`src/mapkey.py:707-710`). -/
outer_of_not_ancestor : ∀ X Y, X ≠ Y → ¬ C.Ancestor X Y → C.locFace X Y = C.outerSel Y
/-- An ancestor host holds the guest where it holds the path child (`:711-716`). -/
inherit : ∀ X Z Y, Z ∈ X :: chase C.parent C.numClusters X → C.parent Z = some Y →
X ≠ Y → C.locFace X Y = C.locFace Z YThe separation core — the Boomerang’s landing, at the default gauge:
theorem compositeIso_of_orientedKeyToks_eq {A B : CompositeMap}
{ceA : Fin A.numClusters → ClusterEnc} {ceB : Fin B.numClusters → ClusterEnc}
{sord : LinearOrder (List SerTok)} {bord : LinearOrder (List ℕ)} {nnA nnB : ℕ}
(hA : DecodeReady A ceA bord) (hB : DecodeReady B ceB bord)
(h : A.orientedKeyToks ceA sord nnA = B.orientedKeyToks ceB sord nnB) :
Nonempty (CompositeIso A B) := by
-- proof elided here (∼70 lines) — kernel-checked, standard axioms only.
-- one token list parses to both sides' erased forests (the parse layer's inversion
-- lemma turns the byte equality into a parse-tree equality); the spine induction pairs
-- the two traversal plans position by position; plan completeness + duplicate-freedom
-- make the pairing a cluster bijection σ; every ≅ₙ field then falls out —
-- per-node DartIsos from equal records by the promoted per-cluster K2, parent_comm from
-- the position pairing, inside_iff/locFace_bare through the ForestFaithful fence.Decoded: this is the theorem that actually recovers a shape from a fingerprint — equal token lists in, a genuine isomorphism witness out, with no re-rooting or mirror sweep involved yet. Everything below builds on this core.
The hypothesis-free sweep fact — the sphere key really is one of the swept rooted keys, no attainment assumed:
theorem sphereKeyToks_attained (C : CompositeMap) (fm : Fin C.numClusters → ℕ → ℕ)
(rf : Fin C.numClusters → List ℕ)
(ce ceM : Rooting C.numClusters → Fin C.numClusters → ClusterEnc)
(sord : LinearOrder (List SerTok)) (nn : ℕ) :
∃ r ∈ C.rootingsOf rf,
C.sphereKeyToks fm rf ce ceM sord nn = C.rootedKeyToks (ce r) sord nn r ∨
C.sphereKeyToks fm rf ce ceM sord nn =
(C.mirrorC fm).rootedKeyToks (ceM r) sord nn (mirrorRooting fm r) := by
-- proof elided here (∼25 lines) — kernel-checked, standard axioms only.
-- the swept minimum is a member of the list it minimizes; unwind keyMin to the
-- underlying min_choice to read off which of the two orientations actually won.And K2d’s statement of record, attainment-qualified:
theorem compositeIso_or_mirror_of_sphereKeyToks_eq {A B : CompositeMap}
{fmA : Fin A.numClusters → ℕ → ℕ} {rfA : Fin A.numClusters → List ℕ}
{ceA ceAM : Rooting A.numClusters → Fin A.numClusters → ClusterEnc}
{fmB : Fin B.numClusters → ℕ → ℕ} {rfB : Fin B.numClusters → List ℕ}
{ceB ceBM : Rooting B.numClusters → Fin B.numClusters → ClusterEnc}
{sord : LinearOrder (List SerTok)} {bord : LinearOrder (List ℕ)} {nnA nnB : ℕ}
(hA : DecodeReady A (ceA none) bord)
(hB : DecodeReady B (ceB none) bord)
(hBM : DecodeReady (B.mirrorC fmB) (ceBM none) bord)
(hattA : A.sphereKeyToks fmA rfA ceA ceAM sord nnA =
A.orientedKeyToks (ceA none) sord nnA)
(hattB : B.sphereKeyToks fmB rfB ceB ceBM sord nnB =
B.orientedKeyToks (ceB none) sord nnB ∨
B.sphereKeyToks fmB rfB ceB ceBM sord nnB =
(B.mirrorC fmB).orientedKeyToks (ceBM none) sord nnB)
(h : A.sphereKeyToks fmA rfA ceA ceAM sord nnA =
B.sphereKeyToks fmB rfB ceB ceBM sord nnB) :
Nonempty (CompositeIso A B) ∨ Nonempty (CompositeIso A (B.mirrorC fmB)) := by
rcases hattB with hatt | hatt
· exact Or.inl (compositeIso_of_orientedKeyToks_eq hA hB
(hattA.symm.trans (h.trans hatt)))
· exact Or.inr (compositeIso_of_orientedKeyToks_eq hA hBM
(hattA.symm.trans (h.trans hatt)))Decoded: hattA/hattB are the attainment hypotheses — each side’s sphere key must equal its own default-gauge key, B’s in either orientation. Note what hBM is and isn’t: it is a hypothesis, supplied to the theorem, not derived from hB. The proof itself is now genuinely short — the real labor already happened inside compositeIso_of_orientedKeyToks_eq; this wrapper just picks, per the attainment disjunction, which default-gauge equality to feed it, and in the mirror case produces a CompositeIso A (B.mirrorC fmB) — the mirror applied to the whole composite, D-F’s honest vocabulary, never a per-cluster mirror smuggled in piecemeal.
And the centerpiece counterexample, kernel-refuting the un-qualified sentence:
theorem lensBare_lensInBare_no_iso : ¬ Nonempty (CompositeIso lensBare lensInBare) := by
-- proof elided here (∼20 lines) — kernel-checked, standard axioms only.
-- the bare nodes must correspond under any candidate σ, forcing σ to be the
-- index flip (0 ↔ 1); inside_iff then demands lensInBare.Inside 0 1 match
-- lensBare.Inside 1 0 read through that flip — and `decide` shows it doesn't.D-F closed the invariance half of obligation Kd: same nesting shape (or its mirror) can never emit two different keys. This round closes the separation half, at the default gauge and under the attainment qualifier that real census representatives already satisfy: equal keys can never come from two genuinely different nesting shapes. Put the two together and the disconnected census’s dedupe-by-key is now faithful in both directions — it neither splits one true type into two keys (what D-F guards against) nor fuses two true types onto one key (what this round guards against), modulo the honest seams named below.
That symmetry matters more here than the connected campaign’s equivalent moment, because the disconnected stratum has no externally published count to check against — no A288568-analog. The 16,597-type count is generated, not corroborated, so both keyer directions carry real weight in the eventual completeness argument (D-H), where the connected campaign found its separation direction came almost free. Kd is not, however, finished. D-H — the disconnected statement of record, assembling K1d and K2d into one completeness theorem — remains open, and it is not bookkeeping: it must derive the mirror-side DecodeReady package by an actual mirror-transport of the whole package (this round only ever takes it as supplied), build the still-undefined ≅ₙ symm/trans, and replay this round’s separation argument at every re-rooted gauge the sphere-key sweep visits, not just the default one this round covers.
Proved, kernel-checked on standard axioms only (gated by 15 #print axioms checks in Tests.lean plus the trusted-base sweep; survived an adversarial cold review, STANDS-WITH-ERRATA): equal default-gauge composite keys force a nesting-respecting composite isomorphism (compositeIso_of_orientedKeyToks_eq); equal sphere keys force or , given each side is attained at its default rooting (compositeIso_or_mirror_of_sphereKeyToks_eq); the un-qualified sentence is false, exhibited rather than merely disbelieved (lensBare_lensInBare_no_iso); decode soundness needs the ForestFaithful fence independent of the laminarity gate, in both directions; and the fuel-sufficiency seam P4 deferred is discharged by the ancestor-set pigeonhole.
The cold review turned up four minor errata, none touching soundness, all worth naming rather than smoothing over: a docstring listed a field DecodeReady doesn’t carry (harmless, corrected); two negative-control docstrings named the wrong Python guard as the one that actually raises first (corrected to name the Lean guard that fires, given the Lean decode’s narrower checks); the sphere-key wrapper theorem has no theorem-driven positive control beyond the axiom gate and the default-gauge core’s own control (a coverage note, not a defect); and — worth stating plainly — the Lean decode is a decoder of canonical keys, not a rejector. It is strictly more permissive than Python’s map_from_key plus verify: it accepts out-of-range face tags and omits some per-cluster structural guards Python enforces. That is disclosed in the module docstring on purpose, not a gap discovered after the fact.
Open seams, named rather than glossed over:
symm/trans for CompositeIso do not exist. The mirror branch above works around this by taking the mirror-side DecodeReady package as a supplied hypothesis rather than deriving it from the plain side’s package. Building that derivation — transporting ForestFaithful, laminarity, and canonicity through the mirror map — is named, explicitly, as D-H’s job.ce-canonicity discharge D-F already flagged — stays deferred to D-H.DecoderChecks, circle faithfulness) is a separate, named follow-on obligation (Sd), not something this round’s decode function establishes about its own output._sphere_key_reference and encodeRooted/map_from_key compute the modeled functions is an implementation seam, gated only, never removed.None of this is a defect in the Boomerang. It is the honest shape of a theorem that found its own naive form false before anyone else could, and chose to prove the qualifier rather than hide the counterexample. With the Matryoshka and the Boomerang both landed, obligation Kd’s two directions are closed — modulo the seams above, all of them named, none of them silent. Kd itself, the full assembled disconnected count, is not. D-H remains.