If two disconnected circle arrangements nest like the same set of dolls — same clusters, same “who sits inside whose face” — their canonical fingerprints come out byte-for-byte identical, no matter which face you declare the horizon.
Most of this project’s arrangements are one connected tangle of circles. Some aren’t: a few separate clusters — connected tangles, or lone bare circles with no crossings at all — sitting on the sphere, some tucked inside a face of another. A composite sphere key is the fingerprint of such a scene: a string built by walking the nesting and recording, recursively, which cluster sits inside which face of which other cluster.
The trouble is that a sphere has no fixed “outside.” Pick any face of any cluster and declare it the horizon — the point at infinity — and the very same scene reads differently. Take the simplest possible case: two disjoint bare circles, nothing crossing, nothing touching. Read from the ordinary horizon, the fingerprint is a flat side-by-side 2|[O][O]. But nothing stops you from declaring the INSIDE of one of the two circles to be the horizon instead — and once you do, the other circle’s outside face reads as “inside” the first one, the forest genuinely nests, and the fingerprint becomes 2|[O@1{[O]}], which sorts smaller. Both are the same sphere — you just relocated infinity. The real keyer doesn’t get to pick one horizon and hope: it tries all of them — every cluster, every one of that cluster’s own faces (plus the option of rooting inside a bare circle) — crossed with both the arrangement and its mirror image, and keeps whichever fingerprint sorts first. That whole exhausting sweep, kernel-checked line by line on exactly this example, is what D-F is a promise about.
2|[O][O]; declaring a point inside one circle the horizon instead makes the other circle’s outside face read as nested inside the first, giving 2|[O@1{[O]}]. K1d says the rooting sweep collapses both readings to the identical minimum — one physical sphere, one key, however you relocate infinity.K1d’s promise: however you scramble two arrangements that really do nest the same way — relabel which cluster comes first, spin any one cluster’s own rotation, or flip the entire scene in the mirror — the sweep converges on the identical fingerprint. That’s the name: sameness of nesting survives the fingerprinting sweep, the way a matryoshka doll survives being taken apart and put back together in a different order.
Write (“A nests like B”) for a nesting-respecting composite isomorphism: a bijection between A’s clusters and B’s such that
Write for B’s diagonal mirror — every cluster’s rotation reversed at once, with every nesting cell re-read through the matching face relabeling, applied to the whole composite in one stroke. (Mirroring the clusters one at a time and reassembling gives the wrong scene — this project’s standing name for that bug is the “oriented pool” problem.) K1d:
Every field above except the forest one is exactly what you’d expect from “the shapes match.” The forest field earns its keep: on an adversarial table, two hosts can sit at equal depth inside the same containing cluster, and which one the scan calls “the parent” depends on a first-index tie-break that a relabeling has no reason to respect — there is a kernel-checked counterexample where every other field lines up and the tie-break alone breaks the correspondence. On genuine geometric arrangements this never happens (any two real hosts of one circle differ in depth, because their territories chain rather than tie), so the field costs nothing where is meant to live — but it has to be stated as its own honest requirement, not derived for free, because “meant to live” doesn’t cover every table the definition could be fed.
The sphere key is literally the smallest fingerprint over the whole sweep: every legal horizon, both orientations. Each single horizon already compares both orientations and keeps the smaller one, and that comparison doesn’t care which side you call “the original” and which “the mirror” — swapping the labels can’t change which one wins. That symmetry is what lets the mirror branch avoid ever constructing a doubly-mirrored composite: if A nests like B’s mirror, then at every horizon A’s plain fingerprint matches B’s mirror fingerprint and vice versa, and the pairwise-minimum simply doesn’t notice the swap. The genuinely new labor was making the “same subtree under this relabeling” argument — already proved, the round before, for the one default horizon — work at every horizon in the sweep, by turning “the outer face” from a hardwired constant into an explicit parameter threaded through the whole recursive fingerprint-builder.
This is the Lean, unmodified. first — the definition every downstream statement quantifies over (A250001/ForestSerInvariance.lean):
structure CompositeIso (A B : CompositeMap) where
/-- The cluster bijection σ. -/
clusterEquiv : Fin A.numClusters ≃ Fin B.numClusters
/-- The per-node witnesses: `DartIso` on crossing clusters, bareness forced to correspond. -/
nodeIso : ∀ i, ClusterNode.NodeIso (A.node i) (B.node (clusterEquiv i))
/-- Bare-host cells carried on the nose: a bare host's column is sentinel-valued and sentinels
have no relabelling gauge. Redundant given `inside_iff` on sentinel-consistent composites
(`locFace_bare_of_inside_iff`); a field so ≅ₙ is meaningful on raw composites. -/
locFace_bare : ∀ X Y, X ≠ Y → (A.node Y).isBare = true →
B.locFace (clusterEquiv X) (clusterEquiv Y) = A.locFace X Y
/-- The containment relation carried (off-diagonal; the diagonal is dead by D-A's convention). -/
inside_iff : ∀ X Y, X ≠ Y → (A.Inside X Y ↔ B.Inside (clusterEquiv X) (clusterEquiv Y))
/-- The nesting forest carried. See the module docstring for why this is a field and when it
is instead derivable (`parent_map_of_inside_iff`). -/
parent_comm : ∀ X, B.parent (clusterEquiv X) = (A.parent X).map clusterEquivAnd the headline, sphereKeyToks_k1d (A250001/CompositeSphereKey.lean):
theorem sphereKeyToks_k1d {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)) (nCircles : ℕ)
(h :
(∃ (E : CompositeIso A B) (EM : CompositeIso (A.mirrorC fmA) (B.mirrorC fmB))
(rmap : Rooting A.numClusters → Rooting B.numClusters),
(B.rootingsOf rfB ~ (A.rootingsOf rfA).map rmap) ∧
(∀ r ∈ A.rootingsOf rfA,
GaugeCorresponds E (A.parentR r) (B.parentR (rmap r)) (ceA r) (ceB (rmap r))) ∧
(∀ r ∈ A.rootingsOf rfA,
GaugeCorresponds EM ((A.mirrorC fmA).parentR (mirrorRooting fmA r))
((B.mirrorC fmB).parentR (mirrorRooting fmB (rmap r))) (ceAM r)
(ceBM (rmap r)))) ∨
(∃ (E : CompositeIso A (B.mirrorC fmB)) (EM : CompositeIso (A.mirrorC fmA) B)
(rmap : Rooting A.numClusters → Rooting B.numClusters),
(B.rootingsOf rfB ~ (A.rootingsOf rfA).map rmap) ∧
(∀ r ∈ A.rootingsOf rfA,
GaugeCorresponds E (A.parentR r)
((B.mirrorC fmB).parentR (mirrorRooting fmB (rmap r))) (ceA r)
(ceBM (rmap r))) ∧
(∀ r ∈ A.rootingsOf rfA,
GaugeCorresponds EM ((A.mirrorC fmA).parentR (mirrorRooting fmA r))
(B.parentR (rmap r)) (ceAM r) (ceB (rmap r))))) :
A.sphereKeyToks fmA rfA ceA ceAM sord nCircles =
B.sphereKeyToks fmB rfB ceB ceBM sord nCircles := by
-- proof elided here (31 lines) — kernel-checked, standard axioms only.
-- rcases into the two disjuncts, each closed by the branch theorem
-- (sphereKeyToks_compositeIso / sphereKeyToks_mirrorIso) plus keyMin_comm.Decoded: Or.inl is the straightforward case — an isomorphism E between A and B directly, plus a second one EM between their two diagonal mirrors. Or.inr is the honest “A nests like B’s mirror” case: E relates A directly to B’s already-mirrored self (B.mirrorC fmB), and EM relates A’s already-mirrored self to B directly — the mirror is applied to the whole composite before any isomorphism is asked to relate anything, never smuggled in cluster-by-cluster. Each branch also carries, for every rooting the sweep visits, a GaugeCorresponds witness (hg/hgM) — the “same subtree, same relabeling” fact from the paragraph above, replayed once per horizon — and a permutation rmap lining up which of A’s rootings corresponds to which of B’s.
Trust label (docs/trust-map.md): PROVED-about-model — K1d assembled; per-gauge ce-canonicity and mirror-transport are D-G/D-H. Kernel-checked on Lean’s standard axioms only (propext, Classical.choice, Quot.sound — no sorry, no native_decide), gated by this project’s own axiom sweep. An adversarial cold review — a separate reviewer with no access to the implementer’s own writeup — tried to break it and could not; the one erratum it turned up was a docstring overstatement in an earlier module (a prior round had called two composites “genuinely different sphere types” when the rooting sweep actually identifies them), fixed in the same changeset — not a defect in this theorem.
K1d is the invariance half of what this campaign calls obligation Kd — the disconnected census’s analog of the keyer-injectivity obligation the connected n=6 census already discharged in full. The disconnected stratum (16,597 candidate types, folded into the 626,020-candidate a(6) total alongside the 609,423 connected ones) isn’t walked circle-by-circle the way the connected stratum is; it’s built by composing smaller connected arrangements every legal way and then deduplicating by this composite sphere key. That dedupe step rests on two separate promises: it must never split one true type into two different keys (which would silently overcount), and it must never fuse two genuinely different types onto one key (which would silently undercount).
K1d, now in the kernel, delivers the first promise: no rooting choice, no relabeling, no mirror can make one true nesting-shape emit two different fingerprints. It says nothing about the second.
Proved: same nesting-shape (or mirror-of-same-nesting-shape) same key, over the entire rooting×orientation sweep, kernel-checked.
Not proved: the converse. Same key same nesting-shape is a separate theorem — this campaign calls it K2d, and its atlas name is the Boomerang (D-G: throw an arrangement at the key, and it should come back the same shape). It is next in the chain and, as of this essay, has not landed. Until it does, the disconnected census’s dedupe is protected against overcounting but not yet certified against undercounting — read no claim here as “the key is a complete invariant” or “Kd is finished.” It isn’t, yet.
Open seams, named rather than glossed over:
ce, ceM) as supplied data. Tying that supplied data back to what the real keyer actually computes (_ceFromCore) at every one of the swept horizons — not just the one default horizon the previous round handled — is deferred to D-G/D-H.CompositeIso still has no general way to flip an isomorphism through the mirror or compose two of them (symm/trans are undefined). K1d’s mirror branch works around this by asking the caller to hand it both isomorphisms (E and EM) separately rather than deriving one from the other — so any later proof that wants the mirror branch has to build that derivation itself. That is named, explicitly, as D-H’s job.fm, rf, the nesting-table entries) are still uninterpreted natural numbers in the model, not yet tied to actual geometric faces of a real arrangement — the same standing gap since this campaign’s first round.None of this is a defect in K1d. It is the honest shape of a half-finished theorem: this repository’s discipline is trusting the label over the location, and the label here is “invariance, proved; separation, not yet; three named seams underneath both.”
Next in the chain: the Boomerang.