the Mirage

D-H revised · todo/lean/080 · disconnected-keyer campaign, Relay 6 · kernel-checked 2026-07-17

A mirage is a thing you are sure you can see until you walk up to where it should be. D-H, “the Ledger,” wrote the disconnected census balance as a single theorem — $|T_d| = |K|$, the true count of disconnected sphere-types set equal to the count of distinct keys the census emits — and one of that theorem’s two columns, no-overcount, it entered on credit: a typed hypothesis, hkeyInj, that distinct decoded types always carry distinct keys. This round walked up to that hypothesis and asked the only question that matters of an assumption: is it actually true? It is not. hkeyInj is kernel-false on census data.

That sentence sounds like a retraction. It is the opposite. Chasing why the assumption fails is what taught the model what a disconnected sphere-type actually is — and the repaired theorem that replaces the Ledger is stronger than the one it supersedes: no-overcount is now derived, not assumed. The mirage was never the theorem. It was the belief that the coarse notion of “same arrangement” the Ledger quietly leaned on was fine enough to count with.

The assumption, and why it looked safe

Recall the shape of the Ledger. K is the finite set of distinct keys the composition enumerator emits after deduping; $T_d$ is the true, finite set of disconnected sphere-types. The obligation Kd asks two independent things of the dedupe. No-undercount: every true type has a representative key. No-overcount: two surviving keys really are two types, so K never inflates $T_d$’s count by naming one type twice. The Ledger derived the first and assumed the second, writing it down as a hypothesis and saying so in its own docstring rather than in a footnote.

Why did assuming it look safe? Because the notion of “same type” the hypothesis was stated against — $\cong_n$, nesting-respecting composite isomorphism, packaged as CompositeIso and quotiented into stypeOf — is the obvious one. Two composites are the same sphere-type when there is a relabeling of their clusters that respects every crossing and every nesting. It is the disconnected analog of the relation that served the connected campaign perfectly. Nobody had reason to doubt that distinct keys could only mean distinct types under it. The refutation is the discovery that this obvious relation is, on the disconnected stratum, genuinely too coarse — and it bites on an arrangement small enough to draw.

The two arrangements the assumption merged

The counterexample is a pair, $\text{lens} \sqcup \text{bare} \sqcup \text{bare}$: a lens — two circles crossing twice, providing the host faces — with two uncrossed “bare” circles set down inside it. The lens carves its sphere into named faces: an outer face, two crescents (inside one lens circle, outside the other), and a middle (inside both — the lens-shaped intersection). The pair differs in which faces the two bares occupy.

These are visibly different arrangements, and the census keyer knows it: it gives them different keys. That is the whole job of the keyer, and it does the job. Both are real, canonical, decoder-ready census entries — each key is attained at its own default gauge (lbb_attained), each composite passes the full DecodeReady package (lbbSplitReady/lbbStackReady). And yet, under the coarse relation, they have the same type:

So any emitted family K that contains both keys — and the real census contains both — satisfies every other hypothesis of the Ledger and falsifies hkeyInj. The conditional bijection is not merely unproven on the census; it is vacuous there, its no-overcount premise provably false. That is hkeyInj_refuted, and it is checked by the kernel, not argued in prose:

theorem hkeyInj_refuted :
    ¬ (∀ P Q : PackedComposite, P.typeOf = Q.typeOf →
        P.key serListCtrlOrd = Q.key serListCtrlOrd) :=
  fun h => lbb_keys_ne (h _ _ lbb_typeOf_eq)

Decoded: feed the assumed injectivity two composites with equal typeOf (lbb_typeOf_eq, the old quotient merging split and stacked) and it would force their keys equal — but lbb_keys_ne says the keys differ. The two facts it rests on, lbb_keys_ne and lbb_typeOf_eq, are each by decide over the real sweep, not hand-waved. The keys are the genuine census bytes; the type-merge is one honest $\cong_n$ step.

Why the coarse relation is genuinely too coarse

