# Natural-number powers and principal square roots: computing powers by recursion and proving √(a²)=|a|

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-power-root/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

derivation-mko-power-root-01 · production-20261019-adopted-96



## Goal and scope

Using only the recursive definition a^0=1, a^(n+1)=a^n·a, compute (−2)^n for n=0,1,2,3,4 and 0^0, 0^3; prove that a nonnegative square root is unique and that √(a²)=|a| for every real a; then find √49, √((−5)²) and the real solution set of y²=9, and explain why √(−4) is not defined in the reals.

Works inside the MKO's scope: real bases, natural-number exponents (including 0), and the principal square root only for real r≥0. Negative and noninteger exponents and complex branches are not treated; 0^0=1 is used only as a convention of this algebraic setting and yields no rule for limits. Existence of a square root for a general r≥0 (for example √2) is not proved here, since the guide only needs the case r=a²; the canonical MKO and its English edition are not changed.





## Givens and symbols


- distributive
- neg_mul
- zero_product
- order_basics
- square_nonneg
- abs_rules
- numeric_evaluation


- G1 — a∈ℝ and n∈ℕ (ℕ contains 0); powers are defined recursively by a^0=1 (including 0^0=1 in this algebraic setting) and a^(n+1)=a^n·a (MKO statement and assumption a1).
- G2 — For r≥0, the principal square root √r is the real y with y≥0 and y²=r; the MKO asserts that such a y is unique. For r<0, √r is not defined in this setting (MKO assumption a2).
- G3 — Data: the bases −2 and 0; the root inputs 49, (−5)², 9 and −4.


- a^n — the n-th power of the real a (n∈ℕ)
- \sqrt{r} — the principal square root of r≥0: the unique real y with y≥0 and y²=r
- |a| — absolute value: a if a≥0, −a if a<0
- y_1,\ y_2 — two nonnegative candidate roots in the uniqueness proof





## Rules and sources


- distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
- neg_mul · prerequisite — Signs and multiplication: (−u)v=−(uv) and (−u)(−v)=uv.
- zero_product · prerequisite — Zero-product property: in ℤ, ℚ, ℝ, ℂ (or any integral domain), uv=0 ⇔ u=0 or v=0.
- order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
- square_nonneg · prerequisite — Squares are nonnegative: for every real u, u²≥0, and u²=0 ⇔ u=0.
- abs_rules · prerequisite — Absolute value (reals): |u|=u if u≥0 and |u|=−u if u<0; |u|≥0; |uv|=|u||v|; triangle inequality |u+v|≤|u|+|v|; |u|<r ⇔ −r<u<r.
- numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
- def_intro · prerequisite — Introducing a definition: a statement, expression or object may be given a name, after which the name and what it stands for are interchangeable.
- def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
- mul_one · prerequisite — Multiplicative identity: 1·u=u.
- mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
- mul_zero · prerequisite — Multiplying by zero: u·0=0. Reason: u·0=u·(0+0)=u·0+u·0; subtracting u·0 from both sides gives 0=u·0.
- add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
- eq_congruence · prerequisite — Congruence of equality: if u=v, applying the same defined operation f to both sides gives f(u)=f(v). Operating on one side only is not an instance of this rule.
- case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
- eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
- sqrt_def · prerequisite — Principal square root: for a≥0, √a is the unique real b with b≥0 and b²=a. Negative numbers have no real square root.
- forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds.
- mko_power_root · cited — 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. · mko-power-root
- L_root_unique · lemma — If reals y_1, y_2 are both ≥0 and y_1²=y_2², then y_1=y_2.
- L_abs_sq · lemma — For every real a, |a|≥0 and |a|²=a².





## Main derivation

S01 · definitionBefore

a^n,\quad a\in\mathbb{R},\ n\in\mathbb{N}

After

a^0=1,\qquad a^{n+1}=a^n\cdot a

Conditions: n\in\mathbb{N}

Rule: mko_power_root · Uses: G1

Leaf basis: mko_power_root + def_intro

