A parameter-free prediction of the tau-lepton mass, kernel-verified in Lean 4

This paper predicts the tau-lepton mass with no adjustable parameter: 1776.98497 MeV, using the measured electron mass solely to set the mass scale. Neither the muon nor the tau mass is used to fit the prediction. The prediction provides a precise target for future measurements. The Particle Data Group world average is 1776.93 ± 0.09 MeV, approximately 0.61 standard deviations below it. If that central value persists, a future determination with total standard uncertainty of 0.02 MeV would differ from the prediction by approximately 2.75σ; at 0.01 MeV, the difference would reach 5.5σ. The manuscript states the comparison procedure and rejection criterion in advance. [PDG tau-lepton listing](https://pdglive.lbl.gov/Particle.action?node=S035). Measurements in progress will sharpen the comparison: BESIII's April 2018 threshold scan is expected to reach an uncertainty below 0.1 MeV, and Belle II's pseudomass measurement (1777.09 ± 0.08 ± 0.11 MeV from 190 fb⁻¹) will be refined by its larger dataset; at the 0.1 MeV level the present central value would sit 0.55σ from the prediction. The construction builds on the phase derivation in [Observer-Rooted Asymmetry](https://doi.org/10.5281/zenodo.21729600) and [Unifying Aperture](https://doi.org/10.5281/zenodo.18067098). A three-register ledger fixes the aperture at 2/3, leading to a 3 × 3 Hermitian operator with spectrum λₖ = 1 + √2 cos(2/9 + 2πk/3), for k = 0, 1, 2. The squared spectral values determine two mass ratios. The middle ratio fixes the completed count at 206. Two supports of 206 elements, sharing three roles, produce a screen of 409 elements. Its derived regular-polygon geometry supplies a chord-to-arc correction to the middle weight while preserving the tau-to-electron ratio. The certified numerical bounds are: * Muon-to-electron ratio: mμ/me ∈ [206.7682815, 206.768283].* Tau-to-electron ratio: mτ/me ∈ [3477.4728176, 3477.4728372]. The measured muon-to-electron central value lies inside the first interval; the evaluated prediction differs from it by approximately 0.007 standard uncertainties. These intervals are mathematical bounds on the calculated ratios, distinct from experimental uncertainty. Koide's relation follows as a corollary for the unscreened weights and is not used as an input. The accompanying Lean 4 development contains 2,387 kernel-checked theorems, with no placeholder proofs or user-declared axioms. Their axiom dependencies are confined to propositional extensionality, choice and quotient soundness. The certification covers the stated spectrum, representation, contraction, readout and screen results, together with the numerical enclosures. The manuscript identifies the earlier source derivations it imports and the precise scope of formal verification. The certified development is deposited at 10.5281/zenodo.22801617.