John, your hol_light/Multivariate/geom.ml proofs are amazing, but too
complicated for high school students, and I think we ought to give a nice
formalization of coordinate geometry, especially as the new high school Common
Core Geometry standards might mean doing coordinate geometry and getting rid of
axiomatic proofs. Here's a sketch for how to do this. Part of it is much
trickier than I would like, and maybe you can simplify this.
Let's prove your TRIANGLE_ANGLE_SUM by rigorizing the standard high school
non-rigorous Euclid proof, which I gave a Hilbert formalization as
TriangleSum : thm =
|- ∀A B C. ¬Collinear A B C
⇒ μ (∡ A B C) + μ (∡ B C A) + μ (∡ C A B) = &180
http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGeometry.tar.gz
(more recent than the version you graciously included in subversion 151) where
I borrowed ideas from your geom.ml. Using my notation, we have 3 noncollinear
points A, B & C. We need a line through B parallel to AC with points E & F on
it, and that's easy:
Let v = C - A (the direction vector of AC), and also let
a = B - A and c = B - C. Let
E = B - v and
F = B + v.
We easily get the 2 angle equalities,
EBA = CAB and CBF = BCA, from your vector/acs definition of angle:
cos (CAB) = (v dot a) / (|v| |a|) = cos (EBA)
cos (BCA) = - (c dot v) / (|c| |v|) = cos (CBF)
We need to show something like what I write:
C is in the interior of ABF.
That's really easy with your vectors, because we have a parallelogram ABFC,
where the diagonals intersect at the midpoints
M = A + (1/2)(a + v) = (1/2)(B + C) = (1/2)(A + F)
ABM = ABC and MBF = CBF since M is the midpoint of B & C. Since M is the
midpoint of A & F, we have
between M (A,F).
So far, this is much simpler than my Hilbert proof, because we didn't use any
Hilbert betweenness stuff, needed e.g. for the converse of the Alternate
Interior Angles Theorem. And between M (A,F) implies, by your
ANGLES_ADD_BETWEEN,
ABF = ABM + MBF = ABC + CBF.
That's the only hard part: giving a simple proof of ANGLES_ADD_BETWEEN. Your
proof uses TRIANGLE_ANGLE_SUM, which you prove with your amazing calculation
cos(ABC + BCA + CAB) = -1.
Putting this off, we need supplementary angles to add up to pi,
EBA + ABF = pi.
You have a lot of results like that in geom.ml, e.g. ANGLES_ALONG_LINE, and I
bet this isn't too hard, although I don't understand your proof yet. Now we're
done:
ABC + BCA + CAB = ABC + CBF + EBA = ABF + EBA = pi.
So we must give a simple proof of ANGLES_ADD_BETWEEN. I'll state it like this:
Take 3 our noncollinear points to be O = (0, 0) and two points on the unit
circle, A and B = (1, 0). Let
P = sA + (1 - s)B for some s in (0, 1). Then ANGLES_ADD_BETWEEN says that
angle(A,O,P) + angle(P,O,B) = angle(A,O,B).
We'll need to push P onto the unit circle, so let
X = (1/|P|) P.
Then |X| = 1, and we're proving
angle(A,O,X) + angle(X,O,B) = angle(A,O,B).
I want to define angle by arclength along the unit circle, which specializes to
arc-cos defined by
acs(x) = int_x^1 dt / sqrt{1 - t^2}
when, as in our case, B = (1,0). Your definition of acs using complex
logarithm is too advanced for high school, and maybe it won't work for what I
want anyway. That means we need a new proof of SIN_ADD and COS_ADD, and that's
bound to be harder than your immediate proofs using the complex exponential
function. Well, a more geometric proof using vectors is OK, right?
So angle(A,O,B) = acs(A dot B),
angle(X,O,B) = acs(X dot B).
That makes ANGLES_ADD_BETWEEN almost obvious, but we need a betweenness result
on the unit circle. This requires a result that I found surprisingly hard to
prove. My son read my proof and helped me spot a good number of mistakes. I
think it's fine now, but maybe someone knows a simpler proof.
Lemma:
A dot B < X dot B.
Proof:
Write d = A dot B. |d| < 1 by the usual proof:
1 - d^2 = |A|^2 |B|^2 - d^2 = (a_1^2 + a_2^2)(b_1^2 + b_2^2) - (a_1 b_1 + a_2
b_2)^2
=
a_1^2 b_2^2 + a_2^2 b_1^2 - 2 a_1 b_1a_2 b_2 = (a_1 b_2 - a_2 b_1)^2 > 0
because we're squaring the determinant, which is nonzero because A and B are
linearly independent, since we assumed that A, O & B are non-collinear. Thus
|d| < 1.
So we're proving d < X dot B. Recall
P = sA + (1 - s)B. Then
|P|^2 = s^2 + 2s(1 - s) d + (1 - s)^2,
so
|P|^2 < s^2 + 2s(1 - s) + (1 - s)^2 = (s + 1 - s)^2 = 1
since d < 1. Thus |P| < 1. Since
X dot B = (1/|P|) (s d + 1 - s),
we're proving
|P| d < s d + 1 - s.
We have three cases.
Suppose 0 <= d < 1. We're proving
(|P| - s) d < 1 - s,
but
(|P| - s) d <= (1 - s) d < 1 - s
since d >= 0 and 1 - s > 0.
qed
Suppose d < 0 and s d + 1 - s >= 0. Then
|P| d < 0 <= s d + 1 - s
qed
Suppose d < 0 and s d + 1 - s < 0.
Our result follows from the result of squaring both sides and changing the
inequality
(|P| d)^2 > (s d + 1 - s)^2
And that's
(s^2 + 2 s (1 - s) d + (1 - s)^2) d^2 > s^2 d^2 + 2 s (1 - s) d + (1 - s)^2.
Eliminate the s^2 d^2 terms and divide by (1 - s) to reduce this to
(2 s d + 1 - s) d^2 > 2 s d + 1 - s
This follows from 2 s d + 1 - s < 0, since d^2 < 1. But this is true because
2 s d + 1 - s = s d + (s d + 1 - s) < 0 + 0 = 0.
qed
There must be a simpler or more direct proof, but at least it's an elementary
argument.
By the lemma, A dot B < X dot B, which means
cos(AOB) < cos(XOB).
For convenience, let d = A dot B and e = X dot B. Then d < e < 1, and
AOB = acs(d) =int_d^1 dt / sqrt{1 - t^2}
=
int_d^e dt / sqrt{1 - t^2} + int_e^1 dt / sqrt{1 - t^2}
=
int_d^e dt / sqrt{1 - t^2} + XOB.
But int_d^e dt / sqrt{1 - t^2} = AOX,
because this is the arclength from A to X.
qed
I suppose we'll have to show that our arclength integral definition is
invariant under rotation matrices, i.e. a 2x2 matrix
[p -q]
[q p]
with p^2 + q^2 = 1. This doesn't actually use any properties of sines &
cosines, but only the change of variables theorem for integrals, and the fact
that such a (special orthogonal) matrix preserves the circle.
One would of course like to teach a high school Geometry that doesn't require
Multivariable Calculus, but that's not possible if we insist on rigorous (and
formalizable!) proofs and radian measure. The only definition of radian
measure is the arclength integral, and this intergral is dicier than the usual
integral for the area under a curve, as for nice functions, the area integral
is the maximum of the lower sums and the minimum of the upper sums. So the
area integral sounds like a nice definition. But for the arclength integral,
we don't have upper and lower sums that get squeezed together.
--
Best,
Bill
------------------------------------------------------------------------------
Monitor your physical, virtual and cloud infrastructure from a single
web console. Get in-depth insight into apps, servers, databases, vmware,
SAP, cloud infrastructure, etc. Download 30-day Free Trial.
Pricing starts from $795 for 25 servers or applications!
http://p.sf.net/sfu/zoho_dev2dev_nov
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
