SixExponentialsTraceInput
plain-language theorem explainer
Packages the six-exponentials arithmetic hypothesis used by the anchor-free gauge classification: if a real exponent c makes the traces n^c + n^{-c} rational at bases 2 through 5, then c is rational. Cited wherever the ledger is reduced to signed power costs. Pure Prop definition; the content is a published corollary of Lang–Ramachandra, not proved in-library.
Claim. The proposition asserting: for every real $c$, if $n^{c} + n^{-c}$ is rational for every natural number $n$ with $2 \le n \le 5$, then $c$ itself is rational.
background
In the Recognition cost ledger, structural native costs factor through real multiplicative characters on the positive rationals. The relevant invariant is the two-sided trace $n^{c} + n^{-c}$ (equivalently $2\cosh(c\log n)$), which is the value that must stay rational when the cost is required to land in a rational gauge orbit at small integer bases.
The six exponentials theorem (Lang, Ramachandra) and its corollaries control linear independence of logarithms of algebraic numbers. A standard consequence is that a real exponent whose traces at a short list of integer bases are rational must itself be rational. The ambient Mathlib stack does not carry six exponentials or Gelfond–Schneider, so the classification imports that consequence as a named hypothesis rather than a proved theorem.
Locally this module isolates the arithmetic step that turns a positive real exponent with rational traces into a positive integer exponent; the analytic existence of a real exponent is supplied upstream by Howe-type factorization.
proof idea
No proof: this is a bare Prop definition. The body is the universal statement over real $c$ with the trace-rationality premise at $n\in{2,3,4,5}$ and the conclusion that $c$ is the coercion of a rational. Downstream theorems assume an inhabitant of this Prop and apply it as a black-box implication.
why it matters
This is the single named arithmetic import for the anchor-free gauge classification. GaugeOrbitIsSignedPowerFamily_of_sixExponentials takes it as hypothesis and concludes every structural ledger inhabitant is the sign cost or a sign-extended power cost of a nonnegative integer exponent. The same hypothesis is the only external input to exists_nat_exponent and to exponent_is_positive_integer, which is the arithmetic half of that classification (the analytic half is Howe).
It deliberately does not force odd exponents: both parities inhabit the ledger via signedPowerNativeCost_sansAnchor, and the stricter odd-power classification is refuted. Selection of the unique minimal cost $J$ is separate and lives in unit-from-minimality, not here. In the broader RS chain this keeps the cost side of T5 (J-uniqueness) honest about which transcendental arithmetic is assumed versus proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.