By the MKO, powers are defined recursively: exponent 0 gives the empty product 1 (including 0^0=1, a convention of this algebraic setting), and raising the exponent by one multiplies once more by the base. So for n>0, a^n is a product of n copies of a, not a·n. Exponents are natural numbers only; negative and noninteger exponents and complex branches are out of scope.



S02 · equivalentBefore

(-2)^1

After

(-2)^0\cdot(-2)=1\cdot(-2)=-2

Conditions: none

Rule: def_unfold · Uses: S01, G3

Leaf basis: def_unfold + mko_power_root + mul_one

Use the second clause with n=0: (−2)^1=(−2)^0·(−2); then the first clause (−2)^0=1 and 1·u=u give −2.



S03 · equivalentBefore

(-2)^2

After

(-2)^1\cdot(-2)=(-2)(-2)=4

Conditions: none

Rule: neg_mul · Uses: S01, S02

Leaf basis: def_unfold + neg_mul + numeric_evaluation

Recursion with n=1: (−2)^2=(−2)^1·(−2)=(−2)(−2). By (−u)(−v)=uv, (−2)(−2)=2·2=4.



S04 · equivalentBefore

(-2)^3

After

(-2)^2\cdot(-2)=4\cdot(-2)=-8

Conditions: none

Rule: neg_mul · Uses: S01, S03

Leaf basis: def_unfold + neg_mul + mul_comm + numeric_evaluation

Recursion with n=2: (−2)^3=(−2)^2·(−2)=4·(−2). By u(−v)=−(uv), 4·(−2)=−8. This is not (−2)·3=−6: a power multiplies the base repeatedly, it does not multiply by the exponent.



S05 · equivalentBefore

(-2)^4

After

(-2)^3\cdot(-2)=(-8)(-2)=16

Conditions: none

Rule: neg_mul · Uses: S01, S04

Leaf basis: def_unfold + neg_mul + numeric_evaluation

Recursion with n=3: (−2)^4=(−8)(−2)=16. So (−2)^n for n=0,1,2,3,4 is 1, −2, 4, −8, 16: these odd powers are negative and these even powers positive, as MKO para0 describes. This is a computation for five exponents and is not offered as a proof for every n.



S06 · equivalentBefore

0^0,\ 0^1,\ 0^2,\ 0^3

After

0^0=1,\ 0^1=1\cdot 0=0,\ 0^2=0\cdot 0=0,\ 0^3=0\cdot 0=0

Conditions: none

Rule: mul_zero · Uses: S01, G3

Leaf basis: def_unfold + mko_power_root + mul_zero + mul_one

0^0=1 comes straight from the first clause of the definition (the algebraic convention stated in the MKO). Then 0^1=0^0·0=1·0=0, 0^2=0^1·0=0 and 0^3=0^2·0=0 (u·0=0). So a zero base gives zero for positive exponents, and the value 1 at n=0 is fixed by convention, not by any limit.



S07 · impliesBefore

y_1\geq 0,\ y_2\geq 0,\ y_1^2=y_2^2

After

y_1=y_2

Conditions: y_1\geq 0; y_2\geq 0

Rule: L_root_unique · Uses: G2

Leaf basis: L_root_unique + order_basics

The MKO says the principal square root is the unique real with y≥0 and y²=r; this uniqueness can be proved. By Lemma L_root_unique, two nonnegative numbers with equal squares are equal. The proof is S07.1 to S07.3.



S08 · impliesBefore

|a|\quad(a\in\mathbb{R})

After

|a|\geq 0\ \land\ |a|^2=a^2

Conditions: none

Rule: L_abs_sq · Uses: abs_rules

Leaf basis: L_abs_sq + abs_rules + case_analysis

By Lemma L_abs_sq, |a| is nonnegative and its square is a². By trichotomy the two cases a≥0 and a<0 cover every real; the proof is S08.1 and S08.2.



S09 · impliesBefore

\sqrt{a^2}\quad(a\in\mathbb{R})

After

\sqrt{a^2}=|a|

Conditions: a^2\geq 0

Rule: L_root_unique · Uses: G2, S07, S08, square_nonneg

