exponent_is_positive_integer
plain-language theorem explainer
A positive real exponent whose power-traces at bases 2 through 5 are all rational must be a positive integer, once the six-exponentials trace input is granted. Gauge-orbit classification cites this as the arithmetic half that turns Howe's real exponent into a natural number. The proof first forces rationality of the exponent, then shows the denominator is one via the base-2 trace.
Claim. Assume the six-exponentials trace input: whenever a real $c$ has rational traces $n^c + n^{-c}$ for all integers $n$ with $2 \le n \le 5$, then $c$ is rational. If $c > 0$ and those traces are rational, then there exists a positive integer $k \ge 1$ with $c = k$.
background
In the Recognition cost calculus the native cost of a ratio is controlled by a real character of the form $n \mapsto n^c + n^{-c}$ (the trace of the power). The module studies when such an exponent $c$ is forced to be integral.
The hypothesis SixExponentialsTraceInput packages a published corollary of the six exponentials theorem (Lang, Ramachandra): rational traces at the three bases 2, 3 and 5 already imply that $c$ itself is rational. It is kept as an explicit hypothesis because the ambient library does not contain six exponentials or Gelfond--Schneider.
Upstream, int_of_rat_exponent_of_trace_rat shows that a positive rational exponent with rational base-2 trace has denominator one. The companion no_rational_character_at_trace_three records that the stronger demand of a rational carrier (not merely a rational trace) is empty: $r + r^{-1} = 3$ has no rational solution. Together these isolate the arithmetic content of the exponent step.
proof idea
Apply the six-exponentials input to $c$ and the given rational-trace hypothesis to obtain a rational $r$ with $c = r$ in $\mathbb{R}$. Positivity of $c$ transfers to $r > 0$. Specialize the trace hypothesis at base 2 to get a rational $t$ with $2^r + 2^{-r} = t$. Feed that into int_of_rat_exponent_of_trace_rat to conclude $r.den = 1$. The numerator is then a positive integer; cast it via toNat and transport equality back through the rational embedding to obtain $c = k$ for $k = r.num.toNat \ge 1$.
why it matters
This is the arithmetic half of the gauge-orbit classification under six exponentials. Downstream, exists_nat_exponent in GaugeOrbitClassification quotes it directly: Howe supplies a real exponent, the anchor root makes it positive, and this lemma turns it into a natural number $k$ so that the nontrivial character is exactly $n \mapsto n^k$. The doc-comment there notes this is the only place the six-exponentials import is used.
It also feeds structural ledger comparisons such as cubeGeneratedNativeCost_two_not_canonical, which need integer exponents to separate cube-generated native costs from the canonical on-ratio orbit. The result deliberately does not force oddness: both parities are inhabited by signed-power native costs, so the classification retains the full positive-integer family rather than only odd powers. In the broader RS forcing picture this pins the discrete rung structure of cost characters once the analytic (Howe) half is in place.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.