Freek #12: parallel postulate

Stream: general

[Eric Rodriguez]

I was browsing Freek's list today and noticed that this one isn't in Lean. This should be really easy, by using ℂ as an example for parallel postulate, and constructing a small example that doesn't obey the parallel postulate (I seem to remember a triangle with 6/10 dots through it being a sufficient counterexample! maybe I'm misremembering, though). Is there any nuance to it that I should know before adding it to the issue-tracker as a <good first project>? Do we want to use any of the specific axiomatizations (Tarski, Hilbert, Euclid)? I can't seem to find the HOL-Light version, but the Isabelle seems to use Tarski's axioms.

[Alex J. Best]

I guess https://github.com/jrh13/hol-light/blob/d125b0ae73e546a63ed458a7891f4e14ae0409e2/100/independence.ml is the hol version

[Bhavik Mehta]

Eric Rodriguez said:

I was browsing Freek's list today and noticed that this one isn't in Lean. This should be really easy, by using ℂ as an example for parallel postulate, and constructing a small example that doesn't obey the parallel postulate (I seem to remember a triangle with 6/10 dots through it being a sufficient counterexample! maybe I'm misremembering, though). Is there any nuance to it that I should know before adding it to the issue-tracker as a <good first project>? Do we want to use any of the specific axiomatizations (Tarski, Hilbert, Euclid)? I can't seem to find the HOL-Light version, but the Isabelle seems to use Tarski's axioms.

I looked into this a while ago too, the Isabelle version spends most of its time proving things about the hyperbolic plane using projective planes to deduce that the Tarski axioms all hold on it

[Eric Rodriguez]

Alex J. Best said:

I guess https://github.com/jrh13/hol-light/blob/d125b0ae73e546a63ed458a7891f4e14ae0409e2/100/independence.ml is the hol version

dear god thank god I never did HOL, I cannot read this

[Patrick Massot]

It looks awfully like Fortran, but keep in mind John Harrison is a god of formalized mathematics and we still haven't formalized everything he did alone.

[Stuart Presnell]

Having each tactic line end with THEN gives it the feeling of an excited 5 year old describing the plot of his favourite movie.

[Yury G. Kudryashov]

I've started a file that defines metric space structure on the upper half plane

[Yury G. Kudryashov]

But proving the triangle inequality without the Riemann metric interpretation is a nightmare (or I don't know some trick)

[Yury G. Kudryashov]

I'll pr the part that drops abbreviation tonight. We don't want to use the induced metric anyway

[Yury G. Kudryashov]

@Heather Macbeth @Alex Kontorovich

[Heather Macbeth]

@Yury G. Kudryashov Do we really need a metric interpretation to do this? We need only an abstract definition of geodesic, right?

[Yury G. Kudryashov]

I think that we should have a metric on the your half plane

[Yury G. Kudryashov]

Sooner or later

[Yury G. Kudryashov]

And prove that SL2 acts by isometries

[Yury G. Kudryashov]

(deleted)

[Bhavik Mehta]

https://www.isa-afp.org/entries/Tarskis_Geometry.html is a good place to look at for these things as well, it looks like all the other implementations have been adapted from this one

[Bhavik Mehta]

imo it's notable how much time is spent on actually understanding the real projective plane rather than checking the axioms: if it helps I have a big development of Tarski geometry in Lean (in a not-very-mathlib-friendly-way) which gives around 70% of the things from GeoCoq and certainly all the theorems needed about Tarski for this

[Heather Macbeth]

The most abstract, and therefore possibly the most Lean-friendly, way I know how to do this is to consider the upper half-plane as the projectivization of the positive cone inside Lorentz 3-space.

[Heather Macbeth]

In this case you consider $SL(2,\mathbb{R})$ as being $SO_+(2,1)$, and it's clearer that this acts by isometries.

[Heather Macbeth]

For the metric structure, instead of the projectivization, one chooses a specific choice of representative of each line in the projectivization, the "unit sphere" (really half of a two-sheeted hyperboloid, because of the Lorentz metric)

[Heather Macbeth]

But Tarski's axioms (or, at least, the parallel postulate) are non-metric, right? So we don't need the metric structure to get the Freek list fact.

[Bhavik Mehta]

Heather Macbeth said:

But Tarski's axioms (or, at least, the parallel postulate) are non-metric, right? So we don't need the metric structure to get the Freek list fact.

You don't strictly need it but I think it's helpful: looking at the Isabelle proof outline section 3.2 verifies the first three axioms on any semimetric space, and one of the primitives in Tarski is the congruence relation, which has an interpretation as "cong A B C D iff d(A,B) = d(C,D)". (and just to clarify, metric structure here does mean the distance function and that it's a metric space, and not some other geometry thing and I'm conflating?)

[Heather Macbeth]

We can get the congruence relation from the group action, though. Either from $SL(2, \mathbb{R})$ on the upper half-plane as we have it now, or from the $SO_+(2,1)$ action on the positive cone in my fancier version.

[Heather Macbeth]

Congruence just means one set of points can be transformed to the other by applying some element of the group.

[Bhavik Mehta]

Heather Macbeth said:

We can get the congruence relation from the group action, though. Either from $SL(2, \mathbb{R})$ on the upper half-plane as we have it now, or from the $SO_+(2,1)$ action on the positive cone in my fancier version.

Agreed, and I think that we should define congruence in this way, I only meant to point out that it could be helpful to have the equivalent form in terms of a metric, if the metric is available

[Yury G. Kudryashov]

I have a metric_space instance on the upper_half_plane in #14703.

[Yury G. Kudryashov]

(docs are missing)

[Yury G. Kudryashov]

Fun fact (either I didn't know about it before, or I totally forgot): after trivial manipulations, the triangle inequality for (a b c : ℍ) becomes the Ptolemy's inequality for a b c (conj b) : ℂ.