Prove2Me

The volume of the box over the rhombus is −∫0π/6log⁡(1−14cos⁡2θ) dθ-\int_0^{\pi/6} \log\bigl(1 - \tfrac{1}{4\cos^2\theta}\bigr)\,d\theta

Proved
Thurston23.hvol_eisBox_eq_ofReal_integral

by t4v1 · Sep 14, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

hyperbolic-geometrykleinian-groupsthurston-question-23

The hyperbolic volume ∫Bt−3 dx dy dt\int_B t^{-3}\,dx\,dy\,dt of the box B={0≤x≤12, 0≤x+3 y≤1, x2+y2+t2≥1}B = \{0 \le x \le \tfrac12,\ 0 \le x + \sqrt3\,y \le 1,\ x^2+y^2+t^2 \ge 1\} equals

−∫0π/6log⁡(1−14cos⁡2θ) dθ,-\int_0^{\pi/6} \log\Bigl(1 - \frac{1}{4\cos^2\theta}\Bigr)\,d\theta,

stated in [0,∞][0,\infty] through ENNReal.ofReal. The height integral reduces the volume to ∫dx dy/(2(1−x2−y2))\int dx\,dy/(2(1 - x^2 - y^2)) over the rhombus; in polar coordinates the rhombus is θ∈[−π/6,π/2]\theta \in [-\pi/6, \pi/2], r≤1/(2max⁡(cos⁡θ,cos⁡(θ−π/3)))r \le 1/(2\max(\cos\theta, \cos(\theta - \pi/3))), the radial integral is −14log⁡(1−r2)-\tfrac14\log(1 - r^2), and the angle folds onto [0,π/6][0, \pi/6]. The integral evaluates to −3 L(2,χ−3)/8-\sqrt3\,L(2,\chi_{-3})/8 (a separate, Mathlib-only statement), which is Humbert's formula for Q(−3)\mathbb{Q}(\sqrt{-3}).

Preamble
import Definitions.Def_Thurston23_eisenstein
Formal statement
namespace Thurston23

open MeasureTheory

theorem hvol_eisBox_eq_ofReal_integral :
    hvol eisBox = ENNReal.ofReal
      (-∫ θ in (0:ℝ)..Real.pi / 6, Real.log (1 - 1 / (4 * Real.cos θ ^ 2))) := by
  sorry

end Thurston23
Source
W. P. Thurston, Three-dimensional manifolds, Kleinian groups and hyperbolic geometry, Bull. Amer. Math. Soc. 6 (1982), 357-381, Question 23 (p. 380). J. Elstrodt, F. Grunewald, J. Mennicke, Groups Acting on Hyperbolic Space, Springer 1998, Chapter 7 (Bianchi groups and Humbert's formula). Formalisation: https://github.com/t4v1/thurston23/blob/main/Thurston23Eisenstein.lean (hvol_eisBox_eq_ofReal_integral).

View graph