Encyclopedia Cost Cost Trace Rational Exponent Exponent Is Positive Integer

ARTICLE 3 claims 3 theorems

Cost Trace Rational Exponent Exponent Is Positive Integer

A rational trace at the small bases forces a positive exponent to be a whole number, and the proof leans on an imported number-theory input.

Verify this page

The exponent step

In the framework's ledger, a discrete record of recognition events, certain costs are built from powers of a base such as 2. The question is which exponents are allowed. The declaration exponent_is_positive_integer states a precise arithmetic condition: if a positive real exponent c has the property that for each base n equal to 2, 3, 4, or 5, the quantity n^c + n^(-c) is a rational number, then c is a positive integer. In plainer terms, once the trace at those four small bases lands in the rationals, the exponent cannot be a fraction or an irrational number; it must be a whole counting number like 1, 2, or 3.

The proof splits into two halves. The first half, already in the machine-checked library, shows that if c is rational and the trace at base 2 is rational, then c has denominator 1, so c is an integer. The argument uses a quadratic object: a real number u above 1 with a rational trace generates a basis {1, d} where d = u - u^(-1), and both coordinates of every power stay strictly positive rationals. That positivity is what prevents the irrational part from cancelling, so a rational power of u forces u itself to be rational. The second half, which rules out irrational c, is not proved inside the library; it is imported as an explicit hypothesis named SixExponentialsTraceInput, a published corollary of the six exponentials theorem of Lang and Ramachandra. The declaration therefore does not claim to prove the six exponentials theorem; it uses it as a stated input.

What the declaration does not claim is as important as what it proves. It does not assert that 2^c itself is rational; only the trace n^c + n^(-c) is required to be rational. That weakening is necessary because, as a separate theorem shows, the equation r + r^(-1) = 3 has no rational solution, so a cost with a perfectly rational value can have no rational character. The declaration also does not restrict c to odd integers; both even and odd positive integers are inhabited by other constructions in the framework. Finally, the theorem does not by itself complete the classification of gauge orbits; it is the arithmetic half, paired with an analytic half attributed to Howe, and the full classification is a separate result that combines both.

THEOREM exponent_is_positive_integer · IndisputableMonolith/Cost/TraceRationalExponent.lean
exponent_is_positive_integer · IndisputableMonolith/Cost/TraceRationalExponent.lean:242 
/-- **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
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 declaration does not prove the six exponentials theorem. It does not require 2^c itself to be rational. It does not restrict the exponent to odd integers.

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