the Gauge Replay

Kd seam · todo/lean/080 · disconnected-keyer campaign, round P-2 · kernel-checked 2026-07-17

There are two ways a round can finish with a proof. It can discharge an open hypothesis, or it can prove that the hypothesis cannot be discharged in the language it is written in. This round tried the first and got the second. The one seam the swept repair left standing — hgen’s per-gauge GaugeCorresponds, the gauge replay — will not close from the per-key package alone, and now there is a kernel proof of exactly that. A negative result, but a load-bearing one: it is a signpost, planted in the kernel, that reads do not try to close this seam in the current vocabulary.

This essay is the sequel to the Mirage. That round refuted the Ledger’s assumed no-overcount hypothesis, then repaired the theorem so that no-overcount is derived rather than assumed — and it named the single debt the repair could not pay in cash: a per-gauge correspondence tying two rooting sweeps together, rooting by rooting. The Mirage set the seam down and priced it honestly. This round walks up to the seam and asks whether it can be paid from what a key already carries. The answer is no, and the value of the round is in knowing that the answer is no — because an open hypothesis with a proof of irreducibility is a very different object from an open hypothesis nobody has managed to close yet. The first is a boundary; the second is a to-do.

The one seam the swept repair left

Recall the shape of the repaired statement. composite_census_complete_swept quotients gauge-carrying PackedComposites by a data-carrying relation, IsoOrMirrorSweptR, and concludes the census balance $\lvert T_d \rvert = \lvert K \rvert$ over four hypotheses. Three are the familiar fences — canonicity (hcanon, Gd3), soundness (hmem, Sd2), and generation (hgen, the Gd4 surjection). The novelty is that hgen now carries, for every generated type, a full swept relation between the decoded key and the generator g:

Relation.EqvGen PackedComposite.IsoOrMirrorSweptR (dec (g.key sord) hk) g

Decoded: for each true type, the object you decode from its key and the object the generator produces must be connected by a chain of swept steps. That chain is the price of deriving no-overcount inside the quotient.

A swept step 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 in the Mirage. Its GaugeCorresponds component — the per-gauge _ceFromCore tables tying the two sweeps together at every rooting — is the one thing the repair does not derive. That is the gauge replay: to replay one composite’s rooting sweep against the other’s and check that the per-gauge marks agree, gauge by gauge. The question this round asked is the only one that decides whether the seam is a boundary or a chore: can that replay be reconstructed from the per-key package — equal keys, canonicity, the DecodeReady data — without ever interpreting the raw face-ids?

A key is a minimum; the swept step is the whole profile

The obstruction is an information mismatch, and it is worth stating exactly, because it is the whole result. A composite’s key is not a single serialization. It is the minimum over a profile of serializations, one per rooting of the arrangement: root every host face in turn, serialize each rooting in both orientations, take the per-rooting minimum, and the key is the smallest entry of that whole list. In Lean the profile is sweepKeys and the reduction to its minimum is one line of rfl:

theorem PackedComposite.key_eq_bestTail_sweepKeys (P : PackedComposite)
    (sord : LinearOrder (List SerTok)) :
    P.key sord = bestTail sord (P.sweepKeys sord) := rfl

Decoded: the sphere key is the profile’s minimum, definitionally. Everything the profile records about a losing rooting is discarded the moment the minimum is taken.

Write the profile as a list and the picture is immediate:

\text{key} \;=\; \operatorname{bestTail}\big(\,[\,k_{r_1},\, k_{r_2},\, \dots,\, k_{r_m}\,]\,\big).

The key sees the sweep through a single slot: the winner, $\min_r k_r$ . Every other rooting — every loser — contributes nothing the key can report. The swept relation is built on the opposite principle. A single swept step does not just match winners; it transports the whole profile, up to the permutation that renames rootings. That is sweepKeys_perm, and lifting it across the entire EqvGen closure — so the whole chain a witness might use is covered — is one short induction:

theorem PackedComposite.sweepKeys_perm_of_eqvGen {P Q : PackedComposite}
    (h : Relation.EqvGen PackedComposite.IsoOrMirrorSweptR P Q)
    (sord : LinearOrder (List SerTok)) : P.sweepKeys sord ~ Q.sweepKeys sord := by
  induction h with
  | rel _ _ hr => exact (hr.sweepKeys_perm sord).symm
  | refl _ => exact List.Perm.refl _
  | symm _ _ _ ih => exact ih.symm
  | trans _ _ _ _ _ ih₁ ih₂ => exact ih₁.trans ih₂

Decoded: any two composites connected by a chain of swept steps have profiles that are permutations of one another ( $\sim$ is List.Perm). Permutation absorbs the reflexive, symmetric, and transitive closure — so the profile is an invariant of the entire swept-relatedness, not just of a single step.

