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

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

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

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

(-2)^1

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

(-2)^2

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

(-2)^3

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

(-2)^4

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

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

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

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

y_1=y_2

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

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

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

\sqrt{a^2}=|a|

\sqrt{49}

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

\sqrt{(-5)^2}

|-5|=5

y^2=9

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

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

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

\{-3,3\}

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

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

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

Substeps and lemmas

y_1^2=y_2^2

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

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

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

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

y_1=y_2

a\geq 0

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

a<0

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

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 ± value

The 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 a

The 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·n

The 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)