Encyclopedia Cost Cost Trace Rational Exponent Int Of Rat Exponent Of Trace Rat

ARTICLE 4 claims 4 theorems

Cost Trace Rational Exponent Int Of Rat Exponent Of Trace Rat

A simple arithmetic fact about powers of two governs which exponents can appear in the framework's cost functions.

Verify this page

The rational exponent theorem

The declaration int_of_rat_exponent_of_trace_rat is a theorem about numbers of the form 2c + 2-c, where c is a positive rational number. It proves that if this sum is itself a rational number, then c must be an integer. In plainer terms: if you take a positive fraction like 1/2 or 3/4 as your exponent, the sum 2c + 2-c will always be irrational. Only whole-number exponents produce a rational result.

The proof rests on a deeper fact about quadratic numbers. If a real number u greater than 1 has a rational trace (meaning u + u-1 is rational), and some positive power of u is rational, then u itself must be rational. The theorem applies this to u = 2c. If c were a non-integer rational like 1/2, then u would be a genuinely quadratic irrational, and no positive power of it could land back in the rationals. Since the trace is assumed rational, the exponent cannot have a denominator greater than one.

This result is the arithmetic half of a larger classification. Together with the six exponentials theorem, which rules out irrational exponents, it pins down the possible exponents in the framework's gauge classification. The theorem is careful about what it assumes: it never requires 2c itself to be rational, only the sum 2c + 2-c. That weakening is necessary, because the trace equation r + r-1 = 3 has no rational solution, even though the golden ratio squared satisfies it.

What the theorem does not claim is broader. It does not prove that all exponents in the classification are integers; that requires the six exponentials input, which is imported as an explicit hypothesis. It also does not restrict the integer to odd values: both parities are inhabited in the framework. The theorem is a precise arithmetic statement, not a complete classification on its own.

THEOREM int_of_rat_exponent_of_trace_rat · IndisputableMonolith/Cost/TraceRationalExponent.lean
int_of_rat_exponent_of_trace_rat · IndisputableMonolith/Cost/TraceRationalExponent.lean:168 
/-- **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)
THEOREM rat_of_trace_rat_of_pow_rat · IndisputableMonolith/Cost/TraceRationalExponent.lean
rat_of_trace_rat_of_pow_rat · IndisputableMonolith/Cost/TraceRationalExponent.lean:145 
/-- **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
THEOREM int_of_rat_exponent_of_trace_rat · IndisputableMonolith/Cost/TraceRationalExponent.lean
int_of_rat_exponent_of_trace_rat · IndisputableMonolith/Cost/TraceRationalExponent.lean:168 
/-- **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)
THEOREM no_rational_character_at_trace_three · IndisputableMonolith/Cost/TraceRationalExponent.lean
no_rational_character_at_trace_three · IndisputableMonolith/Cost/TraceRationalExponent.lean:70 
/-- **The demand for a carrier-valued character is too strong.** The trace equation
`r + r⁻¹ = 3` has no rational solution. So a cost whose value at the ratio two is the
perfectly rational `1/2` has no rational character at that ratio, and asking the
factorization to produce one asks for something that does not exist. -/
theorem no_rational_character_at_trace_three : ¬ ∃ r : ℚ, r + r⁻¹ = 3 := by
  rintro ⟨r, hr⟩
  have hr0 : r ≠ 0 := by
    intro h
    rw [h] at hr
    norm_num at hr
  have hquad : r ^ 2 - 3 * r + 1 = 0 := by
    field_simp at hr
    linarith [hr]
  exact no_rational_sqrt_five ⟨2 * r - 3, by nlinarith [hquad]⟩

What this page does not claim

The theorem does not prove that all exponents in the classification are integers, since that relies on the six exponentials input. It does not restrict the exponent to odd integers; both parities are inhabited. It does not require 2^c itself to be rational, only the sum 2^c + 2^(-c).

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cost/TraceRationalExponent.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND