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

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 Platonic 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.