Formal Koide Structure: Mass Bounds, Generation Counting, and Neutrino Predictions from the Z_N Ansatz

Dr. Tamás Nagy ORCID: 0009-0004-8079-4679 Independent Researcher tnagyphd@gmail.com https://the-latent.com

April 2026

---

Abstract

The Z₃ Ansatz \(\sqrt{m_r} = a(1 + b\cos(\theta_0 + 2\pi r/3))\) with \(b^2 = 2\) is a parametrization — not a dynamical model — that encodes the Koide mass relation \(Q = 2/3\). We extract its structural implications through fifteen machine-verified theorems, showing that the Ansatz imposes a hierarchy tolerance that depends sharply on the number of generations: \(N = 3\) is the unique integer where charged leptons satisfy the parametrization but quarks do not. The mass-fraction bound \(m_{\max}/M \leq (3+2\sqrt{2})/6 \approx 97.1\%\) (T6–T9) yields an exact incompatibility threshold at \(m_{\max}/m_{\text{rest}} > 17 + 12\sqrt{2} \approx 33.97\) (T10). The N-generation extension \(Q_N = 2/N\) (T11–T15) shows the threshold drops to 2.68 at \(N=4\), excluding even leptons. We enumerate all eight neutrino sign assignments and show that normal ordering with \(\sigma_1 = -1\) is uniquely consistent; combined with NuFit 6.0 data [7], it predicts \(m_1 = 0.362 \pm 0.013\) meV and \(\Sigma m_\nu = 59.4 \pm 0.3\) meV (1σ), testable by Euclid, DESI, and CMB-S4 (mass sum) and JUNO (mass ordering). All proofs are verified in the formal proof kernel (74/74 checks, zero sorry, zero user axioms) with Lean 4 source generated. A companion paper [II] extends the analysis to all 220 SM fermion triples, flavor symmetry, radiative stability, and statistical significance.

---

1. Introduction

The Koide formula, discovered empirically by Yoshio Koide in 1983 [1], relates the masses of charged leptons through the ratio

\[Q = \frac{m_e + m_\mu + m_\tau}{(\sqrt{m_e} + \sqrt{m_\mu} + \sqrt{m_\tau})^2} = \frac{2}{3},\]

which holds to within \(0.001\%\) of experimental values [2]. Despite decades of attention, the formula lacks a consensus derivation from fundamental physics.

The Z₃ Ansatz parametrizes square-root masses as \(\sqrt{m_r} = a(1 + b \cdot c_r)\) where \(c_r = \cos(\theta_0 + 2\pi r/3)\) for \(r = 0, 1, 2\). The discrete Fourier orthogonality identities

\[\sum_{r=0}^{2} c_r = 0, \qquad \sum_{r=0}^{2} c_r^2 = \frac{3}{2}\]

together with the normalization \(b^2 = 2\) immediately yield \(Q = 2/3\). This is not a dynamical derivation: the Ansatz is a parametrization designed to encode the Koide relation, with \(b^2 = 2\) as the unique normalization that produces \(Q = 2/3\) (see §2.1). The algebraic framework has been noted by Żenczykowski [3, 4] and others, but the structural consequences of the parametrization — what mass hierarchies it can and cannot accommodate, and how these constraints depend on the number of generations — have not been systematically extracted.

Our central result is that \(N = 3\) is the unique generation count for which the Z_N Ansatz accommodates the charged lepton mass hierarchy but excludes the quark hierarchy (§4.2, Theorem 14), providing a structural (though not dynamical) argument distinguishing the observed three generations. In establishing this, we derive mass-fraction bounds showing no single mass can exceed \((3 + 2\sqrt{2})/6 \approx 97.1\%\) of the total under the Ansatz, with an exact incompatibility threshold at \(m_{\max}/m_{\text{rest}} > 17 + 12\sqrt{2} \approx 33.97\) (§3). We then generalize the Ansatz to \(N\) generations, proving \(Q_N = 2/N\) with a hierarchy tolerance that decreases rapidly with \(N\) (§4). We enumerate all eight sign assignments for the neutrino square roots and show that only \((\sigma_1, \sigma_2, \sigma_3) = (-1, +1, +1)\) with normal ordering is consistent with the Ansatz bounds; combined with NuFit 6.0 data, this yields \(m_1 = 0.362 \pm 0.013\) meV (§5).

