Cost Trace Rational Exponent Rat Of Trace Rat Of Pow Rat

The rationality bridge

In number theory, the trace of a real number u is the sum u + u⁻¹. The question behind this theorem is simple: if you know the trace is a rational number, and you know some positive power of u is also rational, what can you conclude about u itself? The answer, proved in the machine-checked library of formal theorems, is that u must be rational. The declaration rat_of_trace_rat_of_pow_rat states this exactly: for u greater than 1, if u + u⁻¹ is rational and u^q is rational for some positive integer q, then u is rational.

The proof is a short argument about quadratic objects. A real number above 1 with a rational trace satisfies a quadratic equation, so it lives in a field generated by 1 and d = u - u⁻¹. The theorem shows that every power of u can be written as a + b·d with a and b strictly positive rationals. If some power lands back in the rationals, the irrational part b·d must vanish, but b is strictly positive at every step, so the only way for the power to be rational is for d itself to be zero, which forces u to be rational. The positivity of b is the load-bearing fact: it forbids the irrational part from cancelling.

This result matters because it separates the arithmetic core of the framework's cost classification from the analytic input. It shows that a genuinely quadratic unit can never have a rational power, so if a rational trace coexists with a rational power, the underlying object was rational all along. The theorem does not, however, say anything about which exponents are allowed. That step requires the six exponentials theorem, which is imported as an explicit hypothesis because the ambient library does not carry it. The framework's own theorem is the arithmetic half; the analytic half is supplied from outside.

In Recognition Science, this theorem is one link in the chain that classifies the possible cost functions. The framework models the cost of recognition as a function of a ratio, and the trace of that ratio appears as a natural quantity. The rationality bridge ensures that when the trace is rational and a power is rational, the ratio itself is rational, which narrows the search for valid cost functions. It is a small, precise fact, but it is the kind of fact that makes a classification tractable: it rules out an entire family of irrational candidates in one stroke.

/-- **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

/-- Powers of `u` on the basis `{1, d}` with `d = u - u⁻¹`, both coordinates strictly
positive rationals. The positivity of the second coordinate is the whole point: it is
what forbids the irrational part from cancelling. -/
private theorem pow_eq_coords {u : ℝ} (hu : 1 < u) {t : ℚ}
    (ht : u + u⁻¹ = (t : ℝ)) :
    ∀ k : ℕ, 1 ≤ k → ∃ a b : ℚ, 0 < a ∧ 0 < b ∧
      u ^ k = (a : ℝ) + (b : ℝ) * (u - u⁻¹) := by
  have hupos : (0 : ℝ) < u := lt_trans zero_lt_one hu
  have hu0 : u ≠ 0 := ne_of_gt hupos
  have htgt : (2 : ℝ) < (t : ℝ) := by
    rw [← ht]
    have hsq : (0 : ℝ) < (u - 1) ^ 2 := by nlinarith
    have hpos : (0 : ℝ) < (u - 1) ^ 2 / u := div_pos hsq hupos
    have hid : u + u⁻¹ - 2 = (u - 1) ^ 2 / u := by field_simp; ring
    linarith
  have htq : (2 : ℚ) < t := by exact_mod_cast htgt
  obtain ⟨d, hddef⟩ : ∃ d : ℝ, d = u - u⁻¹ := ⟨_, rfl⟩
  have hbase : u = (t : ℝ) / 2 + d / 2 := by
    rw [hddef, ← ht]; ring
  have hd2 : d ^ 2 = (t : ℝ) ^ 2 - 4 := by
    rw [hddef, ← ht]
    field_simp
    ring
  intro k hk
  rw [← hddef]
  induction k with
  | zero => omega
  | succ n ih =>
      rcases Nat.eq_or_lt_of_le hk with h1 | h1
      · refine ⟨t / 2, 1 / 2, by linarith, by norm_num, ?_⟩
        have hn0 : n = 0 := by omega
        subst hn0
        rw [pow_one]
        push_cast
        linarith [hbase]
      · have hn : 1 ≤ n := by omega
        obtain ⟨a, b, ha, hb, hab⟩ := ih hn
        have h4 : (0 : ℚ) < t ^ 2 - 4 := by nlinarith
        refine ⟨a * (t / 2) + b * (1 / 2) * (t ^ 2 - 4),
                a * (1 / 2) + b * (t / 2), by positivity, by positivity, ?_⟩
        rw [pow_succ, hab]
        push_cast
        linear_combination ((a : ℝ) + (b : ℝ) * d) * hbase + ((b : ℝ) / 2) * hd2

What this page does not claim

The theorem does not identify which exponents are allowed; that requires the imported six exponentials hypothesis. The theorem does not apply to u less than or equal to 1, where the positivity argument fails. The theorem does not prove that a rational trace alone forces rationality; a rational power is also required.

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: