{"id":"palomar/PALOMAR-2026-09-17-000006","url":"https://github.com/blawton/fried-conj-lean/tree/610d659ea15af869553f6e3e79c432880d9b0ab0","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-17-000006-v1.json","repo":"https://github.com/blawton/fried-conj-lean","tags":["math.DS","math.SP","msc:37C30","msc:37D20","msc:58J52","msc:57Q10","dynamical-systems","spectral-geometry","ruelle-resonances","lean-formalization"],"score":0,"title":"Resonance-cluster analysis for a proposed counterexample to Fried's conjecture","trust":"high","domain":"math.DS","source":"palomar","authors":["Benjamin Lawton"],"reviews":0,"subject":"math.DS","summary":"A Lean 4 formalization of the theorem FriedCrossing.fried_counterexample_of_resolvent_inputs, the machine-checked reduction behind a proposed codimension-one failure of Fried's identity ζ(0) = τ_R for acyclic characters on a closed hyperbolic 3-manifold with b₁ = 1. For a simple illustration of the method with figures, see docs/counterexample_intuitive_view.pdf. The Mechanism: Near (g_hyp, ρ_triv), along the conformal family g_τ = e^{−2τb}g_hyp with characters χ_θ, the Ruelle resonances near 0 form two small clusters: a rank-2 cluster in degree 1, encoded by a 2×2 matrix M(θ,τ), and a rank-4…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-17","reactions":{},"formalized":true}