Here is the gap, stated as an asymmetry. The key remembers one entry of the profile and forgets the rest. Swept-relatedness remembers all of them, as a multiset. So the swept step constrains strictly more than the key does — and the difference is exactly the losing rootings. If two composites can be made to agree on the winner and disagree on a loser, their keys are equal but they cannot be swept-related. All that remains is to exhibit such a pair as a genuine, admissible object.

The counterexample: one losing rooting, re-marked

The pair is lbbSplit — the same arrangement the Mirage refuted with — against a twin of itself, lbbSplitTw, that differs at a single losing rooting the key never looks at. lbbSplit is a lens (two circles crossing twice, providing three bounded host faces) carrying two bare circles: one in a crescent, one in the central almond, occupied-face multiset $\{1, 2\}$ . The third host face — the far crescent, face 3 — is empty. It is a real face; it is simply unoccupied. And because it is unoccupied, no bare circle roots there, so no serialized token ever mentions it. The key cannot see face 3, for the plain reason that face 3 puts nothing into the key.

lbbSplit, drawn to the combinatorics that carry the argument. The lens circles (radius 64, centers 80 apart) cross at

(240, 130.0)

and

(240, 230.0)

; the two rust bares sit in the left crescent (face 1) and the central almond (face 2), each clearing every lens boundary by at least 13 units. The dashed rust ring marks face 3, the unoccupied crescent — a genuine host face with no circle in it. The counterexample re-supplies one losing rooting’s mark,

0 \mapsto 7

, at the gauge

(0, \text{face } 3)

. The difference lives at a rooting the key cannot see.

Now the twin. lbbSplitTw is lbbSplit with exactly one edit: at the losing rooting $(0, \text{face } 3)$ — root the lens node at the empty crescent — the lens node’s per-gauge mark is re-supplied as $7$ instead of the probed $0$ . The face-id filters are untouched; only the mark value in that one gauge’s ce and ceM tables moves. And it is a fully admissible object, not a strawman. It shares the entire per-key package with its partner — same underlying composite, same mirror map, same rooting schedule, same default-gauge encodings, same circle count — every one of them a definitional rfl:

theorem lbbSplitTw_shares_perKey_data :
    lbbSplitTwP.C = lbbSplitP.C ∧ lbbSplitTwP.fm = lbbSplitP.fm ∧
      lbbSplitTwP.rf = lbbSplitP.rf ∧ lbbSplitTwP.ce none = lbbSplitP.ce none ∧
      lbbSplitTwP.ceM none = lbbSplitP.ceM none ∧ lbbSplitTwP.nCircles = lbbSplitP.nCircles :=
  ⟨rfl, rfl, rfl, rfl, rfl, rfl⟩

Decoded: on every input a per-key hypothesis is allowed to mention — the composite, the mirror map, the rooting-face lists, both default-gauge encoding tables, the circle count — the two objects are identical. The tweak is invisible until a non-default gauge is read.

Everything a key-level hypothesis could test comes back equal. The keys are equal and both attained at their canonical default gauge (lbbSplitTw_key_eq, lbbSplitTw_attained); the tweaked mark preserves the canonical body ++ [mark] shape (lensEncToksTw_canonical); the two objects carry the same DecodeReady package (lbbSplitTwReady). The mark that changed sits at a losing rooting, so it was never the winner and the minimum forgets it: the key is byte-for-byte the same on both sides. Only the profile has moved — one loser’s entry is now a different list — and that move is exactly what the key was built to discard.

Why no per-key hypothesis can see the difference

Put the two facts together and the seam’s status is decided. The profile is a permutation invariant of swept-relatedness; the twin’s profile is provably not a permutation of the original’s. A single kernel decide settles the second fact, and the first is sweepKeys_perm_of_eqvGen. Their composition is the round’s headline:

theorem gauge_replay_blocked :
    lbbSplitTwP.key serListCtrlOrd = lbbSplitP.key serListCtrlOrd ∧
      ¬ Relation.EqvGen PackedComposite.IsoOrMirrorSweptR lbbSplitP lbbSplitTwP :=
  ⟨lbbSplitTw_key_eq, fun h =>
    lbbSplitTw_sweepKeys_not_perm (PackedComposite.sweepKeys_perm_of_eqvGen h serListCtrlOrd)⟩

Decoded: two composites with equal keys that are provably not swept-related. If they were swept-related, their profiles would be permutations of one another; a kernel computation shows they are not; contradiction. The equal-keys conjunct and the not-swept-related conjunct hold simultaneously, in the kernel.

