(define square (lambda (n) (if (= n 0) 0 (+ (square ( n 1)) ( (+ n n) 1)))))
The proof  Comments on the proof  

Theorem:For any integer n that is greater
than or equal to 0, (square n)
evaluates to n^{2}.

The mathematical expression n^{2} should be thought of as the
name for some specific number, depending on which specific number
n is. The theorem is just a short hand for an
infinitely long list of claims: that (square 0) evaluates to
0, that (square 1) evaluates to 1, that (square 2)
evaluates to 4, etc.
 
Base case (n = 0): From the code, we see that (square 0) evaluates to 0. Since 0 = 0^{2}, the theorem holds in this
case.
 The base case of the proof verifies that the base case of the code works, and provides a foundation for the induction. We look at the code to see what it does compute, at the theorem to see what it should compute, and use a little math to show that they are equal. In the base case, this is frequently trivial, as here: the code directly tells us what is computed, and the math needed to show equality is just arithmetic.  
Induction hypothesis:
For any integer k that is greater
than or equal to 0 and less than n, assume that (square k)
evaluates to k^{2}.

This is just a copy of the theorem, but with the variable n
renamed to k and the additional restriction that
k<n. If there were multiple variables in the
theorem, they would each be renamed to a new one, and whichever
variable is the one that decreases towards the base case would be the
one we restrict.
Notice that there are two separate restrictions on k. It must be greater than or equal to 0, and it must be less than n. These come from two different sources. The first is copied along with the rest of the theorem. The second is added to ensure that we only rely on smaller cases in our inductive reasoning. Often times (as in the book) we combine these two into a single statement, that k must be in the range from 0 up to (but not including) n. However, don't let that throw you: there are still two different restrictions, coming from two different sources. The induction hypothesis needs to be understood together with the next part of the proof, the inductive step. The two of them together form a statement of the form "If XXX is true, then YYY is true as well." The XXX part is the induction hypothesis, and the YYY part is the inductive step. In this case, "If we assume that numbers smaller than n are correctly squared, then it would follow that n is also correctly squared." Note that this doesn't (yet) take a stand on whether the XXX and YYY are true; both could be false. Only when we put this together with the base case will we see that there is a good reason to conclude that all nonnegative integers are in fact correctly squared.  
Inductive step (n > 0):
Because we are now only considering the case that n is
greater than 0, we know it isn't equal to 0, and can see from
the code that the result will be the result of adding 2n1
to whatever (square ( n 1)) computes. Because n is greater than 0, we know
that n  1 must be greater than or equal to 0. And clearly
n  1 < n. Therefore, we can apply the
induction hypothesis, substituting n  1 for k.
This tells us that (square ( n 1)) evaluates to
(n  1)^{2}. This is what 2n1 then gets added to, producing
(n  1)^{2} + 2n  1.
Doing the algebra,

Notice that we restrict our attention to n > 0, because
the base case has already handled the possibility that n = 0. Just like in the base case, we are again figuring out what the
procedure does compute and comparing that with what it
should compute. This time it is a bit less straightforward,
however, to figure out what the procedure computes, and also to check
for equality with what it should compute.
To figure out what the procedure does compute, we need to rely on the
induction hypothesis. Notice that we first verify that the argument
value (which here is n  1) lies in the range where the
induction hypothesis applies. Having done so, we can substitute the
argument value, n  1, in
place of the induction hypothesis's placeholder variable, k.
If you want to think of a concrete example, suppose we look at the
case where n = 10. We see that (+ (square 9) ( (+ 10 10) 1))We check that 9 is greater than or equal to 0 and less than 10. Since it is, we know we can rely on (square 9) to return 81. Thus the overall result in this
example is 81 + 19, or 100. By expressing our proof in terms of
n and n  1 rather than 10 and 9, we've
handled not only this one specific case, but all the other specific
cases too.
 
Conclusion: By mathematical induction,
(square n)
evaluates to n^{2}, for any integer n that is greater
than or equal to 0.
 This appears to be just a restatement of the theorem, but it also explains why we now believe the theorem to be true: "by mathematical induction." In other words, this is where we bring together the base case (that 0 is correctly squared) with the "if XXX then YYY" combination of induction hypothesis and inductive step (if smaller numbers are correctly squared, then so is n). We see that together, they show that there is a sound chain of reasoning leading to the conclusion that any nonnegative integer is correctly squared. This reasoning is what we call mathematical induction. 
Instructor: Max Hailperin