The failure is specific and worth naming exactly, because it is the reframe. CompositeIso asks for a cluster relabeling under which every per-cluster crossing structure matches, the nesting forest matches, and each cluster’s host-face cell is consistent. The defect is in that last clause. It never compares two sibling bares’ host-face cells against each other — it only compares each cluster’s own cell against outerSel, the marker for “this is the outer face.” So the relation can check “this bare is not in the outer face” and “that bare is not in the outer face,” but never “these two bares are in the same face” versus “in different faces.” The host-face spread — the very thing that distinguishes $\{1, 2\}$ from $\{2, 2\}$ — is invisible to it.

The witness is the identity. Split and stacked are related by $\cong_n$ with cluster map $\sigma = \mathrm{id}$: the per-node witnesses ignore the outer-face gauge, inside_iff and parent_comm see only the forest (both arrangements: two bare children inside the one lens root), and locFace_bare only ever inspects bare-host cells, which are all bareOut on both sides. Every field holds trivially, and the spread slips through untouched:

def splitStackIso : CompositeIso lbbSplit lbbStack where
  clusterEquiv := Equiv.refl (Fin 3)
  nodeIso := fun i => match i with
    | ⟨0, _⟩ => DartIso.refl lens
    | ⟨1, _⟩ => PUnit.unit
    | ⟨2, _⟩ => PUnit.unit
  locFace_bare := by decide
  inside_iff := by decide
  parent_comm := by decide

Decoded: a complete $\cong_n$-witness between two composites that are not the same sphere-type. It is not a bug in this witness — the witness is correct about what $\cong_n$ demands. It is a demonstration that $\cong_n$, on bare composites, demands too little.

What the refutation actually teaches

Here is the turn. The refutation is the model learning what a disconnected type is. A bare CompositeMap carries face-ids that are, at this modeling depth, uninterpreted numbers — the interpretation that would pin them (Gd1, the face-id semantics) is fenced, not yet cashed in the kernel. To CompositeIso, a face label is a token it is free to permute, and because it only ever tests a cell against the single distinguished outerSel, it never fixes two labels relative to each other. So a bare composite, on its own, cannot define a sphere-type finely enough to tell $\{1, 2\}$ from $\{2, 2\}$. Only a composite that also carries its gauge — its rooting, its per-rooting encoding tables, the sweep data the sphere key is actually computed from — has enough structure to.

Read that way, the “repair” below is not a workaround bolted on to route around a failure. It is the correct definition of $\cong_n$ at the model’s granularity. The coarse stypeOf was standing in for the right notion of sameness and getting it slightly wrong; the swept relation is the right notion, stated on the objects that actually carry enough information to support it. And the debt that gets “relocated” in the process turns out to be a pre-existing deferred item — finally priced honestly instead of hidden inside an assumed hypothesis.

The swept repair: no-overcount, derived

Move the quotient off bare composites and onto PackedComposite — a composite bundled with exactly the sweep data its sphere key needs: the face map fm, the rooting list rf, the per-rooting encoding tables ce and ceM, the circle count. Relate two packed composites by IsoOrMirrorSweptR: they agree on circle count and are related by the verbatim hypothesis package the promoted descent lemma sphereKeyToks_k1d consumes — a plain $\cong_n$ with a mirror-side companion, or an $\cong_n$ onto the diagonal mirror $\overline{Q}$ with the crossed companion, in each case with a rooting correspondence and, per rooting, a GaugeCorresponds record tying the two sweeps together.

The point of stating the relation this way is mechanical and decisive. Because every step carries sweep data, sphereKeyToks_k1d fires on each step: related packed composites have equal keys (IsoOrMirrorSweptR.key_eq). And key-equality, being an equality, absorbs refl, symm, and trans for free — so it survives the entire EqvGen equivalence closure without needing the relation itself to be transitively closed (key_eq_of_eqvGen). This is exactly the “closure collapse” the old design kept deferring. The old design deferred it because, on bare composites, it can never exist — that is what the refutation proves. On packed composites it is three lines of induction:

theorem PackedComposite.key_eq_of_sweptTypeOf_eq {P Q : PackedComposite}
    (h : P.sweptTypeOf = Q.sweptTypeOf) (sord : LinearOrder (List SerTok)) :
    P.key sord = Q.key sord :=
  PackedComposite.key_eq_of_eqvGen (Quotient.exact h) sord

