sorry: the radial gate commutes with the pointwise cubic nonlinearity but not with the angular coupling; the sixfold rotation is a symmetry of the coupling; the uniform state is rotation-invariant; and the uniform state is an eigenvector of the coupling with eigenvalue 2. We observe that the last of these identifies the uniform hexagonal configuration as the Perron–Frobenius mode of the cyclic 6-ring, and that the coupling’s degenerate eigenspaces carry the two-dimensional irreducible representations of $D_6$, which is where symmetry breaking must occur. We separately record a classical index constraint: any tangent vector field on a sphere has zero-indices summing to 2, so a $D_6$-symmetric flow admitting six vortices must also admit six saddles. We do not claim a bridge between the ring and the sphere; none is established here, and constructing one is the principal open problem.
1 · Motivation, and what is not claimed
Hexagonal planforms recur across pattern-forming systems with planar rotational and translational symmetry — Rayleigh–Bénard convection, Faraday waves, Turing patterns, Chladni figures on suitably symmetric plates, and the persistent wavenumber-6 jet at Saturn’s north pole. Equivariant bifurcation theory explains this recurrence [1,2]: hexagonal planforms are generic outcomes of symmetry breaking in the relevant equivariant class, independently of the underlying physics.
That common explanation is a statement about symmetry, not about mechanism. Saturn’s hexagon is a barotropic instability of a polar jet; a Chladni figure is the nodal set of a Laplacian eigenmode on an elastic plate. These are different operators with different selection rules. They share a symmetry group and nothing else, and this paper does not assert otherwise.
What follows is deliberately minimal: the smallest $D_6$-equivariant discrete model in which the questions of invariance and of operator order can be posed exactly, together with a machine-checked proof of what that model does and does not settle. Saturn appears as motivation only. A six-site ring of real amplitudes is not a rotating shallow-water system, and no result below should be read as bearing on planetary observation.
2 · The model
State is an amplitude over six angular sextants, $\theta_k = k\pi/3$ for $k = 0,\dots,5$, represented as a function Fin 6 → ℝ. Four operators act on it.
| angCoupling v k | = v(k−1) + v(k+1), cyclic — the discrete Laplacian coupling; the only operator that moves amplitude between sextants |
| onsite v k | = (v k)3 — the $\lambda|\psi|^2\psi$ term, real cube; strictly pointwise |
| gate v k | = v k if $k$ even, 0 if $k$ odd — a 0/1 radial mask, pointwise |
| rot v k | = v(k−1) — the generator of the sixfold rotation |
The uniform or hexagonal configuration is hex c = $(c,c,c,c,c,c)$. Together, angCoupling and onsite constitute a six-site DNLS ring with real amplitudes: a discrete Laplacian plus a cubic on-site nonlinearity, closed cyclically [3].
3 · Results [PROVED]
All five are proved in Lean 4 with Mathlib, without sorry. For each, #print axioms reports [propext, Classical.choice, Quot.sound] and no sorryAx.
| Statement | Reading | |
|---|---|---|
| T1 | gate (onsite v) = onsite (gate v) | The radial gate commutes with the pointwise nonlinearity. |
| T2 | angCoupling ∘ gate ≠ gate ∘ angCoupling | It does not commute with the angular coupling. Order is observable. |
| T3 | rot (angCoupling v) = angCoupling (rot v) | The sixfold rotation is a symmetry of the coupling: $D_6$-equivariance. |
| T4 | rot (hex c) = hex c | The uniform configuration is rotation-invariant. |
| T5 | angCoupling (hex c) = hex (2c) | The uniform configuration is an eigenvector, eigenvalue 2. |
T1 and T2 together are the substantive pair. A gate acting pointwise commutes with any pointwise map, so T1 is expected; T2 shows that the same gate fails to commute with the operator that moves amplitude between sextants. Order-dependence in this model is carried entirely by the angular coupling, and not by the nonlinearity.
4 · Spectral reading of T5
angCoupling is the adjacency operator of the cyclic graph on six vertices. Its eigenvectors are the discrete Fourier modes $v_k(j) = \exp(2\pi i\,kj/6)$ with eigenvalues $\lambda_k = 2\cos(2\pi k/6)$.
angCoupling (hex c) = hex (2c) — places the uniform configuration at $\lambda = +2$, the Perron–Frobenius mode: the unique eigenvector of largest eigenvalue with constant sign. The two degenerate pairs, at $+1$ and $-1$, are the two-dimensional irreducible representations of $D_6$, and any symmetry-breaking bifurcation from the uniform branch must occur inside one of them.The model therefore contains both the invariant state and the modes that compete with it, which is the minimum needed to pose a mode-selection question. What it does not yet contain is the dynamics that would decide between them.
5 · An index constraint on the sphere [CLASSICAL]
The following is standard and is included because it constrains any attempt to place a $D_6$ pattern on a closed surface. By the Poincaré–Hopf theorem [4], a tangent vector field with isolated zeros on a closed surface has zero-indices summing to the Euler characteristic. For the sphere, $\chi(S^2) = 2$, so a global flow cannot be everywhere non-vanishing: fixed points must exist, and their indices must total exactly 2.
6 · What is not established [OPEN]
- No equation of motion is formalised, so no stability result is available. Writing the flow explicitly is the immediate next step; linearising the cubic at
hex cgives a Jacobian $3c^2 I$ on the diagonal, and a per-mode threshold in $\lambda_k + 3c^2$ follows at once. That calculation is not performed here. - Which isotropy subgroup breaks first as amplitude grows is not determined.
- The correspondence between the ring and any field on a surface is not constructed (§5).
- No claim is made that the model bears on Saturn, on Chladni figures, or on any physical system. A shared symmetry class is not a shared mechanism.
7 · Provenance
Two corrections are recorded in the source file and are reported here because they bear on how the verification should be read.
An earlier version of the surrounding work asserted that a radial gate fails to commute with a pointwise fold. That is false, and T1 is the corrected statement.
More consequentially: the first draft of the formalisation expressed the operators in vector notation. Mathlib’s Matrix.cons_val simplification lemmas do not chain to index 5 on a Fin 6 literal, so every proof silently failed into sorry, and all five theorems reported sorryAx. The kernel caught it. The definitions were rewritten by explicit pattern match, which reduces definitionally at every index, and the proofs returned clean. We record this because a formalisation that compiles is not thereby a formalisation that proves anything, and the axiom check — not the build — is what distinguishes the two.
References
[1] M. Golubitsky, I. Stewart, D. G. Schaeffer. Singularities and Groups in Bifurcation Theory, Volume II. Springer, 1988.
[2] J. W. Swift. Bifurcation and symmetry in convection. PhD thesis, University of California, Berkeley, 1984.
[3] P. G. Kevrekidis. The Discrete Nonlinear Schrödinger Equation. Springer Tracts in Modern Physics 232, 2009.
[4] J. Milnor. Topology from the Differentiable Viewpoint. University Press of Virginia, 1965.
[5] The mathlib Community. The Lean mathematical library. CPP 2020.