All fifteen theorems are machine-verified in the formal proof kernel [5] with zero sorry obligations and zero user axioms. Lean 4 source code has been generated from the formal proofs; independent Lean compilation is pending (see Appendix).

Overview

Section 2 establishes the Z₃ Ansatz and derives the Koide ratio \(Q = 2/3\) (T1–T4) and the Koide angle (T5). Section 3 extracts structural consequences: mass-fraction bounds and the exact quark-incompatibility threshold (T6–T10). Section 4 generalizes to the Z_N Ansatz, proving \(Q_N = 2/N\) and showing that the threshold drops rapidly with \(N\), making \(N = 3\) the unique generation count compatible with the lepton hierarchy (T11–T15). Section 5 applies the framework to neutrinos, deriving predictions with error bars from NuFit 6.0 data. Section 6 discusses novelty, limitations, and testable predictions. The Appendix documents the formal verification infrastructure.

1.1 Related work

The Koide formula has generated a substantial literature since 1983, which can be grouped into three strands. The first seeks geometric or group-theoretic explanations: Koide's original paper [1] and Foot's 45° mixing-angle interpretation [11] fall here, as does the broad survey by Rivero and Gsponer [12]. The second strand develops the discrete Fourier (Z₃) parametrization: Żenczykowski [3, 4] formalized the framework and extended it to quark masses, identifying the phase \(\delta_\ell \approx 2/9\); Brannen [6] applied a signed-square-root convention to predict neutrino masses; Kartavtsev [13] explored "Koide tuples" across quark and lepton sectors. The third strand addresses dynamical protection: Sumino [8] showed that a U(3)\(\times\)SU(2) family-gauge symmetry can cancel radiative corrections that would otherwise destroy the Koide relation.

Our work builds primarily on the second strand but asks a different question: not "why does \(Q = 2/3\)?" but "what structural constraints does the Ansatz impose, and how do they depend on \(N\)?" The companion paper [II] bridges to discrete flavor symmetry models by identifying the Koide condition with a specific VEV alignment in \(A_4\) notation.

---

2. The Z₃ Ansatz and Q = 2/3

2.1 Setup

Let \(a > 0\), \(b > 0\) with \(b^2 = 2\), and define

\[s_r = a(1 + b \cdot c_r), \quad m_r = s_r^2, \quad r = 0, 1, 2\]

where \(c_r = \cos(\theta_0 + 2\pi r/3)\) satisfy the Z₃ Fourier identities (F1) \(\sum c_r = 0\) and (F2) \(2 \sum c_r^2 = 3\).

Why \(b^2 = 2\)? The normalization \(b^2 = 2\) is not derived from a dynamical principle — it is the unique positive value for which the Ansatz yields \(Q = 2/3\). For general \(b\), one obtains \(Q = (1 + b^2/2)/3\); setting this equal to \(2/3\) forces \(b^2 = 2\). The physical origin of this constraint is an open question; Sumino [8] proposed a family-gauge mechanism that could protect it against radiative corrections. Throughout this paper, \(b^2 = 2\) is treated as a defining assumption of the Ansatz, not a derived quantity.

2.2 Theorems T1–T4

T4 is the Koide formula in cross-product form: \(Q = M/S^2 = 6a^2/(9a^2) = 2/3\).

2.3 Koide angle (T5)

