The sharp reciprocal bound for hyperbolic triples

For natural numbers a, b, c ≥ 2 with 1/a + 1/b + 1/c < 1, the deficit 1 - 1/a - 1/b - 1/c is at least 1/42, attained at (2, 3, 7). Applied to ramification indices, this is the numerical part of Hurwitz's sharp 84(g - 1) bound for finite automorphism groups.

The result is stated for arbitrary orders of the three indices.

Reference

H. Stichtenoth, Algebraic Function Fields and Codes, second edition, Exercise 3.18.

theorem TauCeti.one_div_forty_two_le_hyperbolic_triangle_deficit {a b c : ℕ} (ha : 2 ≤ a) (hb : 2 ≤ b) (hc : 2 ≤ c) (hhyper : 1 / ↑a + 1 / ↑b + 1 / ↑c < 1) : 1 / 42 ≤ 1 - 1 / ↑a - 1 / ↑b - 1 / ↑c

The sharp numerical bound for a hyperbolic triple of natural numbers. The equality case is realized by the indices (2, 3, 7).

theorem TauCeti.two_three_seven_deficit_eq_one_div_forty_two : 1 - 1 / 2 - 1 / 3 - 1 / 7 = 1 / 42

The triangle indices (2, 3, 7) attain the bound.