Decoded: equal swept types force equal keys. This is the statement hkeyInj assumed, now a theorem — no-overcount, derived. Under the swept quotient, $$\mathrm{sweptTypeOf}(P) = \mathrm{sweptTypeOf}(Q) \;\implies\; \mathrm{key}(P) = \mathrm{key}(Q)$$ is a proof, not a premise.

With no-overcount discharged inside the quotient, the statement of record needs no injectivity hypothesis at all. composite_census_complete_swept takes the census family, per-key canonicity, soundness, and generation — and returns the bijection, plus the strong pairwise conjunct: distinct keys decode to composites that are not even EqvGen-related.

theorem composite_census_complete_swept (sord : LinearOrder (List SerTok))
    {K : Finset (List SerTok)} (dec : ∀ k ∈ K, PackedComposite)
    -- Gd3: each emitted key re-keys to itself
    (hcanon : ∀ k (hk : k ∈ K), (dec k hk).key sord = k)
    {Td : Finset SweptSphereType}
    -- Sd2 soundness: every emitted key names a genuine type
    (hmem : ∀ k (hk : k ∈ K), (dec k hk).sweptTypeOf ∈ Td)
    -- L2 + generation-exhaustiveness + connected-≤-5, with the swept decode step (Gd2/Gd4 seam)
    (hgen : ∀ t ∈ Td, ∃ (g : PackedComposite) (hk : g.key sord ∈ K),
      g.sweptTypeOf = t ∧
      Relation.EqvGen PackedComposite.IsoOrMirrorSweptR (dec (g.key sord) hk) g) :
    (∀ k₁ k₂ (hk₁ : k₁ ∈ K) (hk₂ : k₂ ∈ K), k₁ ≠ k₂ →
        ¬ Relation.EqvGen PackedComposite.IsoOrMirrorSweptR (dec k₁ hk₁) (dec k₂ hk₂)) ∧
      Td.card = K.card := by
  -- proof elided here (∼26 lines) -- kernel-checked, standard axioms only.
  -- injectivity DERIVED from key_eq_of_sweptTypeOf_eq + hcanon; surjectivity from hgen's
  -- swept step; closes with Finset.card_image_of_injOn + Finset.card_attach.

Decoded: four hypotheses in — canonicity, soundness, generation, and the family itself — a genuine bijection out, with no hkeyInj. Compare the Ledger’s six-hypothesis signature: the assumed no-overcount premise is simply gone, replaced by a derivation. This is strictly stronger than the theorem it supersedes.

The contrast the round exists to draw fits in two lines. The old quotient merges the refutation pair; the swept quotient separates it, via the derived injectivity:

theorem lbb_stypeOf_eq   : lbbSplit.stypeOf = lbbStack.stypeOf := …      -- the bug
theorem lbb_sweptTypeOf_ne : lbbSplitP.sweptTypeOf ≠ lbbStackP.sweptTypeOf :=  -- the fix
  fun h => lbb_keys_ne (PackedComposite.key_eq_of_sweptTypeOf_eq h serListCtrlOrd)

Decoded: same pair, two quotients. stypeOf identifies them (equal type — the merge the refutation exploits). sweptTypeOf distinguishes them, because equal swept types would force equal keys and the keys differ. The bug and the fix, kernel-pinned, side by side.

The one honest open seam: the gauge replay

Nothing is free. What moved, rather than vanished, is the no-undercount cost — and moving it made it visible. In the repaired theorem, every true type’s witness must arrive with a swept relation between the decoded key and the generator g: the hgen hypothesis now carries a full EqvGen PackedComposite.IsoOrMirrorSweptR (dec (g.key)) g. That relation has two components. Its $\cong_n$ component — that decode and generator are isomorphic-or-mirror — is discharged on census data by the Boomerang’s attainment-qualified K2d, exactly as before. Its GaugeCorresponds component — the per-gauge _ceFromCore correspondence tying the two sweeps rooting-by-rooting — is the one named open seam: the gauge replay.

