exists_nat_exponent
plain-language theorem explainer
Under the six-exponentials trace input and nondegeneracy at 2, the extracted real character on positive integers is exactly n ↦ n^k for some positive integer k. Classification of anchor-free gauge orbits cites this to pin the power family to ℕ-exponents. The proof takes Howe's real exponent, forces positivity from the anchor root, then integrality from six exponentials on n = 2..5.
Claim. Assume the six-exponentials trace input, the anchor-free structural hypotheses on the ledger map $F$, and nondegeneracy $\mathrm{Tr}_F(2)\neq 2$. Then there exists an integer $k\ge 1$ such that for every integer $n\ge 1$, the nontrivial character value of $F$ at $n$ equals $n^k$ as a real number.
background
In the cost/gauge-orbit setting, a ledger map $F$ on ratio orbits yields a rational trace. When that trace at 2 is not the flat value 2, one extracts a real character nontrivialCharacterValue by linear extraction against the principal root at two (the anchor root). That root is strictly larger than 1 under the same nondegeneracy.
Restricted to positive integers, the extracted character is completely multiplicative and monotone (via the ledger comparison le_of_trace_le). Erdős's theorem in Howe's form then supplies a single nonnegative real exponent $c$ with $f(n)=n^c$. The six-exponentials trace input is the arithmetic hypothesis that upgrades $c$ from a real to a positive integer; the module doc marks this theorem as the sole consumer of that import.
Upstream, natChar_monotoneMultiplicative packages the integer restriction into the exact hypotheses of exists_exponent. The anchor-root comparison and the character-trace identities at positive rationals are the RealCharacterFactorization facts used to feed the integrality step.
proof idea
Apply exists_exponent to natChar_monotoneMultiplicative hS hnt to obtain a real $c\ge 0$ with character value $n^c$ on $\mathbb{N}_{\ge 1}$. Identify the value at 2 with the anchor root (nontrivialCharacterValue_two), and use anchorRoot_gt_one plus real-power monotonicity to rule out $c\le 0$, so $c>0$.
For each integer $n$ with $2\le n\le 5$, rebuild the doubled-trace identity: $n^c+(n^c)^{-1}$ equals a rational (the native doubled cost of the ratio orbit of $n$), via nontrivialCharacterValue_trace. Feed positivity of $c$ and these four rational traces into exponent_is_positive_integer under the six-exponentials input to obtain $k\in\mathbb{N}$, $k\ge 1$, with $c=k$. Rewrite $n^c$ as the natural power $n^k$.
why it matters
This is the integrality bridge in the anchor-free gauge classification. Downstream, GaugeOrbitIsSignedPowerFamily_of_sixExponentials case-splits on degeneracy at 2: the flat case is the pure sign gauge; the nonflat case routes through this theorem (and the rational extension) to conclude every structural cost is a sign-extended integer power cost.
As the doc-comment states, Howe gives the real exponent, the anchor root forces positivity, and six exponentials forces integrality; this is the only use site of that arithmetic import in the module. The parent theorem explicitly does not force odd exponents and does not yet select the RS cost $J$; selection is leastness in Cost.UnitFromMinimality. In the broader forcing chain this sits on the cost side that eventually isolates $J(x)=\cosh(\log x)-1$ (T5) rather than on the geometric T6–T8 steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.