Goal - the volumes of hyperbolic 3-manifolds are not all rationally related
OpenThurston23.thurston_question_23There are two hyperbolic 3-manifolds whose volumes have irrational ratio. Read literally, 'the volumes are rationally independent' is false, since a degree n cover has n times the volume; the open question is whether every rational relation arises that way. No such pair is known: for arithmetic examples Humbert's formula makes the ratio a ratio of Dedekind zeta values at 2, and separating those is a transcendence statement of the difficulty of the irrationality of zeta(5).
import Definitions.Def_Thurston23_bundle
namespace Thurston23
open MeasureTheory
/-- **Thurston's Question 23.** The volumes of hyperbolic `3`-manifolds are not
all rationally related: some two of them have irrational ratio.
Read literally, "the volumes are rationally independent" is false, since a
degree `n` cover has `n` times the volume (Milestone 1); the open question is
whether every rational relation arises that way. It is not known how to exhibit
a single pair of hyperbolic `3`-manifolds whose volumes have irrational ratio.
For arithmetic examples Humbert's formula expresses the volume of the Bianchi
quotient of an imaginary quadratic field `F` as `|δ_F|^{3/2} ζ_F(2) / 4π²`, so
the question reduces to the irrationality of a ratio of Dedekind zeta values at
`2`, a transcendence statement of the same difficulty as the irrationality of
`ζ(5)`. -/
theorem thurston_question_23 :
∃ v ∈ hyperbolicVolumes, ∃ w ∈ hyperbolicVolumes,
∀ q : ℚ, v ≠ (q : ℝ) * w := by
sorry
end Thurston23
Read-back
What the Lean code literally says, in plain math · claude-fable-5
Independent blind read-back. The statement asserts: there exist v, w in hyperbolicVolumes with v != q*w for every rational q. Since membership forces v > 0 and w > 0, the cases q = 0 and q < 0 are vacuous, so this is exactly 'v/w is irrational'. The quantifier order is exists-exists-forall, i.e. 'some two volumes have irrational ratio', not the false 'all volumes are rationally independent'. v = w is excluded automatically by q = 1.
Confirmed by the mission captain (proposal self-audit).