As a parametric consistency condition, setting \(\theta_0 = 2/(r_{\text{G}_2} \cdot N_{\text{gen}})\) with \(r_{\text{G}_2} = 3\) (squared root-length ratio of the G₂ Lie algebra) and \(N_{\text{gen}} = 3\) yields \(9\theta_0 = 2\), i.e., \(\theta_0 = 2/9 \approx 0.2222\) rad. This coincides with Żenczykowski's lepton phase parameter \(\delta_\ell \approx 2/9\) in the Z₃ parametrization [3, 4] and matches the experimental value from charged lepton masses. We emphasize that this is a definition-level instantiation, not an independent derivation: the G₂ constants are postulated, not derived from dynamics.

---

3. Mass Bounds and Quark Incompatibility

3.1 Cosine and mass-fraction bounds (T6–T9)

From F1 and F2 we derive the algebraic identity \(3(1 - c_0^2) = (c_1 - c_2)^2 \geq 0\), giving \(c_0^2 \leq 1\) (T6). Combined with positivity of \(s_0 = a(1 + bc_0) > 0\), this yields \(c_0 \leq 1\) (T7), hence \(s_0 \leq a(1+b)\) (T8), and finally:

\[6m_0 \leq M(1+b)^2 = M(3 + 2\sqrt{2}) \quad \text{(T9)}\]

The mass-fraction bound \(m_{\max}/M \leq (3 + 2\sqrt{2})/6 \approx 0.9714\) means no single mass can exceed 97.1% of the total.

Numerical check: For charged leptons, \(m_\tau/M \approx 94.5\%\), safely below the bound. For quarks, \(m_t/M \approx 99.3\%\), violating it.

3.2 Quark incompatibility theorem (T10)

If the heaviest mass satisfies \(m_0 > (17 + 12b)(m_1 + m_2)\), then \(6m_0 > M(3 + 2b)\), contradicting T9. The key algebraic identity is

\[(17 + 12b)(3 - 2b) = 3 + 2b \quad \text{when } b^2 = 2,\]

which makes the threshold exact: \(17 + 12\sqrt{2} \approx 33.97\).

Quark masses are \(\overline{\text{MS}}\) values at \(\mu = 2\) GeV from the PDG [2]: \(m_u = 2.16\) MeV, \(m_d = 4.67\) MeV, \(m_s = 93.4\) MeV, \(m_c = 1.27\) GeV, \(m_b = 4.18\) GeV. For the top quark we use the pole mass \(m_t = 172.76\) GeV, which is the PDG convention (a \(\overline{\text{MS}}\) value at 2 GeV is not standard for top). The conclusion is scheme-robust: \(m_t/m_{\text{rest}}\) exceeds the threshold by a factor \(>3\) in any convention, and \(m_b/m_{\text{rest}}\) has a \(>25\%\) margin above 33.97.

---

4. N-Generation Extension

4.1 Generalized Koide Q_N = 2/N (T11–T13)

For the Z_N Ansatz with \(N\) generations, the Fourier identities generalize to \(\sum c_r = 0\) and \(\sum c_r^2 = N/2\). With \(b^2 = 2\):

\[S = Na, \quad M = 2Na^2, \quad Q_N = \frac{M}{S^2} = \frac{2}{N} \quad \text{(T11)}\]

The mass-fraction bound generalizes to \(2N \cdot m_{\max} \leq M(1+b)^2\) (T12), giving \(m_{\max}/M \leq (3 + 2\sqrt{2})/(2N)\).

The threshold reciprocity identity \((3 + 2b)(3 - 2b) = 1\) (T13) explains why the \(N = 3\) threshold is the perfect square \((3 + 2b)^2 = 17 + 12\sqrt{2}\).

4.2 Generation counting and N = 3 optimality

The general threshold theorem (T14): if \(m_0 \cdot (2N - 3 - 2b) > m_{\text{rest}} \cdot (3 + 2b)\), then \(2N \cdot m_0 > M(3 + 2b)\), contradicting T12. The \(N\)-dependent threshold ratio is:

\[T_N = \frac{3 + 2\sqrt{2}}{2N - 3 - 2\sqrt{2}}\]

