Hello, I was the author of the new proof.

First of all, I do admit that overwriting the existing proof was a mistake - it is good to have multiple proofs of the same thing in an article. (See the fundamental theorem of algebra article where the same thing gets proven multiple times).

Secondly, to Todd Trimble’s comment; this was not a troll, this was a serious effort that was just poorly executed.

The exponential and natural logarithm functions are real analytic in character: the existence of the former rely on Cauchy completeness of the real numbers and the existence of the latter rely on the inverse function theorem on the domain of the exponential function, or some other definition, like the integral definition or the analytic completion of power series definition, and proofs that they are inverses of each other rely on other theorems of real analysis.

The algebra was an attempt to prove that partial inverses exist of the quadratic functions, but it relied on another property of the exponential and natural logarithm, the fact that exponential and natural logarithm are group isomorphisms between addition on the real numbers and multiplication on the positive real numbers, and I never explicitly mentioned that in my proof. More specifically, given that the exponential function is a group isomorphism from the additive group of real numbers and the multiplicative group of positive real numbers, then

$y = x^2 = x x = \exp(\ln(x)) \exp(\ln(x)) = \exp(\ln(x) + \ln(x)) = \exp(2 \ln(x))$and then one gets $\ln(y) = 2 \ln (x)$ and $\exp\left(\frac{1}{2} \ln(y)\right) = x$, the latter which is the inverse of $x^2$ on the domain $(0, \infty)$ and codomain $(0, \infty)$, and thus we could call it the square root $\mathrm{sqrt}(x)$. The other branch, when $x \lt 0$ for $x \mapsto x^2$, follows from

$y = x^2 = (-x) (-x) = \exp(\ln(-x)) \exp(\ln(-x)) = \exp(\ln(-x) + \ln(-x)) = \exp(2 \ln(-x))$and then one gets $\ln(y) = 2 \ln (-x)$ and $-\exp\left(\frac{1}{2} \ln(y)\right) = x$, which is just the negation of $\mathrm{sqrt}(x)$.

]]>The original proof relies on the inverse function theorem. The subsection titled “In constructive mathematics” needs to state that the quadratic function is analytic or uniformly differentiable or something similar, since a function being continuously differentiable is not enough for the inverse function theorem to apply to the function in constructive mathematics from what i could remember.

]]>I rolled back the changes made by the guest.

Theresa Leba

]]>Well, at this point I expect this is trolling.

]]>I do not think the change in #3 is an improvement.

Two things that are lost by removing the previous contents are:

- Actually justifying the existence of the partial inverses
- Examples of applying the basics of real analysis to rigorously prove things

The first is a critical loss. The latter, I suspect, is a main part of the reason the page was created in the first place.

I do not think it improves clarity to replace all uses of the square root function with a more complicated expression via $\exp$ and $\log$.

And… I’m not sure imprecisely belaboring the high school algebra to solve the functional equation adds any value for the intended audience of this page. I feel like that’s a *lot* of detail spelling out something the reader would already be proficient in (and is still missing the detail to get the logic exactly right).

replaced existing derivation of the real quadratic formula using differential calculus and the inverse function theorem with a conceptually simpler derivation of the quadratic formula using the exponential and natural logarithm and basic algebra

]]>in the first line of *Properties*, I have changed “could be” to “may be” (okay?)

took the liberty of changing “image of $f$” to “value of $f$” (to be pedantic, but let me know if you disagree)

removed the redundant duplicate of the work “Wikipedia”

]]>Page created, but author did not leave any comments.

Anonymous

]]>