feat: add Martinet totally-real towers eval problem

LeanEval/NumberTheory/MartinetTowers.lean

@@ -0,0 +1,37 @@
+import Mathlib.NumberTheory.NumberField.Discriminant.Defs
+import Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
+import EvalTools.Markers
+
+/-!
+# Martinet's totally real class-field towers
+
+Jacques Martinet's construction of a totally real number field with an infinite unramified
+2-class-field tower gives an infinite family of totally real number fields of unbounded degree and
+bounded root discriminant. This is the benchmark statement corresponding to the classical input
+used in the formalization of the real sum-product counterexample.
+
+Assuming Martinet's Proposition 4.1 and Example 4.2: there is a totally real degree-four field
+`k'` with an infinite unramified 2-class-field tower and root discriminant
+`ρ = 4 * sqrt (3 * 5 * 7 * 23 * 29) < 1059`. Finite layers `K / k'` in the tower have unbounded
+degrees, remain totally real, and are unramified at finite primes, so
+`|discr K| = |discr k'| ^ [K : k'] = ρ ^ [K : ℚ]`. Hence `C = ρ` works.
+
+Reference: Jacques Martinet, *Tours de corps de classes et estimations de discriminants*,
+Inventiones Mathematicae 44 (1978), 65--73, especially §4, Proposition 4.1 and Example 4.2.
+-/
+
+namespace LeanEval.NumberTheory
+
+/-- Martinet's bounded-root-discriminant theorem for totally real fields.
+
+There is an absolute constant `C > 0` such that for arbitrarily large degrees `d` there exists a
+totally real number field `K / ℚ` of degree `d` whose discriminant satisfies `|Δ_K| ≤ C ^ d`.
+-/
+@[eval_problem]
+theorem martinet_totally_real_towers :
+    ∃ C : ℝ, 0 < C ∧ ∀ N : ℕ, ∃ d : ℕ, N ≤ d ∧
+      ∃ (K : Type) (_ : Field K) (_ : NumberField K) (_ : NumberField.IsTotallyReal K),
+        Module.finrank ℚ K = d ∧ |(NumberField.discr K : ℝ)| ≤ C ^ d := by
+  sorry
+
+end LeanEval.NumberTheory

manifests/problems/martinet_totally_real_towers.toml

@@ -0,0 +1,9 @@
+id = "martinet_totally_real_towers"
+title = "Martinet's totally real class-field towers"
+test = false
+module = "LeanEval.NumberTheory.MartinetTowers"
+holes = ["martinet_totally_real_towers"]
+submitter = "Adam Topaz"
+source = "Jacques Martinet, *Tours de corps de classes et estimations de discriminants*, Invent. Math. 44 (1978), 65--73. DOI: 10.1007/BF01389902."
+notes = "The Lean statement is Martinet's bounded-root-discriminant theorem for totally real class-field towers."
+informal_solution = "By Proposition 4.1 and Example 4.2, Martinet constructs a totally real degree-four field k' with an infinite unramified 2-class-field tower and root discriminant rho = 4 sqrt(3*5*7*23*29) < 1059. Finite tower layers K/k' remain totally real and have unbounded degrees; since they are unramified at finite primes, |D_K| = |D_k'|^[K:k'] = rho^[K:Q]. Thus C = rho works."