†For \(N = 4\), the feasible set \(\Theta_4\) degenerates to boundary points (one mass vanishing); for \(N \geq 5\), \(\Theta_N = \emptyset\) and no positive masses exist under the Ansatz. The thresholds listed are formal algebraic bounds that cannot be realized by any valid parameter choice (see Remark below).

\(N = 3\) is the unique integer where the lepton mass hierarchy (\(m_\tau/m_{\text{rest}} \approx 16.7\)) fits within the threshold but the quark hierarchy (\(m_t/m_{\text{rest}} \approx 135.8\)) does not.


For \(N = 4\), the exact threshold is \((23 + 16\sqrt{2})/17 \approx 2.684\) (T15), which excludes even the lepton hierarchy. For \(N = 2\), the bound is vacuous. This suggests that the Koide structure naturally selects three generations of fermions.

Remark (feasibility of the positivity constraint). The Ansatz requires \(1 + b\cos(\theta_0 + 2\pi r/N) > 0\) for all \(r\), which constrains \(\theta_0\) to avoid the arc where \(\cos < -1/b = -1/\sqrt{2}\) (of width \(\pi/2\)). For \(N\) equally spaced points with inter-point gap \(2\pi/N\), the feasible set \(\Theta_N := \{\theta_0 : 1 + b\cos(\theta_0 + 2\pi r/N) > 0 \;\forall r\}\) is non-empty only when \(2\pi/N > \pi/2\), i.e., \(N < 4\). At \(N = 4\) the gap equals the arc width and \(\Theta_4\) degenerates to boundary points (one mass vanishing); for \(N \geq 5\), \(\Theta_N = \emptyset\). Thus \(N = 3\) is distinguished not only by having the largest hierarchy threshold but as the unique \(N\) for which the unsigned Ansatz admits positive masses with non-trivial hierarchy.

---

5. Neutrino Mass Prediction

5.1 Signed-square-root convention and sign uniqueness

In the Z₃ Ansatz, \(s_r = a(1 + bc_r)\) can be negative when \(1 + bc_r < 0\). For physical masses \(m_r = s_r^2 > 0\), this corresponds to a signed square root: \(s_r = \sigma_r \sqrt{m_r}\) with \(\sigma_r \in \{+1, -1\}\). Three neutrinos admit \(2^3 = 8\) sign patterns. The all-positive pattern \((+,+,+)\) gives the standard (unsigned) Koide ratio, which for normal-ordering neutrino masses yields \(Q \neq 2/3\) — the unsigned formula is not satisfied. The all-negative pattern \((-,-,-)\) is equivalent to \((+,+,+)\) by overall sign.

We solve \(Q_{\text{signed}} = \sum m_r / (\sum \sigma_r \sqrt{m_r})^2 = 2/3\) for each of the six remaining sign patterns, checking two consistency conditions: (a) a positive solution \(m_1 > 0\) exists, and (b) the fitted Ansatz parameters satisfy \(|c_r| \leq 1\) for all \(r\) (the cosine bound from T6).

Only \((\sigma_1, \sigma_2, \sigma_3) = (-1, +1, +1)\) — the lightest neutrino carrying the negative sign under normal ordering — yields a solution within the Ansatz bounds. This was first identified by Brannen [6]; we confirm it with updated oscillation data and add the exclusion of all alternatives as a consistency check. The full sign-pattern sweep is implemented in neutrino_check() of the proof file koide_z3_proof.py; for each pattern, the solver either finds no positive root, or the fitted \(|c_r|\) exceeds 1. The Koide constraint \(Q_{\text{signed}} = 2/3\) then becomes a genuine prediction for the absolute mass scale, not a fit selected from a menu.

5.2 Prediction from oscillation data

Using NuFit 6.0 mass-squared differences [7]:

\[\Delta m_{21}^2 = (7.49 \pm 0.18) \times 10^{-5}\;\text{eV}^2, \quad \Delta m_{31}^2 = (2.534 \pm 0.023) \times 10^{-3}\;\text{eV}^2\]

