SaturnHexagon.lean carries six definitions and five theorems on Fin 6, and its header is one of the more careful in this corpus: it records two false starts, a header that claimed verification which had not happened, the retraction of that claim, and the decay of two theorems across toolchain versions. As of 2026-08-21, under Lean v4.33.0-rc1, all five report [propext, Classical.choice, Quot.sound] — no sorryAx. CHECKED
A first pass here counted three sorry occurrences in the file. All three are in that header, describing the earlier failure. Stripping block comments, the code contains zero. COMPUTED
The coupling operator is
which is the adjacency operator of the cycle graph C₆, and hex c is its constant eigenvector at eigenvalue 2. Neither of those facts involves the number six. Restated:
hex_rotation_invariant and hex_coupling_uniform hold verbatim for the cycle on any number of sectors. Fin 6 is a choice of instance, not a consequence of anything proved. The file establishes that the hexagon is a fixed point. It does not establish that it is the fixed point, because six entered as a hypothesis and left as one.
CycleCoupling.lean states the same three results over ZMod (n+1), with the six replaced by a variable, and specialises them back to six as corollaries. If it typechecks, §2 stops being a reading and becomes a theorem.
lake env lean CycleCoupling.lean in ~/Desktop/geometry, under leanprover/lean4:v4.32.0, returns for each of the three theorems: [propext, Classical.choice, Quot.sound]. No sorryAx, no errors, and the three example blocks specialising to six typecheck. COMPUTED
So §2 is no longer a reading of a file. It is a theorem that SaturnHexagon.lean’s content is available at every sector count, and that Fin 6 entered as a hypothesis.
Both anticipated failures occurred, and both are recorded in the file’s header. Over Fin (n+1), abel reported “made no progress” and so did simp; neither engaged that type’s additive structure. The fix was not a third tactic but a change of index type to ZMod (n+1), a genuine CommRing, where ring discharges both goals. The two types agree, so the mathematics did not change — arguably it is now stated over the right one, since the vertex set of a cycle is ℤ/n. CHECKED
Provenance. SaturnHexagon.lean’s own clean run was recorded in the orthogenesis tree under v4.33.0-rc1; this file was verified in geometry under v4.32.0 — a different toolchain, stated because that file’s header is a catalogue of exactly this drift.
The same gap appears three times in this corpus, and naming it is the point of the note.
Everything the corpus holds is a stability result. Saturn’s question is a selection result. Stability says that once a pattern is there it stays; selection says how it got there. They are different theorems, and no amount of the first supplies the second.
The current literature answers selection dynamically rather than mathematically: Yadav and Bloxham (2020) find that “self-organized turbulence in the form of giant vortices pinches the eastward jet, forming polygonal shapes.” CHECKED No resonance, no phase-locking. Resonance-adjacent language does apply to a narrower question — a Rossby wave whose westward phase speed cancels the eastward jet stands still, which is why the hexagon’s motion is measured as long-term steady — but that explains why it does not drift, not why it has six sides.
The spectrum of the cycle Cn is 2 cos(2πk/n). Ask when the angular coupling has an integer spectrum:
Cn is integral exactly for n ∈ {3, 4, 6}, and six is the largest. COMPUTED That is the same set WP-103 derives from lattices, reached here from the operator’s spectrum with no lattice present — the same 2 cos in both places, because both are ℤ/n acting, but a different hypothesis and so a second route rather than a restatement.
The mathematics is classical. Integral graphs are Harary & Schwenk, Which graphs have integral spectra? (1974); the integral circulants are a studied family. Nothing in the table above is new. CHECKED
The application appears to be unprecedented — a search of the hexagon literature (Allison–Godfrey–Beebe 1990; Barbosa Aguiar 2010; Rostami & Sánchez-Lavega 2017; Marsh 2017; Yadav & Bloxham 2020) returns nothing using spectral integrality as a wavenumber criterion. Unprecedented is not the same as justified.
The hypothesis is unargued, and that is the real gap. On a lattice, integrality descends from a rotation matrix with entries in ℤ. There is no matrix over ℤ here. Why a jet should have an integer spectrum has no physical argument in this note. OPEN Until it does, §5 is a coincidence of arithmetic with the right shape, and this corpus has a standing rule about those.
It also selects {3, 4, 6} rather than 6 alone. “Largest integral cycle” is a choice, not yet a principle.
WP-102 and WP-103 supply φ(n), cut-and-project, and the embedding dimensions. All of it constrains what a lattice can carry. A zonal jet has no translational order, so the hypothesis has nothing to bite on and the theorems return nothing. The six in ℤ[ω] and the six in a polar jet are the same integer reached by unrelated routes, which is the bridge tools/verify-polar/README.md refuses and is right to refuse.
It proposes no mechanism. OPEN §3 is unverified. §5 rests on an unargued hypothesis and is carried as a proposal, not as support for anything. The φ(n) material of WP-103 is crystallography and does not reach an atmosphere.
Not deposited. The mathematics of §5 is fifty years old and the application has no physical argument; a deposit built on that would be answering a referee’s first question with silence. What would earn one, in order: run CycleCoupling.lean so §2 becomes kernel-checked; then argue the integrality hypothesis or kill it. A negative outcome on the second is publishable and is what WP-98 already is.
[1] Harary & Schwenk, “Which graphs have integral spectra?”, in
Graphs and Combinatorics, Springer LNM 406 (1974).
[2] Yadav & Bloxham, “Deep rotating convection generates the polar hexagon on Saturn”,
PNAS 117, 13991 (2020); arXiv:2007.08958.
[3] Allison, Godfrey & Beebe, “A wave dynamical interpretation of Saturn’s polar
hexagon”, Science 247, 1061 (1990).
[4] Rostami, Sánchez-Lavega et al., “On the dynamical nature of Saturn’s
North Polar hexagon”, Icarus 297, 59 (2017).
[5] Barbosa Aguiar et al., “A laboratory model of Saturn’s North Polar
Hexagon”, Icarus 206, 755 (2010).
[6] This corpus: SaturnHexagon.lean,
CycleCoupling.lean, book4/ch18-seismic-lattice.html,
tools/verify-polar/README.md, WP-100 §7, WP-103.
sorryAx. A clean axiom report is not a reading of the statement: per R20, a theorem can assume its conclusion and still report clean. Follow the link before citing one as evidence.