Leaf basis: L_root_unique + L_abs_sq + square_nonneg + sqrt_def

First check that √(a²) makes sense: by square_nonneg, a²≥0, so the definition in G2 applies with r=a². The number y=|a| satisfies y≥0 and y²=a² (S08), so at least one such y exists; by S07 there is at most one such nonnegative y. Hence √(a²) exists and equals |a|. Note that the result is |a|, not a.



S10 · impliesBefore

\sqrt{49}

After

\sqrt{7^2}=|7|=7

Conditions: 7\geq 0

Rule: forall_elim · Uses: S09, G3

Leaf basis: forall_elim + abs_rules + numeric_evaluation

49=7², so S09 with a=7 gives √49=|7|=7. The square of −7 is also 49, but −7<0 fails y≥0, so it is not the principal root.



S11 · impliesBefore

\sqrt{(-5)^2}

After

|-5|=5

Conditions: -5<0

Rule: forall_elim · Uses: S09, G3

Leaf basis: forall_elim + abs_rules + numeric_evaluation

Substitute a=−5 in S09: √((−5)²)=|−5|=5. Direct check: (−5)²=25, 5≥0 and 5²=25. Writing √((−5)²)=−5 would put a negative number on the right, violating y≥0 for the principal root.



S12 · equivalentBefore

y^2=9

After

(y-3)(y+3)=0

Conditions: none

Rule: distributive · Uses: G3, distributive

Leaf basis: distributive + eq_congruence + add_inverse

Subtract 9 from both sides to get y²−9=0; expanding (y−3)(y+3)=y²+3y−3y−9=y²−9 shows that y²=9 is equivalent to (y−3)(y+3)=0.



S13 · equivalentBefore

(y-3)(y+3)=0

After

y=3\ \lor\ y=-3,\quad\text{solution set}\ \{-3,3\}

Conditions: none

Rule: zero_product · Uses: S12, zero_product

Leaf basis: zero_product + eq_congruence

By the zero-product property, y−3=0 or y+3=0, that is y=3 or y=−3. So the real solution set of y²=9 is {−3,3}, with two elements.



S14 · impliesBefore

\{-3,3\}

After

\sqrt{9}=3,\quad \{-3,3\}=\{-\sqrt{9},\sqrt{9}\}

Conditions: none

Rule: L_root_unique · Uses: S09, S13

Leaf basis: L_root_unique + forall_elim + order_basics

Only 3 in the solution set satisfies y≥0, and by S09 with a=3, √9=|3|=3. So the equation has two solutions ±√9, but the symbol √9 denotes one number, 3. The solutions of an equation and the principal root are different things.



S15 · impliesBefore

y^2=-4,\ y\in\mathbb{R}

After

\text{no real solution};\ \sqrt{-4}\ \text{undefined here}

Conditions: -4<0

Rule: square_nonneg · Uses: G2, G3, square_nonneg

Leaf basis: square_nonneg + order_basics + sqrt_def

For every real y, y²≥0>−4, so y²≠−4 and the equation y²=−4 has no real solution. G2 also defines √r only for r≥0, so √(−4) is undefined in this setting. Writing −2 is wrong: (−2)²=4≠−4, and −2<0.







## Substeps and lemmas

S07.1 · equivalentBefore

y_1^2=y_2^2

After

(y_1-y_2)(y_1+y_2)=0

Conditions: none

Rule: distributive · Uses: distributive

Leaf basis: distributive + mul_comm + add_inverse + eq_congruence

Expand (y_1−y_2)(y_1+y_2)=y_1²+y_1y_2−y_2y_1−y_2²=y_1²−y_2² (distributivity, commutativity of multiplication, additive inverses). So y_1²=y_2² is equivalent to y_1²−y_2²=0, that is (y_1−y_2)(y_1+y_2)=0.



S07.2 · equivalentBefore

(y_1-y_2)(y_1+y_2)=0

After

y_1-y_2=0\ \lor\ y_1+y_2=0

Conditions: none

Rule: zero_product · Uses: S07.1, zero_product

Leaf basis: zero_product