the Koide constraint determines (uncertainties propagated via grid scan over NuFit 1σ/2σ/3σ ranges of \(\Delta m^2\), rounded up to account for correlations). We also report \(|c|_{\max} = \max_r |c_r|\), the largest absolute cosine in the fitted Ansatz; this measures how close the solution is to the structural boundary \(|c_r| = 1\) from T6, with values well below 1 indicating a comfortable fit:


The prediction \(\sum m_\nu = 59.4\) meV is consistent with current bounds (Planck + BAO: \(< 120\) meV [9]; DESI 2024 combined analyses: \(< 72\) meV [10], though this limit is model- and dataset-dependent) and will be testable by next-generation cosmological surveys.

5.3 Inverted ordering

For inverted ordering (IO: \(m_3 < m_1 < m_2\), \(\sigma_3 = -1\)), the same sign-enumeration procedure yields a solution, but with \(|c|_{\max} = 1.000^{+0.003}_{-0.002}\) (central value at NuFit 6.0 best fit, uncertainties from 1σ propagation of \(\Delta m^2\)). The central value sits exactly on the boundary of the allowed cosine range \(|c_r| \leq 1\) (T6). Within the 1σ interval, the upper end exceeds 1, placing IO outside the strict Ansatz domain for a substantial fraction of the parameter space.

IO is not formally excluded — the 1σ lower bound barely reaches \(|c|_{\max} < 1\) — but it is structurally marginal. This provides an independent, parametric argument favoring normal ordering, testable by JUNO. We note that this distinction depends on the current NuFit central values and could shift with future oscillation measurements.

5.4 Comparison with Brannen (2006)

Brannen [6] predicted \(m_1 = 0.383\) meV using the same signed-convention with older oscillation data. Our result (\(m_1 = 0.362\) meV) agrees to within 6%, with the difference arising from updated \(\Delta m^2\) values. The principal advance here is the formal proof infrastructure, error propagation, and the N-generation context showing why the Ansatz works for leptons.

---

6. Discussion

6.1 What is new

Prior work established the algebraic identity \(Q = 2/3\) from the Z₃ Ansatz (folklore; formalized by Żenczykowski [3, 4]). Brannen [6] applied the signed convention to neutrinos. Sumino [8] proposed a family-gauge mechanism. Our contributions:

• Exact incompatibility threshold (T10): The number \(17 + 12\sqrt{2}\) as a sharp algebraic boundary.
• N-generation Koide (T11–T15): The generalization \(Q_N = 2/N\) and the decreasing threshold table.
• Generation counting: \(N = 3\) as the unique generation count compatible with leptons but not quarks.
• Formal verification: First machine-verified Koide treatment, with Lean 4 export.
• Error-propagated neutrino prediction: Systematic error bars from NuFit 6.0.

The companion paper [II] adds quark tuple taxonomy (220 SM triples), \(A_4\) flavor symmetry connection, radiative stability analysis, and Monte Carlo statistical significance.

6.2 Limitations

• The Ansatz is not a dynamical model. The Z₃ parametrization encodes the Koide relation; it does not explain why \(Q = 2/3\). The normalization \(b^2 = 2\) has no known dynamical origin (see §2.1).
• The Koide angle \(\theta_0 = 2/9\) is introduced parametrically; we do not derive it from dynamics.
• The signed-convention \(\sigma_1 = -1\) is selected by the Ansatz consistency check (§5.1), not by an independent physical principle.
• The Ansatz does not constrain PMNS mixing angles (see [II] §7.3 for details).
• The effective masses \(m_\beta\) and \(m_{\beta\beta}\) predicted (\(\approx 8.8\) meV and \(\approx 1.2\)–\(3.9\) meV respectively) are below current experimental sensitivity.
• The "quark incompatibility" (T10) is a property of the parametrization, not a physical exclusion.