This is what forecloses the seam. Suppose, for contradiction, that some theorem discharged hgen’s swept step from the per-key package — a theorem of the shape “equal keys, canonicity, and DecodeReady imply the swept step.” Write $\Phi$ for that per-key antecedent and $\approx$ for swept-relatedness. Such a theorem asserts the left; the counterexample exhibits the right:

\Phi(P, Q)\ \Longrightarrow\ P \approx Q \qquad\text{vs.}\qquad \Phi(P, P')\ \wedge\ \lnot\,(P \approx P').

The pair $(P, P') = (\text{lbbSplit},\, \text{lbbSplitTw})$ satisfies $\Phi$ in full — that is precisely what lbbSplitTw_shares_perKey_data and the equal-key, same-DecodeReady lemmas establish — and yet $\lnot\,(P \approx P')$ . No implication of that shape can hold; a proof of one would combine with gauge_replay_blocked to derive $P \approx P'$ against $\lnot\,(P \approx P')$ . The repaired quotient agrees: its swept type separates the pair despite the equal keys (lbbSplitTw_sweptTypeOf_ne), so on this off-census object the swept type is strictly finer than the key.

The two sweep profiles, schematically. Each row is one rooting’s serialized key; the shortest bar (rust) is the minimum — the bestTail the sphere key reports, identical on both sides. The tweak lengthens one losing row (dashed) and leaves the winner untouched. The key reads only the highlighted row, so it cannot tell the columns apart; the swept relation must match the whole column as a multiset, and the moved loser makes that impossible. Schematic, not the literal token lists — the real inequality is the kernel decide in lbbSplitTw_sweepKeys_not_perm.

Trace the missing information back to its source and it lands on the fence the whole campaign has drawn. To reconstruct the replay per-key you would have to know where the rooting map sends face 3 — an unoccupied face that appears in no serialized artifact — and to compare the per-gauge marks the _ceFromCore filter emits at losing rootings the key never records. Both are functions of the raw, uninterpreted face-ids: choosing an image for face 3 is assigning it its geometric meaning. That is the Gd1 interpretation the campaign has fenced from the start. The seam is not slack in a proof; it is the Gd1/Gd2 fence, seen from inside the swept relation.

What this means for the count

The consequence is exact, and it cuts in the direction that helps. Because no per-key theorem can discharge hgen’s swept step, hgen is right to carry it as data. The repair was not lazy in leaving the replay in the hypothesis; it was correct, and now provably so. Closing the seam requires computing the per-gauge _ceFromCore tables in-model — interpreting the face-ids — which is a genuine extension of the model, not a lemma waiting to be found in the current one. Future work on Kd now has a precise instruction: the gauge replay closes through Gd1, or it does not close.

And the part that must be said as plainly as the Mirage said it: none of this touches what the census counts. The realized lower bound and the disconnected counts are completely unaffected. This is a statement about the derivability of one hypothesis, not about the truth of it and not about the data. hgen is not shown false — on census data the replay holds, because split and stacked and all their kin carry their gauges honestly; it is shown underivable per-key, which is a different claim. L(6) = 308,727 stands. The disconnected census stands. The bracket is unchanged:

308{,}727 \;\le\; a(6) \;\le\; 621{,}782.

What’s proved, and what isn’t

The trust label, plainly. gauge_replay_blocked and its supporting lemmas are kernel-checked on the standard three axioms — every decide a real kernel reduction, never native_decide, no sorry. What they prove is a negative result: the gauge-replay seam of composite_census_complete_swept is irreducible in the current vocabulary. The seam itself remains an open hypothesis; hgen still carries the swept step as data, byte-identically to before this round. What changed is not the theorem but our knowledge of it: the open hypothesis now comes with a kernel proof of why it is open, and a name for the interpretation layer that would close it.

The counterexample is legitimate, not a strawman. lbbSplitTw satisfies the full per-key antecedent — equal canonical-attained keys, the same DecodeReady package, every default-gauge input a rfl match — and it is exactly the kind of object any candidate “per-key implies swept-step” theorem would have to handle. The round was put through a firewalled adversarial Opus cold review, which independently ran #print axioms on every headline result, confirmed the counterexample legitimate rather than a strawman, and confirmed composite_census_complete_swept and hgen unchanged — verdict CONFIRMED. And Sd, “No Phantoms,” the disconnected generator-soundness result, is untouched.

A replay you cannot reconstruct from the winner alone is not a defect in the race; it is a fact about what a winner records. The gauge replay asks whether two arrangements agree at every rooting, and the key only ever reports one. This round did not close that gap — it proved the gap is real, drew its boundary in the kernel, and handed the next attempt the one coordinate it needs. The debt still standing has a name, a location, and now a proof that it cannot be paid in the currency of keys. Everything the census actually counts came through untouched.