By the zero-product property, a product of reals is 0 exactly when at least one factor is 0.



S07.3 · case_splitBefore

y_1-y_2=0\ \lor\ y_1+y_2=0

After

y_1=y_2

Conditions: y_1\geq 0; y_2\geq 0

Rule: case_analysis · Uses: S07.2, order_basics

Leaf basis: case_analysis + order_basics + add_inverse

Case one: y_1−y_2=0; adding y_2 gives y_1=y_2. Case two: y_1+y_2=0, so y_1=−y_2; since y_2≥0, −y_2≤0, so y_1≤0, and with y_1≥0 this gives y_1=0, hence y_2=−y_1=0 and again y_1=y_2. Both cases give y_1=y_2. S07.1 to S07.3 together prove Lemma L_root_unique.



S08.1 · impliesBefore

a\geq 0

After

|a|=a\geq 0,\quad |a|^2=a^2

Conditions: a\geq 0

Rule: abs_rules · Uses: abs_rules

Leaf basis: abs_rules + eq_replace

If a≥0 then |a|=a, so |a|≥0 and |a|²=a² (replacement of equals).



S08.2 · impliesBefore

a<0

After

|a|=-a>0,\quad |a|^2=(-a)(-a)=a^2

Conditions: a<0

Rule: neg_mul · Uses: abs_rules, neg_mul, order_basics

Leaf basis: abs_rules + neg_mul + order_basics

If a<0 then |a|=−a. Adding −a to both sides of a<0 gives 0<−a, so |a|>0. Also (−a)(−a)=a·a=a² (neg_mul). S08.1 and S08.2 together prove Lemma L_abs_sq.







## Reverse audits


- S15 · premise_audit · square_nonneg, G2, order_basics — The conclusion is 'undefined in the reals'; complex branches are not discussed, and the software convention of returning 0 for negative input (MKO para2) is not adopted.
- S14 · premise_audit · S09, S13, L_root_unique — The nonnegativity condition is what selects one of the two solutions; writing √9 as ±3 contradicts uniqueness.
- S13 · inverse_equivalence · zero_product, eq_congruence — The zero-product property is two-way; substituting back gives 3²=9 and (−3)²=9 (N19, N20).
- S12 · inverse_equivalence · distributive, eq_congruence, add_inverse — Subtracting 9 and adding 9 undo each other, and the expansion is an identity (N18), so the step is two-way.
- S11 · premise_audit · S09, forall_elim, abs_rules — This illustrates the misconception identified in the MKO: √(a²) may not be written as a without conditions; for a<0 they differ (N15 to N17).
- S10 · premise_audit · S09, forall_elim, numeric_evaluation — It needs 49 written as a square (N13); −7 is excluded by the nonnegativity condition (N14 shows its square is also 49).
- S09 · sufficient_goal_reduction · S07, S08, square_nonneg, G2 — Goal G: √(a²)=|a|. Sufficient condition H: a²≥0, |a| is a nonnegative number whose square is a², and such a number is unique; H⇒G by the definition of the principal root. H is proved forwards by square_nonneg, S08 and S07; G is never used as a premise.
- S08.2 · premise_audit · abs_rules, neg_mul, order_basics — |a|=−a needs a<0; the identity (−a)(−a)=a² holds for every a (N11).
- S08.1 · premise_audit · abs_rules, eq_replace — |a|=a is used only in the case a≥0; the other case is S08.2.
- S08 · premise_audit · L_abs_sq, abs_rules, case_analysis — The two cases must cover every real; trichotomy ensures none is missed.
- S07.3 · premise_audit · S07.2, case_analysis, order_basics — Case two is exactly where nonnegativity is used; if y_2<0 were allowed, for example y_1=3 and y_2=−3, case two would hold with y_1≠y_2.
- S07.2 · inverse_equivalence · zero_product — The zero-product property is itself two-way (ℝ is an integral domain).
- S07.1 · inverse_equivalence · distributive, mul_comm, add_inverse, eq_congruence — Subtracting y_2² and adding y_2² undo each other, and the expansion is an identity (N10), so the step is two-way.
- S07 · premise_audit · L_root_unique, G2 — Uniqueness needs the nonnegativity condition; without it, 3 and −3 have equal squares but differ. The converse (equal numbers have equal squares) is obvious and not used.
- S06 · inverse_equivalence · def_unfold, mul_zero — Each equality is the definition or the substitution u·0=0, valid both ways; 0^0=1 may not be used to derive any statement about limits.
- S05 · inverse_equivalence · def_unfold, neg_mul — A replacement of equals, valid both ways; the general sign-alternation statement is not claimed as proved here.
- S04 · inverse_equivalence · def_unfold, neg_mul, mul_comm — A replacement of equals, valid both ways; N3 and N4 recompute it, and N5 confirms −8≠−6.
- S03 · inverse_equivalence · def_unfold, neg_mul — A replacement of equals, valid both ways; N2 recomputes it.
- S02 · inverse_equivalence · def_unfold, mul_one — Each equality replaces an expression by an equal one, and reading backwards returns to (−2)^1; both sides name the same number.
- S01 · premise_audit · G1, mko_power_root — This step only states the definition; every power below is computed from these two clauses alone, with no exponent law assumed.