6.3 Testable predictions

1. 1. \(\sum m_\nu = 59.4 \pm 0.3\) meV — testable by Euclid, DESI, and CMB-S4.
2. 2. Normal ordering preferred — IO is structurally marginal (\(|c|_{\max} = 1\)); JUNO will determine the ordering.
3. 3. \(m_1 = 0.362 \pm 0.013\) meV — sets the absolute mass scale.

---

Appendix: Proof Infrastructure

All 15 theorems are proved in the formal proof kernel (ProofEnv, strict=True) using the nlinarith tactic backed by Z3 and Wolfram verification. The proof file koide_z3_proof.py contains three ProofEnv instances:

ProofEnv	Theorems	Kernel checks	Debt
build_koide_z3	T1–T9	40/40	0
build_quark_check	T10	8/8	0
build_ngen_koide	T11–T15	26/26	0
Total	15	74/74	0

Lean 4 source files generated from the formal proofs (independent lake build compilation pending):

File	Theorems	Size	Sorry
stamp/Koide_Z3_Ansatz.lean	T1–T9	175 KB	0
stamp/Koide_quark_impossible.lean	T10	150 KB	0
stamp/Koide_Ngen.lean	T11–T15	16 KB	0

Note on axioms: The formal proof kernel reports zero user axioms (all hypotheses are explicit parameters, not postulated). The exported Lean 4 files declare variables and hypotheses as Lean axiom lines — these encode the mathematical setup (e.g., \(b^2 = 2\), Fourier identities), not unproved claims.

---

Declaration of Generative AI Use

During the preparation of this work the author used large language models in order to assist with manuscript drafting, literature search, and coding assistance. After using these tools, the author reviewed and edited the content as needed and takes full responsibility for the content of the published article.

---

References

[1] Y. Koide, "New view of quark and lepton mass hierarchy," Phys. Rev. D 28, 252 (1983).

[2] Particle Data Group, "Review of Particle Physics," Phys. Rev. D 110, 030001 (2024).

[3] P. Żenczykowski, "Remark on Koide's Z₃-symmetric parametrization of quark masses," Phys. Rev. D 86, 117303 (2012). arXiv:1210.4125.

[4] P. Żenczykowski, "Koide's Z₃-symmetric parametrization, quark masses and mixings," arXiv:1301.4143 (2013).

[5] T. Nagy, "The formal proof kernel: a formally verified proof environment for real arithmetic," (2026). [Companion paper in preparation.]

[6] C. Brannen, "The lepton masses," unpublished manuscript (2006). Available at https://brannenworks.com/MASSES2.pdf.

[7] I. Esteban, M. C. Gonzalez-Garcia, M. Maltoni, I. Martinez-Soler, J. P. Pinheiro, and T. Schwetz, "NuFit-6.0: Updated global analysis of three-flavor neutrino oscillations," JHEP 12, 216 (2024). arXiv:2410.05380.

[8] Y. Sumino, "Family gauge symmetry as an origin of Koide's mass formula and charged lepton spectrum," JHEP 05, 075 (2009). arXiv:0812.2103.

[9] Planck Collaboration, "Planck 2018 results. VI. Cosmological parameters," Astron. Astrophys. 641, A6 (2020). arXiv:1807.06209.

[10] DESI Collaboration, "DESI 2024 VI: Cosmological constraints from the measurements of baryon acoustic oscillations," arXiv:2404.03002 (2024).

[11] R. Foot, "A note on Koide's lepton mass relation," arXiv:hep-ph/9402242 (1994).

[12] A. Rivero and A. Gsponer, "The strange formula of Dr. Koide," arXiv:hep-ph/0505220 (2005).

[13] A. Kartavtsev, "A remark on the Koide relation for quarks," arXiv:1111.4524 (2011).

[II] T. Nagy, "Near-Koide structure across the Standard Model fermion spectrum," (2026). DOI: 10.5281/zenodo.19698028.