Cost Trace Rational Exponent Six Exponentials Trace Input

/-- The six exponentials input, in exactly the form the classification uses: if the trace
of `n^c` is rational at the three bases two, three and five, the exponent is rational.
This is a published corollary of the six exponentials theorem (Lang, Ramachandra) and is
stated as a hypothesis because the ambient library carries neither it nor
Gelfond--Schneider. -/
def SixExponentialsTraceInput : Prop :=
  ∀ c : ℝ, (∀ n : ℕ, 2 ≤ n → n ≤ 5 →
      ∃ t : ℚ, ((n : ℝ)) ^ c + (((n : ℝ)) ^ c)⁻¹ = (t : ℝ)) →
    ∃ r : ℚ, c = (r : ℝ)

/-- **A rational trace plus any rational power forces rationality.** If `u > 1` has a
rational trace and some positive power of `u` is rational, then `u` is rational.

This is what makes the trace formulation tractable: a genuinely quadratic unit can never
have a rational power. -/
theorem rat_of_trace_rat_of_pow_rat {u : ℝ} (hu : 1 < u) {t : ℚ}
    (ht : u + u⁻¹ = (t : ℝ)) {q : ℕ} (hq : 1 ≤ q) {A : ℚ}
    (hA : u ^ q = (A : ℝ)) :
    ∃ r : ℚ, u = (r : ℝ) := by
  obtain ⟨a, b, ha, hb, hab⟩ := pow_eq_coords hu ht q hq
  have hbne' : ((b : ℝ)) ≠ 0 := by
    simpa using (ne_of_gt hb : b ≠ 0)
  have hval : (A : ℝ) = (a : ℝ) + (b : ℝ) * (u - u⁻¹) := by rw [← hA, hab]
  have hd : u - u⁻¹ = ((A : ℝ) - (a : ℝ)) / (b : ℝ) := by
    rw [eq_div_iff hbne']
    linear_combination -hval
  refine ⟨(t + (A - a) / b) / 2, ?_⟩
  push_cast
  rw [← hd, ← ht]
  ring

/-- **A positive rational exponent with a rational trace is an integer.** If `c` is a
positive rational and `2^c + 2^(-c)` is rational, then `c` has denominator one.

Together with the six exponentials theorem, which rules out irrational `c`, this is the
whole exponent step of the gauge classification. Note what it never assumes: `2^c` is
not required to be rational, only its trace, which is exactly the weakening that
`no_rational_character_at_trace_three` shows to be necessary. -/
theorem int_of_rat_exponent_of_trace_rat {c : ℚ} (hc : 0 < c) {t : ℚ}
    (ht : (2 : ℝ) ^ (c : ℝ) + ((2 : ℝ) ^ (c : ℝ))⁻¹ = (t : ℝ)) :
    c.den = 1 := by
  haveI : Fact (Nat.Prime 2) := ⟨Nat.prime_two⟩
  have hu1 : 1 < (2 : ℝ) ^ (c : ℝ) := by
    have h0 : (2 : ℝ) ^ (0 : ℝ) < (2 : ℝ) ^ (c : ℝ) := by
      apply (Real.rpow_lt_rpow_left_iff (by norm_num)).mpr
      exact_mod_cast hc
    rwa [Real.rpow_zero] at h0
  have hnum : 0 < c.num := Rat.num_pos.mpr hc
  have hpR : ((c.num.toNat : ℕ) : ℝ) = ((c.num : ℤ) : ℝ) := by
    exact_mod_cast congrArg (fun z : ℤ => (z : ℝ)) (Int.toNat_of_nonneg (le_of_lt hnum))
  have hcq : (c : ℝ) * ((c.den : ℕ) : ℝ) = ((c.num.toNat : ℕ) : ℝ) := by
    rw [hpR]
    exact_mod_cast congrArg (fun x : ℚ => (x : ℝ)) (Rat.mul_den_eq_num c)
  have hpow : ((2 : ℝ) ^ (c : ℝ)) ^ (c.den) = (((2 : ℚ) ^ (c.num.toNat) : ℚ) : ℝ) := by
    rw [← Real.rpow_natCast ((2 : ℝ) ^ (c : ℝ)) c.den, ← Real.rpow_mul (by norm_num), hcq,
      Real.rpow_natCast]
    push_cast
    ring
  obtain ⟨r, hr⟩ := rat_of_trace_rat_of_pow_rat hu1 ht c.pos hpow
  have hrq : r ^ (c.den) = (2 : ℚ) ^ (c.num.toNat) := by
    have h : ((r ^ (c.den) : ℚ) : ℝ) = (((2 : ℚ) ^ (c.num.toNat) : ℚ) : ℝ) := by
      rw [← hpow, hr]; push_cast; ring
    exact_mod_cast h
  have hrne : r ≠ 0 := by
    intro h
    rw [h, zero_pow (by have := c.pos; omega : c.den ≠ 0)] at hrq
    have hp : (0 : ℚ) < (2 : ℚ) ^ (c.num.toNat) := by positivity
    rw [← hrq] at hp
    exact lt_irrefl _ hp
  have hv1 : padicValRat 2 (r ^ (c.den)) = (c.den : ℕ) * padicValRat 2 r :=
    padicValRat.pow hrne
  have hself : padicValRat 2 ((2 : ℚ)) = 1 := by
    have h := padicValRat.self (p := 2) (by norm_num)
    norm_num at h
    exact h
  have hv2 : padicValRat 2 ((2 : ℚ) ^ (c.num.toNat)) = (c.num.toNat : ℕ) * 1 := by
    rw [padicValRat.pow (by norm_num : (2 : ℚ) ≠ 0), hself]
  rw [hrq, hv2] at hv1
  have hdvd : c.den ∣ c.num.toNat := by
    have hz : ((c.den : ℕ) : ℤ) ∣ ((c.num.toNat : ℕ) : ℤ) :=
      ⟨padicValRat 2 r, by push_cast at hv1 ⊢; linarith⟩
    exact_mod_cast hz
  have hpabs : c.num.toNat = c.num.natAbs := by
    have h1 : ((c.num.toNat : ℕ) : ℤ) = c.num := Int.toNat_of_nonneg (le_of_lt hnum)
    have h2 : ((c.num.natAbs : ℕ) : ℤ) = c.num := Int.natAbs_of_nonneg (le_of_lt hnum)
    omega
  have hcop : Nat.gcd c.num.toNat c.den = 1 := by
    rw [hpabs]; exact c.reduced
  exact Nat.dvd_one.mp (hcop ▸ Nat.dvd_gcd hdvd dvd_rfl)

/-- **The exponent is a positive integer.** Given the imported six exponentials input, a
positive real exponent whose traces at the small bases are rational is a positive integer.
It is not further restricted to the odd integers: both parities are inhabited, by
`Cost.GaugeOrbitFromRealCharacter.signedPowerNativeCost_sansAnchor`. This is the arithmetic
half of `GaugeOrbitIsSignedPowerFamily_of_sixExponentials`; the analytic half is Howe. -/
theorem exponent_is_positive_integer (hsix : SixExponentialsTraceInput)
    {c : ℝ} (hc : 0 < c)
    (htrace : ∀ n : ℕ, 2 ≤ n → n ≤ 5 →
      ∃ t : ℚ, ((n : ℝ)) ^ c + (((n : ℝ)) ^ c)⁻¹ = (t : ℝ)) :
    ∃ k : ℕ, 1 ≤ k ∧ c = (k : ℝ) := by
  obtain ⟨r, hr⟩ := hsix c htrace
  have hrpos : 0 < r := by
    have h : (0 : ℝ) < (r : ℝ) := hr ▸ hc
    exact_mod_cast h
  obtain ⟨t, ht⟩ := htrace 2 (by norm_num) (by norm_num)
  have ht' : (2 : ℝ) ^ ((r : ℚ) : ℝ) + ((2 : ℝ) ^ ((r : ℚ) : ℝ))⁻¹ = (t : ℝ) := by
    rw [← hr]
    norm_num at ht ⊢
    exact ht
  have hden : r.den = 1 := int_of_rat_exponent_of_trace_rat hrpos ht'
  have hnum : 0 < r.num := Rat.num_pos.mpr hrpos
  refine ⟨r.num.toNat, by omega, ?_⟩
  have hrn : ((r.num : ℤ) : ℚ) = r := by
    conv_rhs => rw [← Rat.num_div_den r]
    rw [hden]
    norm_num
  have hfin : ((r.num.toNat : ℕ) : ℚ) = r := by
    rw [show ((r.num.toNat : ℕ) : ℚ) = ((r.num.toNat : ℕ) : ℤ) by push_cast; ring,
      Int.toNat_of_nonneg (le_of_lt hnum)]
    exact hrn
  rw [hr]
  exact_mod_cast congrArg (fun x : ℚ => (x : ℝ)) hfin.symm