IndisputableMonolith.Cost.TraceRationalExponent

   1/-
   2# The exponent is an integer, and why the character was never rational
   3
   4This module supplies the arithmetic core of the anchor-free gauge classification, and
   5corrects a structural mistake in how that classification has been attacked.
   6
   7## The mistake
   8
   9The program has been trying to prove that every inhabitant of the anchor-free cost
  10ledger factors through a character valued **in the carrier**, that is, a rational-valued
  11completely multiplicative function. That target is stronger than the mathematics
  12supports, which is why it has resisted and why its unrestricted form is refuted.
  13
  14Solving the composition law by the d'Alembert route gives `F = J ∘ χ`, and the quantity
  15a cost actually exposes is the trace `χ(x) + χ(x)⁻¹`. A cost is carrier-valued exactly
  16when its **traces** are rational. It does not follow that `χ` is rational.
  17`no_rational_character_at_trace_three` makes the gap concrete: the trace equation with
  18value `3` has no rational solution at all, so a cost charging `1/2` at the ratio two is
  19perfectly carrier-valued while having no rational character behind it.
  20
  21## What replaces it
  22
  23Work with the trace. Writing `χ(n) = n^c`, carrier-valuedness says `n^c + n^(-c)` is
  24rational for every `n`, which is strictly weaker than `n^c` rational. The classification
  25then needs only that `c` is an odd positive integer, and the arithmetic of that is here:
  26
  27* `rat_of_trace_rat_of_pow_rat`: a real above one with rational trace that has **some**
  28  rational power is itself rational. The proof writes `u^k = a + b·(u - u⁻¹)` with `a`
  29  and `b` positive rationals, so the irrational part can never cancel.
  30* `int_of_rat_exponent_of_trace_rat`: a positive rational exponent whose trace at base
  31  two is rational is an integer.
  32
  33One input stays outside Lean and is named rather than hidden, since Mathlib does not carry
  34it: the six exponentials theorem, which rules out irrational exponents.
  35`exponent_is_positive_integer` packages the chain so that what is imported is visible in
  36the statement.
  37
  38There used to be a second import, the Erdős power-function step for monotone completely
  39multiplicative functions. It is now a theorem, `Cost.MonotonePower.exists_exponent`, proved
  40by Howe's elementary argument, and the classification that consumes both
  41(`Cost.GaugeOrbitClassification.GaugeOrbitIsSignedPowerFamily_of_sixExponentials`) now runs
  42on the six exponentials input alone.
  43-/
  44
  45import Mathlib
  46
  47namespace IndisputableMonolith
  48namespace Cost
  49namespace TraceRationalExponent
  50
  51/-! ## A rational trace need not come from a rational character -/
  52
  53/-- No rational number squares to five. Proved by counting the five-adic valuation:
  54a square has even valuation and five has valuation one. -/
  55theorem no_rational_sqrt_five : ¬ ∃ s : ℚ, s ^ 2 = 5 := by
  56  haveI : Fact (Nat.Prime 5) := ⟨by norm_num⟩
  57  rintro ⟨s, hs⟩
  58  have hs0 : s ≠ 0 := by
  59    intro h
  60    rw [h] at hs
  61    norm_num at hs
  62  have h1 : padicValRat 5 (s ^ 2) = (2 : ℕ) * padicValRat 5 s :=
  63    padicValRat.pow hs0
  64  have h2 : padicValRat 5 ((5 : ℕ) : ℚ) = 1 := padicValRat.self (by norm_num)
  65  rw [hs] at h1
  66  norm_num at h2
  67  rw [h2] at h1
  68  omega
  69
  70/-- **The demand for a carrier-valued character is too strong.** The trace equation
  71`r + r⁻¹ = 3` has no rational solution. So a cost whose value at the ratio two is the
  72perfectly rational `1/2` has no rational character at that ratio, and asking the
  73factorization to produce one asks for something that does not exist. -/
  74theorem no_rational_character_at_trace_three : ¬ ∃ r : ℚ, r + r⁻¹ = 3 := by
  75  rintro ⟨r, hr⟩
  76  have hr0 : r ≠ 0 := by
  77    intro h
  78    rw [h] at hr
  79    norm_num at hr
  80  have hquad : r ^ 2 - 3 * r + 1 = 0 := by
  81    field_simp at hr
  82    linarith [hr]
  83  exact no_rational_sqrt_five ⟨2 * r - 3, by nlinarith [hquad]⟩
  84
  85/-- The real witness behind the previous theorem, recorded so the object is on the page:
  86the square of the golden ratio has trace exactly three. -/
  87theorem golden_square_has_trace_three :
  88    ((3 + Real.sqrt 5) / 2) + ((3 + Real.sqrt 5) / 2)⁻¹ = 3 := by
  89  have hsq : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt (by norm_num)
  90  have hnn : (0 : ℝ) ≤ Real.sqrt 5 := Real.sqrt_nonneg 5
  91  have hne : (3 + Real.sqrt 5) / 2 ≠ 0 := by positivity
  92  field_simp
  93  nlinarith [hsq, hnn]
  94
  95/-! ## The arithmetic core
  96
  97A real above one with a rational trace generates a quadratic object. If any power of it
  98lands back in the rationals, the irrational part has to cancel, and it cannot, because
  99its coefficient is a strictly positive rational at every step. -/
 100
 101/-- Powers of `u` on the basis `{1, d}` with `d = u - u⁻¹`, both coordinates strictly
 102positive rationals. The positivity of the second coordinate is the whole point: it is
 103what forbids the irrational part from cancelling. -/
 104private theorem pow_eq_coords {u : ℝ} (hu : 1 < u) {t : ℚ}
 105    (ht : u + u⁻¹ = (t : ℝ)) :
 106    ∀ k : ℕ, 1 ≤ k → ∃ a b : ℚ, 0 < a ∧ 0 < b ∧
 107      u ^ k = (a : ℝ) + (b : ℝ) * (u - u⁻¹) := by
 108  have hupos : (0 : ℝ) < u := lt_trans zero_lt_one hu
 109  have hu0 : u ≠ 0 := ne_of_gt hupos
 110  have htgt : (2 : ℝ) < (t : ℝ) := by
 111    rw [← ht]
 112    have hsq : (0 : ℝ) < (u - 1) ^ 2 := by nlinarith
 113    have hpos : (0 : ℝ) < (u - 1) ^ 2 / u := div_pos hsq hupos
 114    have hid : u + u⁻¹ - 2 = (u - 1) ^ 2 / u := by field_simp; ring
 115    linarith
 116  have htq : (2 : ℚ) < t := by exact_mod_cast htgt
 117  obtain ⟨d, hddef⟩ : ∃ d : ℝ, d = u - u⁻¹ := ⟨_, rfl⟩
 118  have hbase : u = (t : ℝ) / 2 + d / 2 := by
 119    rw [hddef, ← ht]; ring
 120  have hd2 : d ^ 2 = (t : ℝ) ^ 2 - 4 := by
 121    rw [hddef, ← ht]
 122    field_simp
 123    ring
 124  intro k hk
 125  rw [← hddef]
 126  induction k with
 127  | zero => omega
 128  | succ n ih =>
 129      rcases Nat.eq_or_lt_of_le hk with h1 | h1
 130      · refine ⟨t / 2, 1 / 2, by linarith, by norm_num, ?_⟩
 131        have hn0 : n = 0 := by omega
 132        subst hn0
 133        rw [pow_one]
 134        push_cast
 135        linarith [hbase]
 136      · have hn : 1 ≤ n := by omega
 137        obtain ⟨a, b, ha, hb, hab⟩ := ih hn
 138        have h4 : (0 : ℚ) < t ^ 2 - 4 := by nlinarith
 139        refine ⟨a * (t / 2) + b * (1 / 2) * (t ^ 2 - 4),
 140                a * (1 / 2) + b * (t / 2), by positivity, by positivity, ?_⟩
 141        rw [pow_succ, hab]
 142        push_cast
 143        linear_combination ((a : ℝ) + (b : ℝ) * d) * hbase + ((b : ℝ) / 2) * hd2
 144
 145/-- **A rational trace plus any rational power forces rationality.** If `u > 1` has a
 146rational trace and some positive power of `u` is rational, then `u` is rational.
 147
 148This is what makes the trace formulation tractable: a genuinely quadratic unit can never
 149have a rational power. -/
 150theorem rat_of_trace_rat_of_pow_rat {u : ℝ} (hu : 1 < u) {t : ℚ}
 151    (ht : u + u⁻¹ = (t : ℝ)) {q : ℕ} (hq : 1 ≤ q) {A : ℚ}
 152    (hA : u ^ q = (A : ℝ)) :
 153    ∃ r : ℚ, u = (r : ℝ) := by
 154  obtain ⟨a, b, ha, hb, hab⟩ := pow_eq_coords hu ht q hq
 155  have hbne' : ((b : ℝ)) ≠ 0 := by
 156    simpa using (ne_of_gt hb : b ≠ 0)
 157  have hval : (A : ℝ) = (a : ℝ) + (b : ℝ) * (u - u⁻¹) := by rw [← hA, hab]
 158  have hd : u - u⁻¹ = ((A : ℝ) - (a : ℝ)) / (b : ℝ) := by
 159    rw [eq_div_iff hbne']
 160    linear_combination -hval
 161  refine ⟨(t + (A - a) / b) / 2, ?_⟩
 162  push_cast
 163  rw [← hd, ← ht]
 164  ring
 165
 166/-! ## The exponent is an integer -/
 167
 168/-- **A positive rational exponent with a rational trace is an integer.** If `c` is a
 169positive rational and `2^c + 2^(-c)` is rational, then `c` has denominator one.
 170
 171Together with the six exponentials theorem, which rules out irrational `c`, this is the
 172whole exponent step of the gauge classification. Note what it never assumes: `2^c` is
 173not required to be rational, only its trace, which is exactly the weakening that
 174`no_rational_character_at_trace_three` shows to be necessary. -/
 175theorem int_of_rat_exponent_of_trace_rat {c : ℚ} (hc : 0 < c) {t : ℚ}
 176    (ht : (2 : ℝ) ^ (c : ℝ) + ((2 : ℝ) ^ (c : ℝ))⁻¹ = (t : ℝ)) :
 177    c.den = 1 := by
 178  haveI : Fact (Nat.Prime 2) := ⟨Nat.prime_two⟩
 179  have hu1 : 1 < (2 : ℝ) ^ (c : ℝ) := by
 180    have h0 : (2 : ℝ) ^ (0 : ℝ) < (2 : ℝ) ^ (c : ℝ) := by
 181      apply (Real.rpow_lt_rpow_left_iff (by norm_num)).mpr
 182      exact_mod_cast hc
 183    rwa [Real.rpow_zero] at h0
 184  have hnum : 0 < c.num := Rat.num_pos.mpr hc
 185  have hpR : ((c.num.toNat : ℕ) : ℝ) = ((c.num : ℤ) : ℝ) := by
 186    exact_mod_cast congrArg (fun z : ℤ => (z : ℝ)) (Int.toNat_of_nonneg (le_of_lt hnum))
 187  have hcq : (c : ℝ) * ((c.den : ℕ) : ℝ) = ((c.num.toNat : ℕ) : ℝ) := by
 188    rw [hpR]
 189    exact_mod_cast congrArg (fun x : ℚ => (x : ℝ)) (Rat.mul_den_eq_num c)
 190  have hpow : ((2 : ℝ) ^ (c : ℝ)) ^ (c.den) = (((2 : ℚ) ^ (c.num.toNat) : ℚ) : ℝ) := by
 191    rw [← Real.rpow_natCast ((2 : ℝ) ^ (c : ℝ)) c.den, ← Real.rpow_mul (by norm_num), hcq,
 192      Real.rpow_natCast]
 193    push_cast
 194    ring
 195  obtain ⟨r, hr⟩ := rat_of_trace_rat_of_pow_rat hu1 ht c.pos hpow
 196  have hrq : r ^ (c.den) = (2 : ℚ) ^ (c.num.toNat) := by
 197    have h : ((r ^ (c.den) : ℚ) : ℝ) = (((2 : ℚ) ^ (c.num.toNat) : ℚ) : ℝ) := by
 198      rw [← hpow, hr]; push_cast; ring
 199    exact_mod_cast h
 200  have hrne : r ≠ 0 := by
 201    intro h
 202    rw [h, zero_pow (by have := c.pos; omega : c.den ≠ 0)] at hrq
 203    have hp : (0 : ℚ) < (2 : ℚ) ^ (c.num.toNat) := by positivity
 204    rw [← hrq] at hp
 205    exact lt_irrefl _ hp
 206  have hv1 : padicValRat 2 (r ^ (c.den)) = (c.den : ℕ) * padicValRat 2 r :=
 207    padicValRat.pow hrne
 208  have hself : padicValRat 2 ((2 : ℚ)) = 1 := by
 209    have h := padicValRat.self (p := 2) (by norm_num)
 210    norm_num at h
 211    exact h
 212  have hv2 : padicValRat 2 ((2 : ℚ) ^ (c.num.toNat)) = (c.num.toNat : ℕ) * 1 := by
 213    rw [padicValRat.pow (by norm_num : (2 : ℚ) ≠ 0), hself]
 214  rw [hrq, hv2] at hv1
 215  have hdvd : c.den ∣ c.num.toNat := by
 216    have hz : ((c.den : ℕ) : ℤ) ∣ ((c.num.toNat : ℕ) : ℤ) :=
 217      ⟨padicValRat 2 r, by push_cast at hv1 ⊢; linarith⟩
 218    exact_mod_cast hz
 219  have hpabs : c.num.toNat = c.num.natAbs := by
 220    have h1 : ((c.num.toNat : ℕ) : ℤ) = c.num := Int.toNat_of_nonneg (le_of_lt hnum)
 221    have h2 : ((c.num.natAbs : ℕ) : ℤ) = c.num := Int.natAbs_of_nonneg (le_of_lt hnum)
 222    omega
 223  have hcop : Nat.gcd c.num.toNat c.den = 1 := by
 224    rw [hpabs]; exact c.reduced
 225  exact Nat.dvd_one.mp (hcop ▸ Nat.dvd_gcd hdvd dvd_rfl)
 226
 227/-! ## The chain, with the imported inputs named
 228
 229Neither the six exponentials theorem nor the Erdős power-function step is in Mathlib, so
 230they enter as explicit hypotheses. A reader can see precisely what is imported. -/
 231
 232/-- The six exponentials input, in exactly the form the classification uses: if the trace
 233of `n^c` is rational at the three bases two, three and five, the exponent is rational.
 234This is a published corollary of the six exponentials theorem (Lang, Ramachandra) and is
 235stated as a hypothesis because the ambient library carries neither it nor
 236Gelfond--Schneider. -/
 237def SixExponentialsTraceInput : Prop :=
 238  ∀ c : ℝ, (∀ n : ℕ, 2 ≤ n → n ≤ 5 →
 239      ∃ t : ℚ, ((n : ℝ)) ^ c + (((n : ℝ)) ^ c)⁻¹ = (t : ℝ)) →
 240    ∃ r : ℚ, c = (r : ℝ)
 241
 242/-- **The exponent is a positive integer.** Given the imported six exponentials input, a
 243positive real exponent whose traces at the small bases are rational is a positive integer.
 244It is not further restricted to the odd integers: both parities are inhabited, by
 245`Cost.GaugeOrbitFromRealCharacter.signedPowerNativeCost_sansAnchor`. This is the arithmetic
 246half of `GaugeOrbitIsSignedPowerFamily_of_sixExponentials`; the analytic half is Howe. -/
 247theorem exponent_is_positive_integer (hsix : SixExponentialsTraceInput)
 248    {c : ℝ} (hc : 0 < c)
 249    (htrace : ∀ n : ℕ, 2 ≤ n → n ≤ 5 →
 250      ∃ t : ℚ, ((n : ℝ)) ^ c + (((n : ℝ)) ^ c)⁻¹ = (t : ℝ)) :
 251    ∃ k : ℕ, 1 ≤ k ∧ c = (k : ℝ) := by
 252  obtain ⟨r, hr⟩ := hsix c htrace
 253  have hrpos : 0 < r := by
 254    have h : (0 : ℝ) < (r : ℝ) := hr ▸ hc
 255    exact_mod_cast h
 256  obtain ⟨t, ht⟩ := htrace 2 (by norm_num) (by norm_num)
 257  have ht' : (2 : ℝ) ^ ((r : ℚ) : ℝ) + ((2 : ℝ) ^ ((r : ℚ) : ℝ))⁻¹ = (t : ℝ) := by
 258    rw [← hr]
 259    norm_num at ht ⊢
 260    exact ht
 261  have hden : r.den = 1 := int_of_rat_exponent_of_trace_rat hrpos ht'
 262  have hnum : 0 < r.num := Rat.num_pos.mpr hrpos
 263  refine ⟨r.num.toNat, by omega, ?_⟩
 264  have hrn : ((r.num : ℤ) : ℚ) = r := by
 265    conv_rhs => rw [← Rat.num_div_den r]
 266    rw [hden]
 267    norm_num
 268  have hfin : ((r.num.toNat : ℕ) : ℚ) = r := by
 269    rw [show ((r.num.toNat : ℕ) : ℚ) = ((r.num.toNat : ℕ) : ℤ) by push_cast; ring,
 270      Int.toNat_of_nonneg (le_of_lt hnum)]
 271    exact hrn
 272  rw [hr]
 273  exact_mod_cast congrArg (fun x : ℚ => (x : ℝ)) hfin.symm
 274
 275/-! ### Axiom audit -/
 276
 277#print axioms no_rational_character_at_trace_three
 278#print axioms rat_of_trace_rat_of_pow_rat
 279#print axioms int_of_rat_exponent_of_trace_rat
 280#print axioms exponent_is_positive_integer
 281
 282end TraceRationalExponent
 283end Cost
 284end IndisputableMonolith
 285