Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-02
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The exponential definition of real powers agrees with the existing rational powers

Statement

If a>0a>0 and r∈Qr\in\mathbb Q, then the real power ar=exp⁡(rlog⁡a)a^r=\exp(r\log a) agrees with the rational power of Rational powers ara^r of a positive base. For r>0r>0, both conventions also give 0r=00^r=0.

Facts & Assumptions

Given: A positive real aa and a rational r=p/qr=p/q with q≥1q\ge1.

[L1]

Rational powers satisfy (ap/q)q=ap(a^{p/q})^q=a^p, are positive for positive base, and obey the rational power laws (Rational powers ara^r of a positive base, Laws of rational exponents).

[L2]

For positive reals, log⁡(xy)=log⁡x+log⁡y\log(xy)=\log x+\log y, log⁡(1/x)=−log⁡x\log(1/x)=-\log x, and log⁡\log is injective (Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm).

[L3]

The real-power definition is au=exp⁡(ulog⁡a)a^u=\exp(u\log a) (Real powers for positive bases, with the zero-base positive-exponent convention).

Proof

technique · direct
1.1

For q≥1q\ge1, the product law for log⁡\log gives log⁡((ap/q)q)=qlog⁡(ap/q)=plog⁡a=log⁡(ap)\log((a^{p/q})^q)=q\log(a^{p/q})=p\log a=\log(a^p).

L1L2
2.1

Injectivity of log⁡\log gives log⁡(ap/q)=(p/q)log⁡a\log(a^{p/q})=(p/q)\log a, and exponentiating gives ap/q=exp⁡((p/q)log⁡a)a^{p/q}=\exp((p/q)\log a).

step 1.1L2L3
3.1

This is the new real power at exponent p/qp/q; negative rational exponents follow by reciprocals, and the stated 0r0^r convention agrees with Rational powers ara^r of a positive base for r>0r>0.

step 2.1L1L3∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 79 results over 22 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources