A conjecture of Erdős, supersingular primes and short character sums

Problem statement

Notes: Unavailable.

Source: M. Bennett and S. Siksek, `A conjecture of Erdős, supersingular primes and short character sums`, Annals of Math, 191 (2) 2020. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2020-191-2-ErdosSupersingularPrimes.lean

Informal solution: Unavailable.

/-- The absolute constant such that for all `k ≥ k₀`, the theorem holds.

Part of the theorem statement is that `k₀` should be "effectively computable".
In principle, this means that the definition of `k₀` should avoid `Classical.choice`.
Unfortunately, this is not currently enforceable in Comparator.
Note that prohibiting `noncomputable` is not sufficient:
https://leanprover.zulipchat.com/#narrow/channel/583341-Model-comparisons-for-Lean/topic/LeanEval/near/598595369 -/
def declaration uses `sorry`k₀ : ℕ := sorry

/--
Statement of Theorem 2:

There is an effectively computable absolute constant `k₀` such
that if `k ≥ k₀` is a positive integer, then any `Solution` with prime exponent `l` satisfies
either `y = 0` or `d = 0` or `l ≤ exp(10 ^ k)`.
-/
theorem declaration uses `sorry`theorem_2 (k : ℕ) (hk : k ≥ k₀) (s : Solution k) (hs : s.l.Prime) :
    s.y = 0 ∨ s.d = 0 ∨ s.l ≤ exp (10 ^ k) := byk:ℕhk:k ≥ k₀s:Solution khs:Nat.Prime s.l⊢ s.y = 0 ∨ s.d = 0 ∨ ↑s.l ≤ rexp (10 ^ k)
  sorryAll goals completed! 🐙