This is not a new debt. It is the same (a)-layer correspondence D-F deferred rounds ago, when the keyer’s two directions were first laid down. What the Ledger did was bury that debt inside an assumed hkeyInj, where it read as one clean hypothesis. The refutation forced it into the open; the swept repair prices it honestly, as a single per-gauge correspondence that is Gd2-shaped, true on census data, and underivable at the current modeling depth. So Kd, the disconnected keyer obligation, is not complete: what it now has is a non-vacuous conditional bijection — no-overcount derived, no-undercount resting on one honest, named seam — where before it had a conditional bijection that was vacuous on the very census it was built to count.

That the repair is non-vacuous is not a claim on credit either. swept_census_control fires the whole statement end-to-end on a one-key family, every hypothesis discharged, $|T_d| = |K|$ concluded:

theorem swept_census_control :
    (({lbPacked.sweptTypeOf} : Finset SweptSphereType)).card
      = (({lbKey} : Finset (List SerTok))).card := by
  classical
  have hkey : lbPacked.key serListCtrlOrd = lbKey := lensBare_sphereKey
  refine (composite_census_complete_swept serListCtrlOrd
    (K := {lbKey}) (fun _ _ => lbPacked)
    (fun k hk => hkey.trans (Finset.mem_singleton.mp hk).symm)
    (Td := {lbPacked.sweptTypeOf})
    (fun k hk => Finset.mem_singleton_self _)
    ?_).2
  intro t ht
  refine ⟨lbPacked, by rw [hkey]; exact Finset.mem_singleton_self _,
    (Finset.mem_singleton.mp ht).symm, Relation.EqvGen.refl _⟩

Decoded: the Ledger shipped no such control — a coverage gap the cold review flagged. The swept repair closes it: a concrete K on which the joint hypothesis bundle is satisfiable in the kernel, retiring the banked toy-K non-vacuity follow-up outright.

What’s proved, and what isn’t — and what is untouched

The trust labels, plainly. The original composite_census_complete is now proved-vacuous-on-the-census: hkeyInj_refuted is kernel-checked on standard axioms (every decide a real kernel reduction, never native_decide, no sorry), and it shows the old conditional bijection establishes nothing about the census cardinality. The statement of record is now composite_census_complete_swept: a proved-about-model conditional bijection with no-overcount derived and exactly one named open seam, the gauge replay. Kd is not complete. The refutation and the repair were both put through a firewalled adversarial Opus cold review — independent #print axioms on every headline result, the refutation confirmed to target the genuine develop objects rather than a strawman, the repair confirmed a sound derivation that still counts the census — verdict CONFIRMED.

Now the part that must be said just as plainly, because a reader who stops at “a proof was refuted” will draw exactly the wrong conclusion. The realized lower bound and the disconnected counts are completely unaffected. L(6) = 308,727 stands. The disconnected census — 16,547 realized, 16,597 types — stands. The bracket is unchanged:

The reason is the root cause. This is a Lean formalization gap, not a census defect. Split and stacked genuinely are distinct sphere-types — a homeomorphism cannot move a circle between two different faces — and the Python keyer already knew that: it gave them distinct keys. The keyer was handed a kernel-grade adversarial probe, engineered from inside the proof to try to make two truly-different arrangements collide, and it separated them cleanly. That is the strongest evidence the disconnected keyer has ever had. What reverted is narrow and exactly stated: the Lean-kernel backing for “distinct keys ⇔ distinct types” on the disconnected stratum drops back to trusted-by-construction — precisely where it sat before D-H was ever written — pending the repair’s one open seam. And Sd, “No Phantoms,” the disconnected generator-soundness result, is untouched.

A mirage does not cost you anything real when you walk through where it was; it costs you a belief you should not have held. The belief here was that the coarse relation was a fine enough notion of sameness to enter no-overcount on credit. Walking up to it returned a better theorem — no-overcount proved rather than promised — and a correct understanding of what a disconnected type requires: not a bare arrangement, but an arrangement that carries its gauge. The one debt left standing has a name, a location, and a stated reason it is not yet paid. Everything the census actually counts came through the walk exactly as it went in.