If every $n^\alpha$ is an integer then $\alpha$ is a positive integer

Proved

HardyFiveAxioms.exponent_isNat_of_rpow_isNat

by Lucas · Oct 2, 2026 · Mathlib 0df444a (Lean v4.33.1)

mathematical-physicsnumber-theoryquantum-foundations

Let $\alpha>0$ be a real number such that $n^\alpha$ is a natural number for every positive integer $n$ . Then $\alpha$ is a positive integer:

\alpha\in\{1,2,3,\dots\}.

In Section 8.1 Hardy passes from $K(N)=N^\alpha$ to $K(N)=N^r$ with $r=1,2,3,\dots$ with the words "Since $K$ must be an integer it follows that the power, $\alpha$ , must be a positive integer." This milestone isolates that step.

Formalization Note $n^\alpha$ is Real.rpow and "is a natural number" means equal to the cast of some m : ℕ.

Preamble

import Mathlib

Formal statement

namespace HardyFiveAxioms

/-- Hardy 2001, Section 8.1: if `α > 0` and `n^α` is a (natural) integer for every positive
integer `n`, then `α` is a positive integer. -/
theorem exponent_isNat_of_rpow_isNat (α : ℝ) (hα : 0 < α)
    (hint : ∀ n : ℕ, 1 ≤ n → ∃ m : ℕ, (n : ℝ) ^ α = m) :
    ∃ r : ℕ, 1 ≤ r ∧ α = r := by sorry

end HardyFiveAxioms

Source

L. Hardy, *Quantum Theory From Five Reasonable Axioms*, arXiv:quant-ph/0101012v4 (2001), https://arxiv.org/abs/quant-ph/0101012, p. 16, Section 8.1, sentence before Eq. (57)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

NON-BLIND READ-BACK — NOT INDEPENDENT TESTIMONY. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement below, with full knowledge of the source paper and of the intended meaning. It was not produced by a blind, independent auditor, so it may share the drafter's blind spots. Reviewers must not treat it as independent confirmation of faithfulness; compare the Lean code against the source directly.

Let $\alpha$ be a real number with $\alpha>0$ . Assume that for every natural number $n\ge1$ there is a natural number $m$ with $n^\alpha=m$ , where $n^\alpha$ is the real power $e^{\alpha\ln n}$ . Then there is a natural number $r\ge1$ with $\alpha=r$ .

Human review

Endorsed by Shuze Chen · Oct 8, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

If every nαn^\alphanα is an integer then α\alphaα is a positive integer

If every $n^\alpha$ is an integer then $\alpha$ is a positive integer