# Natural-number powers and principal square roots

This English edition is an AI candidate and does not yet have an OCME Atlas (GPT-6) Twin closure receipt.

This entry covers natural-number powers of real bases and principal square roots of nonnegative real numbers, keeping powers, root values, and solution sets distinct.

mko-power-root · definition · v0.10.0



## Mathematical statement

For a real number a and a natural number n, use the empty-product convention a^0=1 (including 0^0=1 in this algebraic setting) and define powers recursively by a^(n+1)=a^n·a. For r≥0, the principal square root √r is the unique real number y satisfying y≥0 and y²=r.





## Representative formula (exact TeX)

a^{n}





## Assumptions


- n∈N={0,1,2,…}; negative exponents, noninteger exponents, and complex branches are outside this entry.
- The real principal square root is defined here only for r≥0. The convention 0^0=1 is algebraic and does not prescribe a rule for limits.





## Symbol scope


- a — real base
- n — natural-number exponent





## Intuition, definition, and misconceptions

a^n does not mean a·n. At n=0, the empty product is 1; for n>0, it is a product of n copies of a. A negative base has a negative positive-odd power and a positive positive-even power. A zero base raised to a positive power remains zero.

√0=0, and the principal square root of positive r selects the nonnegative branch. The real solution set of y²=r has two roots ±√r when r>0, only zero when r=0, and is empty when r<0. Consequently √(a²)=|a|, and it cannot be replaced by a without a sign condition.

The exercises use exact instances with integer bases, nonnegative integer exponents, and perfect squares, and separately check the domain condition for negative radicands. A future bridge to Mathlib Real.sqrt must impose r≥0 because its zero value for negative inputs is not the textbook root value defined here.

Common errors include giving ± values for a principal square root, replacing √(a²) with a without checking its sign, or applying the local 0^0 convention to limits.





## Adopted derivation guide

[Natural-number powers and principal square roots: computing powers by recursion and proving √(a²)=|a|](https://ocme.evemisslab.com/en/derivations/derivation-mko-power-root-01/)The original MKO is retained. The guide has its own append-only revision and verification boundaries, not a new Lean proof.





## Prerequisites


- [Arithmetic operations](https://ocme.evemisslab.com/en/mko/mko-arithmetic-operations/) — Natural-number powers are defined recursively using multiplication.
- [Real number](https://ocme.evemisslab.com/en/mko/mko-real-number/) — The principal square-root branch is selected using the nonnegative real domain and its order.





## Verification boundary

The stated instances can be recomputed exactly; formal Evidence for general square-root existence and uniqueness and power laws has not yet been attached.

not_formalized

This does not mean the content is false; it means no replayable computational or formal evidence is registered yet.





## Next obligation

Bind the empty-product recursion for natural powers, the nonnegative principal-root premise, sqrt_sq_eq_abs, and the zero-value boundary of Real.sqrt.





## Same-source structured data

This page and the interactive view use the same object and existing language edition; this adds no proof or human review.

[Canonical MKO JSON](https://ocme.evemisslab.com/data/mko/power-root.json) · [Plain Markdown](https://ocme.evemisslab.com/en/mko/mko-power-root/index.md)