On 2 September 2026 Hubble OPAL imagery established a wavenumber-ten pattern encircling Saturn’s south pole — the first regular polygonal jet observed in that hemisphere, alongside the north polar hexagon that has been present in every observation for more than forty years. CHECKED
Three days later this series published, in Vol V §4 and on a standalone page, the following:
The hexagon and the decagon are not two symmetries of one field — the only field admitting both is the trivial one.
It rested on a theorem, hex_and_dec_forces_constant, which had been through the Lean kernel and reported [propext, Quot.sound]. No sorryAx. The theorem is true. It is still true. What follows is not a retraction of it.
Represent a field on a polar ring as a function on a finite number of angular sectors. To carry a sixfold and a tenfold symmetry at once, the sector count must be a common multiple of six and ten; the smallest is thirty, and thirty is what was chosen.
On thirty sectors a sixfold pattern repeats every five and a tenfold every three. Sums and differences of five and three reach every one of the thirty, so a field carrying both takes the same value everywhere. It is constant. KERNEL COMPUTED
Every word of that is right, and the theorem states exactly it — hypotheses Periodic v 5 and Periodic v 3, conclusion ∀ k, v k = v 0. The numbers five and three are in the statement. They are where thirty is hiding. The prose translated them back into “sixfold” and “tenfold” and dropped the grid that made the translation valid.
Take sixty sectors instead. Nothing forbids it: sixty is a common multiple of six and ten, so both symmetries are expressible there, and every sixfold field on thirty sectors lifts to one on sixty.
Two, not one. So on sixty sectors the two symmetries force a field only to have period two — and a non-constant field of period two exists, immediately:
alt(k) = k mod 2 on the sixty-sector ring.
alt(k+10) = alt(k) — sixfold. alt(k+6) = alt(k) — tenfold. alt(1) ≠ alt(0) — not constant. KERNEL
The published sentence asserted that no such field exists. One does. The forcing-to-constant was never a fact about six and ten; it was a fact about taking the minimal common refinement, where the subgroup the two symmetries generate happens to exhaust the grid.
Orbit counting over every refinement from thirty to twelve hundred gives the pattern without assuming it. The dimension of the invariant space — the number of values a field carrying both symmetries is free to choose — is N/30 at every step, and equals one only at N = 30. COMPUTED
| Sectors N | sixfold period | tenfold period | gcd | free values | reading |
|---|---|---|---|---|---|
| 30 | 5 | 3 | 1 | 1 | constant — the case that was published |
| 60 | 10 | 6 | 2 | 2 | period two; alt is the witness |
| 90 | 15 | 9 | 3 | 3 | period three |
| 120 | 20 | 12 | 4 | 4 | period four |
| 150 | 25 | 15 | 5 | 5 | period five |
The group-theoretic statement is the one that does not mention a grid at all. Rotation by 2π/6 and rotation by 2π/10 generate rotation by 2π/30: the subgroup of the circle group they generate is C30.
A field carrying both a sixfold and a tenfold symmetry is invariant under C30, and no more. On a ring of N sectors it has period N/30. It exhibits neither a hexagon nor a decagon. It exhibits a thirty-sided pattern.
At N = 30 this reads “constant”, because N/30 = 1. That is the whole of the original result, recovered as one case.
The general fact is Euclid’s algorithm on periods, and it was already half-written: the file carried periodic_sub — two periods give their difference — which is the Euclidean step. What it lacked was the closure.
With periodic_add and periodic_mul giving multiples, periodic_mod gives the remainder, and periodic_gcd recurses on it exactly as Nat.gcd does. hex_and_dec_forces_constant is now the case gcd(5, 3) = 1, and the sixty-sector case is gcd(10, 6) = 2 with alt attached to it.
Audited the same day. bash tools/leancheck.sh --audit PolarPolygonCommonRefinement.lean — 7 s, 15 declarations, 0 trusting sorryAx, nothing outside propext, Classical.choice, Quot.sound. KERNEL
| Declaration | Rests on |
|---|---|
| periodic_add | — no axiom at all |
| alt_not_constant | — no axiom at all |
| alt_periodic_ten | propext |
| alt_periodic_six | propext |
| sixty_sectors_permit_structure | propext |
| periodic_mul | propext |
| periodic_mod | propext, Quot.sound |
| periodic_gcd | propext, Quot.sound |
Five of the file’s fifteen declarations rest on no axiom whatever — not even propext. That is the strongest outcome #print axioms can report, and a gate that counts only the depends on axioms: form is blind to it; see WP-73 §6, where a CI job failed a file over its own three best results for exactly that reason.
The corrected statement is stronger than the one it replaces, which is not the usual direction for a correction and is worth being explicit about.
“The only field admitting both is trivial” named no observation. Nothing could have been looked at to test it, because a trivial field is not a thing a telescope resolves. The replacement names one: a single field carrying both symmetries would show thirty sides. Nobody has photographed a triacontagon on Saturn. So the two polygons remain two rings — two jets, in two hemispheres — and the claim now carries its own refutation condition.
It does not explain why the decagon exists. NASA does not either — the discovery team states the mechanism is not known and asks openly why it formed now. CHECKED Wavenumber selection in a rotating stratified fluid is a stability question turning on measured quantities: jet latitude, width, shear, deformation radius. No theorem supplies those. Every result in this note is a statement about periodic functions on a finite ring. None of them is a statement about Saturn.
WP-73 separated the ways a verification claim comes loose from its artifact — MISMATCH, STALE, FAIL — and then four more concerning the artifact itself: FALSE, VACUOUS, UNTRUSTED, MISATTRIBUTED. This defect is none of them, and it is nearest to the last two.
| Class | What is wrong | Detected by |
|---|---|---|
| VACUOUS | the statement has no content | a declared-baseline scan; fully only on the elaborated type |
| MISATTRIBUTED | the statement is true but does not support the claim made from it | nothing, and nothing can |
| OVER-GENERALISED | the statement is true and does support a claim — a narrower one than the prose makes, because a parameter fixed in the statement reads in prose as a constant of nature | instantiating the statement at a second value of that parameter |
The distinguishing feature is that it is mechanisable, unlike MISATTRIBUTED, and cheaply: the test is to ask what the theorem says at another value of every number appearing in its hypotheses. Here the numbers were five and three; asking what happens at ten and six took one line of arithmetic and overturned a published sentence. A theorem whose hypotheses contain a numeral that the surrounding prose does not mention should be read as a warning.
The question that found this was whether base sixty would change the arithmetic. It was asked twice. The first time it was answered — correctly, and uselessly — that a base is notation and changes no number. That answer is true and was not responsive: the questioner was not proposing to write thirty differently, but pointing at sixty as a quantity with room where thirty has none, because 60/6 and 60/10 still share a factor while 30/6 and 30/10 do not. The instinct was right and the vocabulary was borrowed. Dismissing the vocabulary cost the finding for a day.
This is the second such episode in this series inside a week. The other concerned ε0 = 1/3, described in a draft as “a chosen threshold” when it is a Grönwall bound, and corrected by the same reader on the same grounds — that the description named the wrong kind of object. Both times the correction arrived in words that were easy to argue with and pointed at something that was not.
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.