## Error controls and negative controls

The principal square root is not a ± valueThe first error named in the MKO is to write the principal root as a ± value. The equation y²=9 has two solutions ±3 (S13), but √9 is fixed as the single number 3 by y≥0 and uniqueness (S07, S14). When both solutions are meant, write ±√9; do not say √9 equals ±3.

√(a²)=|a|, not aThe second error named in the MKO is to take √(a²) to be a. For a=−5, √((−5)²)=√25=5=|−5|, while −5 fails y≥0 (S11). Only for a≥0 may one write √(a²)=a.

0^0=1 is an algebraic convention; a^n is not a·nThe third error named in the MKO is to carry 0^0=1 over to limits. The sequence 0^n takes the values 1, 0, 0, 0 and so on, equal to 0 for every n≥1, so its limit is 0, not 1; the value at n=0 is only a convention (S06). Also, (−2)^3=−8, not (−2)·3=−6 (S04).


- √9=±3 → reject — The principal root requires y≥0 and is unique, so √9=3; ±3 are the two solutions of y²=9.
- √((−5)²)=−5 → reject — √((−5)²)=√25=5=|−5|; −5<0 fails the condition for the principal root.
- (−2)³=(−2)·3=−6 → reject — A power multiplies the base repeatedly: (−2)³=4·(−2)=−8≠−6.
- Since 0^0=1, the sequence 0^n has limit 1 → reject — For n≥1, 0^n=0, so the limit is 0; 0^0=1 is an algebraic convention and does not decide limits.
- √(−4)=−2 → reject — (−2)²=4≠−4 and −2<0; no real square equals −4, so √(−4) is undefined in the reals.





## Result and limitations

By the recursion, (−2)^0, (−2)^1, (−2)^2, (−2)^3, (−2)^4 are 1, −2, 4, −8, 16; 0^0=1 (convention) and 0^3=0. A nonnegative square root is unique, and √(a²)=|a| for every real a. Hence √49=7, √((−5)²)=5 (not −5), the solution set of y²=9 is {−3,3} while √9=3, and √(−4) is undefined in the reals.


- This guide proves uniqueness and gives existence for r=a² (take y=|a|). Existence for a general r≥0 (for example r=2) needs the completeness of the reals; it is neither proved nor used here.
- N12 is a finite check for a from −20 to 20 only; the general proof of |a|²=a² is S08.
- Mathlib's Real.sqrt returns 0 on negative input, unlike 'undefined' here; bridging them needs the premise r≥0 (MKO para2) and is outside this guide.





## Verification and source binding

22 declared checks for this guide; only the listed expressions are covered.


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 500af794d5ac8f50bed01f893eca7a76224302cea15cd5ef78efee08f8a81236
- original source SHA-256: 500af794d5ac8f50bed01f893eca7a76224302cea15cd5ef78efee08f8a81236
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-power-root-01.json)