Independence of Playfair's axiom via Euclidean and Klein models

Source: url:https://github.com/Richiesutie/ParallelPostulate/tree/8ee502804263194ae40babeca9773127f1e0a085 Authors: Richard Sutton Status: verified Main declarations: ParallelPostulate.Hilbert.playfair_independent_continuous Tags: synthetic-geometry, hyperbolic-geometry, parallel-postulate, klein-model MSC: 51F15, 51M10, 53A35

Coordinate Euclidean and Klein geometry

Coordinate infrastructure for the models in LeanPool/ParallelPostulate.lean. The dimensions section develops lines over commutative rings and fields. The three-dimensions section proves Euclid's fifth postulate and its angle formulation over ordered fields and the real numbers, respectively. The bounded-plane sections use the domain 0 < 1 + κ * (x² + y²): nonnegative bounds give the whole affine plane, while negative bounds give Klein domains with infinitely many parallels.

The real-coordinate development constructs projective motions, invariant angles and metric, Brioschi curvature, smooth-path distance, and Hilbert congruence constructions. Algebraic and incidence/order results retain their upstream field generality. The explicit leaning figure at bound -1 has interior angles summing to less than π, yet its two lines do not meet.

Scope

• The model is a set of coordinate pairs with lines obtained by intersecting affine lines with the domain. Its identification with other constructions of hyperbolic space is not formalized. Pasch order, congruence, Archimedes continuity, and Dedekind continuity are verified by the constructions in the entry module.
• kleinAngle agrees with Mathlib's Euclidean angle at the origin under every bound, and everywhere at bound zero. Its invariance and uniqueness under the projective motions are proved. Degenerate rays use Mathlib's totalized angle convention.
• kleinMetric is the coordinate bilinear form. Motion invariance uses Mathlib's actual Fréchet derivatives. gaussCurvature is Brioschi's coordinate formula; its identification with connection curvature or surface curvature is not formalized. The formula gives κ throughout the domain and gives -1 for the upper-half-plane metric.
• kleinDist is the infimum of lengths of C1 paths on [0, 1]. Piecewise smooth paths and its identification with Mathlib's Riemannian distance are not formalized. Its closed form and relation to apart are proved for negative bounds.
• The angle counterexample is proved at bound -1; its rescaling to other negative bounds is not formalized. Positive bounds still have the whole affine coordinate plane; the interpretation as a half sphere is not formalized.
• Lean's division is totalized. step_comm, apart_comm, apart_centre, and rot_apart have identical quotients on both sides even at zero denominators. step_neg, apart_self, and shift_axis use division by zero at boundary points. Geometric model results supply domain and nonzero-denominator hypotheses where they are needed.

The upstream labels H11 and H12 concern a larger project and are absent from this development.

Hilbert planes, and the independence of the parallel postulate

HilbertPlane P L is a plane with points P and lines L, a betweenness, and congruence of segments and of angles, that meets Hilbert's axioms of incidence (I1 to I3), of order (B1 to B4) and of congruence (C1 to C6). Playfair's axiom, HilbertPlane.Playfair, is not among them. The axioms of continuity are HilbertPlane.Archimedes and HilbertPlane.Dedekind.

model κ makes a Hilbert plane of the plane of HyperbolicPlane under a bound κ that is not positive: its points and its lines, its Between, apart for segments and kleinAngle for angles. euclidPlane is the bound 0 and kleinPlane the bound -1. Playfair's axiom holds in the first and fails in the second, so it is independent of the axioms of a Hilbert plane: playfair_independent. Both planes meet Archimedes' axiom and Dedekind's axiom, so it is independent of these axioms too: playfair_independent_continuous.

The synthetic definitions are in Hilbert.lean; the model, continuity, and independence proofs are in this entry module. Everything is in the namespace ParallelPostulate.Hilbert.

What is assumed, and what is not formalised

• The axioms of a Hilbert plane, as Hartshorne calls it, are those of incidence, order and congruence. The axioms of continuity are stated apart, as Archimedes and Dedekind, and both planes meet them.
• Dedekind's axiom stands for Hilbert's axiom of completeness. Hilbert's axiom V.2 says that the points of a line cannot be extended while the other axioms still hold. It is a statement about all the models, not an axiom inside one plane. Dedekind's axiom is the usual axiom in its place. That the two are equivalent, given Archimedes' axiom, is not formalised.
• B4 is Pasch's axiom, as Hilbert states it. Hartshorne takes plane separation instead. Given the other axioms the two are equivalent. That is not formalised.
• A segment is a pair of points, and an angle is a triple with its vertex in the middle. The fields seg_swap, ang_swap and ang_rays say that congruence does not see the order of the ends of a segment, the order of the two rays of an angle, or the points chosen on the rays.
• Not in the style of Mathlib. In Mathlib the plane would be built on EuclideanSpace, betweenness would be Sbtw, and Klein's distance would be riemannianEDist.

Three dimensions and the parallel postulate

Three dimensions a, b, c, each a number line with its own zero, and two constraints:

a0 = b0        a1 = c0

So a is the straight line that falls on the two other lines: it meets b where a has its zero, and c where a has its 1.

Checked with Lean v4.35.0-rc3 and Mathlib at the matching tag (September 2026). Every theorem uses only Lean's standard axioms propext, Classical.choice and Quot.sound.

The dimensions, the cross product and the figure, with their small facts, are in the dimensions section, in the namespace Pairs. Some of the names below are there.

Contents

• Lemma E1, read as numbers a1 = c0 collapses a: collapse
• a dimension, its direction, its points, its sides: Dim, Dim.dir, Dim.pt, Dim.points, Dim.side
• the cross product: cross
• the figure, with the two constraints: Figure, Figure.a0_eq_b0, Figure.a1_eq_c0
• Lemma E2, three independent dimensions: skew_of_independent
• Example E3, whole numbers and fractions: wholeFigure_hypotheses, whole_numbers_never_meet, exampleFigure_meets
• Theorem E4, the postulate with no angle: Figure.meet_eq, fifth_postulate, and fifth_postulate_right on the right of a
• Theorem E5, the two other cases: Figure.never_meet_of_two_right_angles, meet_on_the_other_side, meet_on_the_other_side_right
• Theorem E6, exactly when: Figure.meet_unique, meet_on_side_iff, meet_on_side_iff_right
• Theorem E7, Playfair: meet_of_cross_ne_zero, not_meet_of_cross_eq_zero, playfair_exists, playfair_unique, playfair_unique_through
• a dimension with its zero moved: Dim.rebase, Dim.rebase_points, meet_iff_common_point
• Lemma E8, the sine of the two angles together: sin_angle_sum, angle_pos_and_lt_pi
• Theorem E9, the postulate as Euclid states it: euclid_fifth_either_side, never_meet_either_side, other_side_either_side, meet_iff_angles_either_side
• the same on the left of a only: euclid_fifth_general, never_meet_general, other_side_general, meet_on_side_iff_angles
• the figure with a run backwards: Figure.reverse, Figure.reverse_side, Figure.reverse_angles
• Proposition E10, the figure with given angles: angleFigure, angle_at_a0, angle_at_a1, angleFigure_cross, law_of_sines, euclid_fifth, never_meet_of_sum_eq_pi

What is assumed, and what is not formalised

• The postulate is not proved from Euclid's other postulates. That cannot be done: the hyperbolic plane meets the others and fails this one. What is proved is that the plane of pairs of numbers of a field meets the postulate. It does so because of how it is made: adding moves a line to any point without turning it, and two lines of one plane meet if neither direction is a multiple of the other, because the numbers can be divided.
• That this plane meets Euclid's other postulates is not formalised.
• That the plane is built from dimensions is a reading, and is not in Lean. In this file the plane is K × K, and a dimension is any line in it with a zero and a 1.

Read as numbers, a1 = c0 collapses the dimension a

theorem ParallelPostulate.ThreeDimensions.collapse {N : Type u_1} [Add N] (ι : ℤ → N) (hadd : ∀ (m n : ℤ), ι (m + n) = ι m + ι n) (hidem : ι 1 + ι 1 = ι 1) (n : ℤ) : ι n = ι 0

ι n is the number n of the plus world of a. The zero of a dimension is its own double: c0 + c0 = c0. So if a1 is c0, then a1 + a1 = a1. Every number of a is then a0.

Three independent dimensions: the two lines never meet

theorem ParallelPostulate.ThreeDimensions.skew_of_independent {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (O a b c : V) (h : LinearIndependent K ![a, b, c]) (t u : K) : O + t • b ≠ O + a + u • c

a runs from O to O + a. The line b leaves O and the line c leaves O + a. If the three directions are independent, the two lines have no point in common.

The plane

def ParallelPostulate.ThreeDimensions.Meet {K : Type u_1} [CommRing K] (L M : Pairs.Dim K) : Prop

Two dimensions meet.

Equations

• ParallelPostulate.ThreeDimensions.Meet L M = ∃ (t : K) (u : K), L.pt t = M.pt u

theorem ParallelPostulate.ThreeDimensions.meet_iff_common_point {K : Type u_1} [CommRing K] (L M : Pairs.Dim K) : Meet L M ↔ ∃ Q ∈ L.points, Q ∈ M.points

Two dimensions meet exactly when they have a point in common.

With whole numbers the postulate is false

def ParallelPostulate.ThreeDimensions.wholeFigure : Pairs.Figure ℤ

A figure with whole numbers: a from (0, 0) to (1, 0), b towards (1, 1), and c from (1, 0) towards (0, 1).

Equations

• One or more equations did not get rendered due to their size.

theorem ParallelPostulate.ThreeDimensions.wholeFigure_hypotheses : 0 < wholeFigure.a.side wholeFigure.b.one ∧ 0 < wholeFigure.a.side wholeFigure.c.one ∧ 0 < Pairs.cross wholeFigure.b.dir wholeFigure.c.dir

It meets every hypothesis of the postulate.

theorem ParallelPostulate.ThreeDimensions.whole_numbers_never_meet (t u : ℤ) : wholeFigure.b.pt t ≠ wholeFigure.c.pt u

And its two lines never meet. They cross at (1/2, 1/2), between their points.

With fractions

The postulate as Playfair states it

theorem ParallelPostulate.ThreeDimensions.meet_of_cross_ne_zero {K : Type u_1} [Field K] (L M : Pairs.Dim K) (h : Pairs.cross L.dir M.dir ≠ 0) : Meet L M

Two dimensions meet if the cross product of their directions is not zero.

theorem ParallelPostulate.ThreeDimensions.not_meet_of_cross_eq_zero {K : Type u_1} [Field K] (L M : Pairs.Dim K) (hL : L.zero ≠ L.one) (h : Pairs.cross L.dir M.dir = 0) (hP : M.zero ∉ L.points) : ¬Meet L M

A dimension with the direction of L, through a point that is not on L, never meets L.

theorem ParallelPostulate.ThreeDimensions.playfair_exists {K : Type u_1} [Field K] (L : Pairs.Dim K) (hL : L.zero ≠ L.one) (P : K × K) (hP : P ∉ L.points) : ∃ (M : Pairs.Dim K), M.zero = P ∧ M.zero ≠ M.one ∧ ¬Meet L M

Playfair, first half. Through a point that is not on L there is a line that never meets L.

theorem ParallelPostulate.ThreeDimensions.points_subset {K : Type u_1} [Field K] (M M' : Pairs.Dim K) (hP : M.zero = M'.zero) (k : K) (hk : M.dir = (k * M'.dir.1, k * M'.dir.2)) : M.points ⊆ M'.points

If the direction of M is a multiple of the direction of M', and they leave the same point, every point of M is a point of M'.

theorem ParallelPostulate.ThreeDimensions.playfair_unique {K : Type u_1} [Field K] (L M M' : Pairs.Dim K) (hL : L.zero ≠ L.one) (hM : M.zero ≠ M.one) (hM' : M'.zero ≠ M'.one) (hP : M.zero = M'.zero) (h : ¬Meet L M) (h' : ¬Meet L M') : M.points = M'.points

Playfair, second half. Two lines through the same point that never meet L are the same line.

theorem ParallelPostulate.ThreeDimensions.playfair_unique_through {K : Type u_1} [Field K] (L M M' : Pairs.Dim K) (hL : L.zero ≠ L.one) (hM : M.zero ≠ M.one) (hM' : M'.zero ≠ M'.one) {P : K × K} (hP : P ∈ M.points) (hP' : P ∈ M'.points) (h : ¬Meet L M) (h' : ¬Meet L M') : M.points = M'.points

Playfair, second half, for lines through a point. Two lines through the point P that never meet L are the same line, wherever they have their zeros.

The postulate, in the plane over an ordered field

theorem ParallelPostulate.ThreeDimensions.fifth_postulate {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (F : Pairs.Figure K) (hb : 0 < F.a.side F.b.one) (hc : 0 < F.a.side F.c.one) (hsum : 0 < Pairs.cross F.b.dir F.c.dir) : ∃ (t : K) (u : K), 0 < t ∧ 0 < u ∧ F.b.pt t = F.c.pt u ∧ 0 < F.a.side (F.b.pt t)

The parallel postulate, in the plane of the three dimensions.

a falls on b and c. Let b1 and c1 lie on the left of a, and let the two interior angles on that side be together less than two right angles: c is a turn to the left of b. Then b and c, produced on that side, meet on that side. For the right of a see fifth_postulate_right.

theorem ParallelPostulate.ThreeDimensions.meet_on_the_other_side {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (F : Pairs.Figure K) (hb : 0 < F.a.side F.b.one) (hc : 0 < F.a.side F.c.one) (hsum : Pairs.cross F.b.dir F.c.dir < 0) : ∃ (t : K) (u : K), t < 0 ∧ u < 0 ∧ F.b.pt t = F.c.pt u ∧ F.a.side (F.b.pt t) < 0

More than two right angles: the lines meet on the other side.

theorem ParallelPostulate.ThreeDimensions.meet_on_side_iff {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (F : Pairs.Figure K) (hb : 0 < F.a.side F.b.one) (hc : 0 < F.a.side F.c.one) : (∃ (t : K) (u : K), 0 < t ∧ 0 < u ∧ F.b.pt t = F.c.pt u) ↔ 0 < Pairs.cross F.b.dir F.c.dir

Exactly when. The lines b and c meet on the side of b1 and c1 exactly when c is a turn to the left of b.

theorem ParallelPostulate.ThreeDimensions.fifth_postulate_right {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (F : Pairs.Figure K) (hb : F.a.side F.b.one < 0) (hc : F.a.side F.c.one < 0) (hsum : Pairs.cross F.b.dir F.c.dir < 0) : ∃ (t : K) (u : K), 0 < t ∧ 0 < u ∧ F.b.pt t = F.c.pt u ∧ F.a.side (F.b.pt t) < 0

The postulate on the other side of a. If b1 and c1 lie on the right of a, and c is a turn to the right of b, the lines meet on the right of a.

theorem ParallelPostulate.ThreeDimensions.meet_on_the_other_side_right {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (F : Pairs.Figure K) (hb : F.a.side F.b.one < 0) (hc : F.a.side F.c.one < 0) (hsum : 0 < Pairs.cross F.b.dir F.c.dir) : ∃ (t : K) (u : K), t < 0 ∧ u < 0 ∧ F.b.pt t = F.c.pt u ∧ 0 < F.a.side (F.b.pt t)

More than two right angles, on the right of a: the lines meet on the left of a.

theorem ParallelPostulate.ThreeDimensions.meet_on_side_iff_right {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (F : Pairs.Figure K) (hb : F.a.side F.b.one < 0) (hc : F.a.side F.c.one < 0) : (∃ (t : K) (u : K), 0 < t ∧ 0 < u ∧ F.b.pt t = F.c.pt u) ↔ Pairs.cross F.b.dir F.c.dir < 0

Exactly when, on the other side.

def ParallelPostulate.ThreeDimensions.exampleFigure : Pairs.Figure ℚ

The figure of wholeFigure, with fractions in the dimensions.

Equations

• One or more equations did not get rendered due to their size.

theorem ParallelPostulate.ThreeDimensions.exampleFigure_meets : 0 < exampleFigure.a.side exampleFigure.b.one ∧ 0 < exampleFigure.a.side exampleFigure.c.one ∧ 0 < Pairs.cross exampleFigure.b.dir exampleFigure.c.dir ∧ exampleFigure.b.pt (1 / 2) = (1 / 2, 1 / 2) ∧ exampleFigure.c.pt (1 / 2) = (1 / 2, 1 / 2)

It meets every hypothesis of the postulate, and its two lines meet at (1/2, 1/2).

The figure with given angles

noncomputable def ParallelPostulate.ThreeDimensions.angleFigure (β γ : ℝ) : Pairs.Figure ℝ

The figure with a from (0, 0) to (1, 0). The line b leaves a0 at the angle β to a. The line c leaves a1 at the angle γ to a run backwards. So β and γ are the two interior angles on the upper side of a.

Equations

• One or more equations did not get rendered due to their size.

theorem ParallelPostulate.ThreeDimensions.angleFigure_side_b (β γ : ℝ) : (angleFigure β γ).a.side (angleFigure β γ).b.one = Real.sin β

theorem ParallelPostulate.ThreeDimensions.angleFigure_side_c (β γ : ℝ) : (angleFigure β γ).a.side (angleFigure β γ).c.one = Real.sin γ

theorem ParallelPostulate.ThreeDimensions.angleFigure_cross (β γ : ℝ) : Pairs.cross (angleFigure β γ).b.dir (angleFigure β γ).c.dir = Real.sin (β + γ)

theorem ParallelPostulate.ThreeDimensions.euclid_fifth (β γ : ℝ) (hβ : 0 < β) (hγ : 0 < γ) (h : β + γ < Real.pi) : ∃ (t : ℝ) (u : ℝ), 0 < t ∧ 0 < u ∧ (angleFigure β γ).b.pt t = (angleFigure β γ).c.pt u ∧ 0 < (angleFigure β γ).a.side ((angleFigure β γ).b.pt t)

Euclid's fifth postulate, for the figure with the angles β and γ. If the two interior angles on the upper side of a are together less than two right angles, the lines b and c, produced on that side, meet on that side.

theorem ParallelPostulate.ThreeDimensions.law_of_sines (β γ : ℝ) (h : Real.sin (β + γ) ≠ 0) : (angleFigure β γ).b.pt (Real.sin γ / Real.sin (β + γ)) = (angleFigure β γ).c.pt (Real.sin β / Real.sin (β + γ))

Where they meet: the law of sines. The point is at the number sin γ / sin (β + γ) of b, and at the number sin β / sin (β + γ) of c.

theorem ParallelPostulate.ThreeDimensions.never_meet_of_sum_eq_pi (β γ : ℝ) (hγ : 0 < γ) (hγ' : γ < Real.pi) (h : β + γ = Real.pi) (t u : ℝ) : (angleFigure β γ).b.pt t ≠ (angleFigure β γ).c.pt u

Two right angles: the lines never meet.

The angles are angles in Mathlib's sense

noncomputable def ParallelPostulate.ThreeDimensions.toE (p : ℝ × ℝ) : EuclideanSpace ℝ (Fin 2)

A direction of the plane of the three dimensions, as a vector of Mathlib's Euclidean plane.

Equations

• ParallelPostulate.ThreeDimensions.toE p = !₂[p.1, p.2]

theorem ParallelPostulate.ThreeDimensions.inner_toE (p q : ℝ × ℝ) : inner ℝ (toE p) (toE q) = p.1 * q.1 + p.2 * q.2

theorem ParallelPostulate.ThreeDimensions.norm_toE (p : ℝ × ℝ) : ‖toE p‖ = √(p.1 ^ 2 + p.2 ^ 2)

theorem ParallelPostulate.ThreeDimensions.norm_toE_sq (p : ℝ × ℝ) : ‖toE p‖ ^ 2 = p.1 ^ 2 + p.2 ^ 2

theorem ParallelPostulate.ThreeDimensions.norm_toE_neg (p : ℝ × ℝ) : ‖toE (-p)‖ = ‖toE p‖

theorem ParallelPostulate.ThreeDimensions.angle_at_a0 (β γ : ℝ) (h0 : 0 ≤ β) (hπ : β ≤ Real.pi) : InnerProductGeometry.angle (toE (angleFigure β γ).a.dir) (toE (angleFigure β γ).b.dir) = β

The interior angle at a0, between a and b, is β.

theorem ParallelPostulate.ThreeDimensions.angle_at_a1 (β γ : ℝ) (h0 : 0 ≤ γ) (hπ : γ ≤ Real.pi) : InnerProductGeometry.angle (toE (-(angleFigure β γ).a.dir)) (toE (angleFigure β γ).c.dir) = γ

The interior angle at a1, between a run backwards and c, is γ.

Any figure in the real plane

theorem ParallelPostulate.ThreeDimensions.cos_angle_toE (p q : ℝ × ℝ) : Real.cos (InnerProductGeometry.angle (toE p) (toE q)) * (‖toE p‖ * ‖toE q‖) = p.1 * q.1 + p.2 * q.2

theorem ParallelPostulate.ThreeDimensions.sin_angle_toE (p q : ℝ × ℝ) : Real.sin (InnerProductGeometry.angle (toE p) (toE q)) * (‖toE p‖ * ‖toE q‖) = |Pairs.cross p q|

theorem ParallelPostulate.ThreeDimensions.normSq_pos_left {p q : ℝ × ℝ} (h : Pairs.cross p q ≠ 0) : 0 < p.1 ^ 2 + p.2 ^ 2

theorem ParallelPostulate.ThreeDimensions.normSq_pos_right {p q : ℝ × ℝ} (h : Pairs.cross p q ≠ 0) : 0 < q.1 ^ 2 + q.2 ^ 2

theorem ParallelPostulate.ThreeDimensions.norm_toE_pos_left {p q : ℝ × ℝ} (h : Pairs.cross p q ≠ 0) : 0 < ‖toE p‖

theorem ParallelPostulate.ThreeDimensions.norm_toE_pos_right {p q : ℝ × ℝ} (h : Pairs.cross p q ≠ 0) : 0 < ‖toE q‖

theorem ParallelPostulate.ThreeDimensions.angle_pos_and_lt_pi {p q : ℝ × ℝ} (h : Pairs.cross p q ≠ 0) : 0 < InnerProductGeometry.angle (toE p) (toE q) ∧ InnerProductGeometry.angle (toE p) (toE q) < Real.pi

Two directions whose cross product is not zero make an angle that is more than nothing and less than two right angles.

theorem ParallelPostulate.ThreeDimensions.sin_angle_sum (a b c : ℝ × ℝ) (hab : 0 < Pairs.cross a b) (hac : 0 < Pairs.cross a c) : Real.sin (InnerProductGeometry.angle (toE a) (toE b) + InnerProductGeometry.angle (toE (-a)) (toE c)) * (‖toE b‖ * ‖toE c‖) = Pairs.cross b c

The sine of the two interior angles together. a is the direction of the line that falls on the two others, and b and c are the directions of the two others, both to the left of a. With β the angle from a to b, and γ the angle from a run backwards to c:

sin (β + γ) · |b| · |c| = cross b c . 

theorem ParallelPostulate.Pairs.Figure.angle_facts (F : Figure ℝ) (hb : 0 < F.a.side F.b.one) (hc : 0 < F.a.side F.c.one) : Real.sin (InnerProductGeometry.angle (ThreeDimensions.toE F.a.dir) (ThreeDimensions.toE F.b.dir) + InnerProductGeometry.angle (ThreeDimensions.toE (-F.a.dir)) (ThreeDimensions.toE F.c.dir)) * (‖ThreeDimensions.toE F.b.dir‖ * ‖ThreeDimensions.toE F.c.dir‖) = cross F.b.dir F.c.dir ∧ 0 < ‖ThreeDimensions.toE F.b.dir‖ * ‖ThreeDimensions.toE F.c.dir‖ ∧ 0 < InnerProductGeometry.angle (ThreeDimensions.toE F.a.dir) (ThreeDimensions.toE F.b.dir) ∧ InnerProductGeometry.angle (ThreeDimensions.toE F.a.dir) (ThreeDimensions.toE F.b.dir) < Real.pi ∧ 0 < InnerProductGeometry.angle (ThreeDimensions.toE (-F.a.dir)) (ThreeDimensions.toE F.c.dir) ∧ InnerProductGeometry.angle (ThreeDimensions.toE (-F.a.dir)) (ThreeDimensions.toE F.c.dir) < Real.pi

What the two interior angles of a figure say, gathered.

theorem ParallelPostulate.ThreeDimensions.cross_pos_of_angles (F : Pairs.Figure ℝ) (hb : 0 < F.a.side F.b.one) (hc : 0 < F.a.side F.c.one) (hang : InnerProductGeometry.angle (toE F.a.dir) (toE F.b.dir) + InnerProductGeometry.angle (toE (-F.a.dir)) (toE F.c.dir) < Real.pi) : 0 < Pairs.cross F.b.dir F.c.dir

Less than two right angles: c is a turn to the left of b.

theorem ParallelPostulate.ThreeDimensions.cross_eq_zero_of_angles (F : Pairs.Figure ℝ) (hb : 0 < F.a.side F.b.one) (hc : 0 < F.a.side F.c.one) (hang : InnerProductGeometry.angle (toE F.a.dir) (toE F.b.dir) + InnerProductGeometry.angle (toE (-F.a.dir)) (toE F.c.dir) = Real.pi) : Pairs.cross F.b.dir F.c.dir = 0

Two right angles: the cross product of the directions of b and c is zero.

theorem ParallelPostulate.ThreeDimensions.cross_neg_of_angles (F : Pairs.Figure ℝ) (hb : 0 < F.a.side F.b.one) (hc : 0 < F.a.side F.c.one) (hang : Real.pi < InnerProductGeometry.angle (toE F.a.dir) (toE F.b.dir) + InnerProductGeometry.angle (toE (-F.a.dir)) (toE F.c.dir)) : Pairs.cross F.b.dir F.c.dir < 0

More than two right angles: c is a turn to the right of b.

theorem ParallelPostulate.ThreeDimensions.euclid_fifth_general (F : Pairs.Figure ℝ) (hb : 0 < F.a.side F.b.one) (hc : 0 < F.a.side F.c.one) (hang : InnerProductGeometry.angle (toE F.a.dir) (toE F.b.dir) + InnerProductGeometry.angle (toE (-F.a.dir)) (toE F.c.dir) < Real.pi) : ∃ (t : ℝ) (u : ℝ), 0 < t ∧ 0 < u ∧ F.b.pt t = F.c.pt u ∧ 0 < F.a.side (F.b.pt t)

Euclid's fifth postulate, on the left of a, for any figure in the real plane. The angles are angles in Mathlib's sense. If b1 and c1 lie on the left of a, and the two interior angles on that side are together less than two right angles, then b and c meet on that side. For either side see euclid_fifth_either_side.

theorem ParallelPostulate.ThreeDimensions.never_meet_general (F : Pairs.Figure ℝ) (hb : 0 < F.a.side F.b.one) (hc : 0 < F.a.side F.c.one) (hang : InnerProductGeometry.angle (toE F.a.dir) (toE F.b.dir) + InnerProductGeometry.angle (toE (-F.a.dir)) (toE F.c.dir) = Real.pi) (t u : ℝ) : F.b.pt t ≠ F.c.pt u

Two right angles, with b1 and c1 on the left of a, for any figure in the real plane: the lines never meet. For either side see never_meet_either_side.

theorem ParallelPostulate.ThreeDimensions.other_side_general (F : Pairs.Figure ℝ) (hb : 0 < F.a.side F.b.one) (hc : 0 < F.a.side F.c.one) (hang : Real.pi < InnerProductGeometry.angle (toE F.a.dir) (toE F.b.dir) + InnerProductGeometry.angle (toE (-F.a.dir)) (toE F.c.dir)) : ∃ (t : ℝ) (u : ℝ), t < 0 ∧ u < 0 ∧ F.b.pt t = F.c.pt u ∧ F.a.side (F.b.pt t) < 0

More than two right angles, with b1 and c1 on the left of a, for any figure in the real plane: the lines meet on the right of a. For either side see other_side_either_side.

theorem ParallelPostulate.ThreeDimensions.meet_on_side_iff_angles (F : Pairs.Figure ℝ) (hb : 0 < F.a.side F.b.one) (hc : 0 < F.a.side F.c.one) : (∃ (t : ℝ) (u : ℝ), 0 < t ∧ 0 < u ∧ F.b.pt t = F.c.pt u) ↔ InnerProductGeometry.angle (toE F.a.dir) (toE F.b.dir) + InnerProductGeometry.angle (toE (-F.a.dir)) (toE F.c.dir) < Real.pi

The postulate and its converse. In the real plane, the lines b and c meet on the side of b1 and c1 exactly when the two interior angles on that side are together less than two right angles.

Either side of a

theorem ParallelPostulate.Pairs.Figure.reverse_angles (F : Figure ℝ) : InnerProductGeometry.angle (ThreeDimensions.toE F.reverse.a.dir) (ThreeDimensions.toE F.reverse.b.dir) + InnerProductGeometry.angle (ThreeDimensions.toE (-F.reverse.a.dir)) (ThreeDimensions.toE F.reverse.c.dir) = InnerProductGeometry.angle (ThreeDimensions.toE F.a.dir) (ThreeDimensions.toE F.b.dir) + InnerProductGeometry.angle (ThreeDimensions.toE (-F.a.dir)) (ThreeDimensions.toE F.c.dir)

The two interior angles of the figure with a run backwards are the two interior angles of the figure, in the other order.

theorem ParallelPostulate.ThreeDimensions.euclid_fifth_right (F : Pairs.Figure ℝ) (hb : F.a.side F.b.one < 0) (hc : F.a.side F.c.one < 0) (hang : InnerProductGeometry.angle (toE F.a.dir) (toE F.b.dir) + InnerProductGeometry.angle (toE (-F.a.dir)) (toE F.c.dir) < Real.pi) : ∃ (t : ℝ) (u : ℝ), 0 < t ∧ 0 < u ∧ F.b.pt t = F.c.pt u ∧ F.a.side (F.b.pt t) < 0

Euclid's fifth postulate on the right of a.

theorem ParallelPostulate.ThreeDimensions.euclid_fifth_either_side (F : Pairs.Figure ℝ) (hside : 0 < F.a.side F.b.one * F.a.side F.c.one) (hang : InnerProductGeometry.angle (toE F.a.dir) (toE F.b.dir) + InnerProductGeometry.angle (toE (-F.a.dir)) (toE F.c.dir) < Real.pi) : ∃ (t : ℝ) (u : ℝ), 0 < t ∧ 0 < u ∧ F.b.pt t = F.c.pt u ∧ 0 < F.a.side (F.b.pt t) * F.a.side F.b.one

Euclid's fifth postulate, in the real plane, on either side. If b1 and c1 lie on the same side of a, and the two interior angles on that side are together less than two right angles, then b and c meet on that side.

theorem ParallelPostulate.ThreeDimensions.never_meet_either_side (F : Pairs.Figure ℝ) (hside : 0 < F.a.side F.b.one * F.a.side F.c.one) (hang : InnerProductGeometry.angle (toE F.a.dir) (toE F.b.dir) + InnerProductGeometry.angle (toE (-F.a.dir)) (toE F.c.dir) = Real.pi) (t u : ℝ) : F.b.pt t ≠ F.c.pt u

Two right angles, on either side: the lines never meet.

theorem ParallelPostulate.ThreeDimensions.other_side_either_side (F : Pairs.Figure ℝ) (hside : 0 < F.a.side F.b.one * F.a.side F.c.one) (hang : Real.pi < InnerProductGeometry.angle (toE F.a.dir) (toE F.b.dir) + InnerProductGeometry.angle (toE (-F.a.dir)) (toE F.c.dir)) : ∃ (t : ℝ) (u : ℝ), t < 0 ∧ u < 0 ∧ F.b.pt t = F.c.pt u ∧ F.a.side (F.b.pt t) * F.a.side F.b.one < 0

More than two right angles, on either side: the lines meet on the other side.

theorem ParallelPostulate.ThreeDimensions.meet_iff_angles_either_side (F : Pairs.Figure ℝ) (hside : 0 < F.a.side F.b.one * F.a.side F.c.one) : (∃ (t : ℝ) (u : ℝ), 0 < t ∧ 0 < u ∧ F.b.pt t = F.c.pt u) ↔ InnerProductGeometry.angle (toE F.a.dir) (toE F.b.dir) + InnerProductGeometry.angle (toE (-F.a.dir)) (toE F.c.dir) < Real.pi

The postulate and its converse, on either side. In the real plane, let b1 and c1 lie on the same side of a. The lines b and c, produced towards b1 and c1, meet exactly when the two interior angles on that side are together less than two right angles.

Steps and motions

What becomes of adding under a bound: the step step κ t u = (t + u) / (1 - κ t u), the motion along the first axis shift, turning rot, and apart, a number that both motions keep.

Contents

• Proposition H8, steps: step, step_zero_bound, step_comm, step_zero_right, step_neg, within_zero, within_neg, step_den_pos, step_within, step_assoc, step_bound, step_edge, step_edge_self
• Theorem H9, the motion along the first axis: shift, shift_zero_bound, shift_centre, shift_axis, shift_den_pos, shift_bound, shift_mem_plane, shift_shift_neg, shift_neg_shift, shift_bijOn, shift_cross, shift_isLine, shift_keeps_left, shift_apart, shift_apart_plane
• Theorem H9, turning: rot, rot_rot_neg, rot_bound, rot_mem_plane, rot_bijOn, rot_pt, rot_isLine, rot_cross, rot_apart
• Theorem H9, how far apart: apart, apart_zero_bound, apart_self, apart_comm, apart_centre, apart_pos
• the algebra of the motions, with the divisions taken out: cross_aux, apart_aux, apart_aux'

What becomes of adding: steps and motions

def ParallelPostulate.HyperbolicPlane.step {K : Type u_1} [Field K] (κ t u : K) : K

The step. Under the bound κ, the number t and then the number u, along a dimension through (0, 0).

Equations

• ParallelPostulate.HyperbolicPlane.step κ t u = (t + u) / (1 - κ * t * u)

theorem ParallelPostulate.HyperbolicPlane.step_zero_bound {K : Type u_1} [Field K] (t u : K) : step 0 t u = t + u

With the bound 0 a step is a sum.

theorem ParallelPostulate.HyperbolicPlane.step_comm {K : Type u_1} [Field K] (κ t u : K) : step κ t u = step κ u t

theorem ParallelPostulate.HyperbolicPlane.step_zero_right {K : Type u_1} [Field K] (κ t : K) : step κ t 0 = t

theorem ParallelPostulate.HyperbolicPlane.step_neg {K : Type u_1} [Field K] (κ t : K) : step κ t (-t) = 0

theorem ParallelPostulate.HyperbolicPlane.step_bound {K : Type u_1} [Field K] {κ t u : K} (h : 1 - κ * t * u ≠ 0) : 1 + κ * step κ t u ^ 2 = (1 + κ * t ^ 2) * (1 + κ * u ^ 2) / (1 - κ * t * u) ^ 2

The bound at a step.

theorem ParallelPostulate.HyperbolicPlane.step_edge {K : Type u_1} [Field K] {κ e t : K} (he : 1 + κ * e ^ 2 = 0) (h : 1 - κ * e * t ≠ 0) : step κ e t = e

A number on the edge swallows every step.

def ParallelPostulate.HyperbolicPlane.shift {K : Type u_1} [Field K] (κ a w : K) (p : K × K) : K × K

The motion along the first axis that takes (0, 0) to the number a of that axis. Here w is a number with w² = 1 + κ a².

Equations

• ParallelPostulate.HyperbolicPlane.shift κ a w p = ((p.1 + a) / (1 - κ * a * p.1), w * p.2 / (1 - κ * a * p.1))

theorem ParallelPostulate.HyperbolicPlane.shift_zero_bound {K : Type u_1} [Field K] (a : K) (p : K × K) : shift 0 a 1 p = (p.1 + a, p.2)

With the bound 0 the motion is adding.

theorem ParallelPostulate.HyperbolicPlane.shift_centre {K : Type u_1} [Field K] (κ a w : K) : shift κ a w (0, 0) = (a, 0)

theorem ParallelPostulate.HyperbolicPlane.shift_axis {K : Type u_1} [Field K] (κ a w t : K) : shift κ a w (t, 0) = (step κ t a, 0)

On the first axis the motion is the step.

theorem ParallelPostulate.HyperbolicPlane.shift_bound {K : Type u_1} [Field K] {κ a w : K} (hw : w ^ 2 = 1 + κ * a ^ 2) {p : K × K} (hD : 1 - κ * a * p.1 ≠ 0) : 1 + κ * ((shift κ a w p).1 ^ 2 + (shift κ a w p).2 ^ 2) = w ^ 2 * (1 + κ * (p.1 ^ 2 + p.2 ^ 2)) / (1 - κ * a * p.1) ^ 2

The bound at the pair to which a pair is moved.

theorem ParallelPostulate.HyperbolicPlane.shift_shift_neg {K : Type u_1} [Field K] {κ a w : K} (hw : w ^ 2 = 1 + κ * a ^ 2) (hw0 : w ≠ 0) {p : K × K} (hD : 1 - κ * a * p.1 ≠ 0) : shift κ (-a) w (shift κ a w p) = p

The motion back.

theorem ParallelPostulate.HyperbolicPlane.cross_aux {K : Type u_1} [Field K] (κ a w xA yA xB yB xC yC XA YA XB YB XC YC : K) (hXA : XA * (1 - κ * a * xA) = xA + a) (hYA : YA * (1 - κ * a * xA) = w * yA) (hXB : XB * (1 - κ * a * xB) = xB + a) (hYB : YB * (1 - κ * a * xB) = w * yB) (hXC : XC * (1 - κ * a * xC) = xC + a) (hYC : YC * (1 - κ * a * xC) = w * yC) : ((XB - XA) * (YC - YA) - (YB - YA) * (XC - XA)) * ((1 - κ * a * xA) * (1 - κ * a * xB) * (1 - κ * a * xC)) = w * (1 + κ * a ^ 2) * ((xB - xA) * (yC - yA) - (yB - yA) * (xC - xA))

The algebra of the next theorem, with the divisions taken out.

theorem ParallelPostulate.HyperbolicPlane.shift_cross {K : Type u_1} [Field K] (κ a w : K) {A B C : K × K} (hA : 1 - κ * a * A.1 ≠ 0) (hB : 1 - κ * a * B.1 ≠ 0) (hC : 1 - κ * a * C.1 ≠ 0) : Pairs.cross ((shift κ a w B).1 - (shift κ a w A).1, (shift κ a w B).2 - (shift κ a w A).2) ((shift κ a w C).1 - (shift κ a w A).1, (shift κ a w C).2 - (shift κ a w A).2) = w * (1 + κ * a ^ 2) * Pairs.cross (B.1 - A.1, B.2 - A.2) (C.1 - A.1, C.2 - A.2) / ((1 - κ * a * A.1) * (1 - κ * a * B.1) * (1 - κ * a * C.1))

A motion keeps three pairs of a dimension on a dimension. If w (1 + κ a²) is not zero, it keeps three pairs that are not on one dimension off it as well.

def ParallelPostulate.HyperbolicPlane.apart {K : Type u_1} [Field K] (κ : K) (P Q : K × K) : K

How far apart two pairs are, under the bound κ.

Equations

• ParallelPostulate.HyperbolicPlane.apart κ P Q = ((P.1 - Q.1) ^ 2 + (P.2 - Q.2) ^ 2 + κ * (P.1 * Q.2 - P.2 * Q.1) ^ 2) / ((1 + κ * (P.1 ^ 2 + P.2 ^ 2)) * (1 + κ * (Q.1 ^ 2 + Q.2 ^ 2)))

theorem ParallelPostulate.HyperbolicPlane.apart_zero_bound {K : Type u_1} [Field K] (P Q : K × K) : apart 0 P Q = (P.1 - Q.1) ^ 2 + (P.2 - Q.2) ^ 2

With the bound 0 it is the square of Euclid's distance.

theorem ParallelPostulate.HyperbolicPlane.apart_self {K : Type u_1} [Field K] (κ : K) (P : K × K) : apart κ P P = 0

theorem ParallelPostulate.HyperbolicPlane.apart_comm {K : Type u_1} [Field K] (κ : K) (P Q : K × K) : apart κ P Q = apart κ Q P

theorem ParallelPostulate.HyperbolicPlane.apart_centre {K : Type u_1} [Field K] (κ t : K) : apart κ (0, 0) (t, 0) = t ^ 2 / (1 + κ * t ^ 2)

From (0, 0) to the number t of the first axis.

theorem ParallelPostulate.HyperbolicPlane.apart_aux {K : Type u_1} [Field K] (κ a w xP yP xQ yQ XP YP XQ YQ : K) (hw : w ^ 2 = 1 + κ * a ^ 2) (hXP : XP * (1 - κ * a * xP) = xP + a) (hYP : YP * (1 - κ * a * xP) = w * yP) (hXQ : XQ * (1 - κ * a * xQ) = xQ + a) (hYQ : YQ * (1 - κ * a * xQ) = w * yQ) : ((XP - XQ) ^ 2 + (YP - YQ) ^ 2 + κ * (XP * YQ - YP * XQ) ^ 2) * ((1 - κ * a * xP) ^ 2 * (1 - κ * a * xQ) ^ 2) = w ^ 4 * ((xP - xQ) ^ 2 + (yP - yQ) ^ 2 + κ * (xP * yQ - yP * xQ) ^ 2)

The algebra of the next theorem, with the divisions taken out.

theorem ParallelPostulate.HyperbolicPlane.apart_aux' {K : Type u_1} [Field K] (N N' BP BQ VP VQ DP DQ w : K) (hw : w ≠ 0) (hDP : DP ≠ 0) (hDQ : DQ ≠ 0) (hBP : BP ≠ 0) (hBQ : BQ ≠ 0) (hN : N' * (DP ^ 2 * DQ ^ 2) = w ^ 4 * N) (hVP : VP * DP ^ 2 = w ^ 2 * BP) (hVQ : VQ * DQ ^ 2 = w ^ 2 * BQ) : N' / (VP * VQ) = N / (BP * BQ)

The last step of the next theorem.

theorem ParallelPostulate.HyperbolicPlane.shift_apart {K : Type u_1} [Field K] {κ a w : K} (hw : w ^ 2 = 1 + κ * a ^ 2) (hw0 : w ≠ 0) {P Q : K × K} (hDP : 1 - κ * a * P.1 ≠ 0) (hDQ : 1 - κ * a * Q.1 ≠ 0) (hP : 1 + κ * (P.1 ^ 2 + P.2 ^ 2) ≠ 0) (hQ : 1 + κ * (Q.1 ^ 2 + Q.2 ^ 2) ≠ 0) : apart κ (shift κ a w P) (shift κ a w Q) = apart κ P Q

The motion along the first axis keeps how far apart two pairs are.

def ParallelPostulate.HyperbolicPlane.rot {K : Type u_1} [Field K] (c s : K) (p : K × K) : K × K

Turning about (0, 0). Here c and s are numbers with c² + s² = 1.

Equations

• ParallelPostulate.HyperbolicPlane.rot c s p = (c * p.1 - s * p.2, s * p.1 + c * p.2)

theorem ParallelPostulate.HyperbolicPlane.rot_rot_neg {K : Type u_1} [Field K] {c s : K} (h : c ^ 2 + s ^ 2 = 1) (p : K × K) : rot c (-s) (rot c s p) = p

Turning back.

theorem ParallelPostulate.HyperbolicPlane.rot_bound {K : Type u_1} [Field K] {c s : K} (h : c ^ 2 + s ^ 2 = 1) (κ : K) (p : K × K) : 1 + κ * ((rot c s p).1 ^ 2 + (rot c s p).2 ^ 2) = 1 + κ * (p.1 ^ 2 + p.2 ^ 2)

Turning keeps the bound of a pair.

theorem ParallelPostulate.HyperbolicPlane.rot_apart {K : Type u_1} [Field K] {c s : K} (h : c ^ 2 + s ^ 2 = 1) (κ : K) (P Q : K × K) : apart κ (rot c s P) (rot c s Q) = apart κ P Q

Turning keeps how far apart two pairs are.

theorem ParallelPostulate.HyperbolicPlane.rot_cross {K : Type u_1} [Field K] {c s : K} (h : c ^ 2 + s ^ 2 = 1) (A B C : K × K) : Pairs.cross ((rot c s B).1 - (rot c s A).1, (rot c s B).2 - (rot c s A).2) ((rot c s C).1 - (rot c s A).1, (rot c s C).2 - (rot c s A).2) = Pairs.cross (B.1 - A.1, B.2 - A.2) (C.1 - A.1, C.2 - A.2)

Turning keeps left and right: it keeps the cross product.

theorem ParallelPostulate.HyperbolicPlane.rot_pt {K : Type u_1} [Field K] (c s : K) (M : Pairs.Dim K) (t : K) : rot c s (M.pt t) = { zero := rot c s M.zero, one := rot c s M.one }.pt t

Turning takes the numbers of a dimension to the numbers of a dimension.

theorem ParallelPostulate.HyperbolicPlane.step_den_pos {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {κ t u : K} (hκ : κ ≤ 0) (ht : 0 < 1 + κ * t ^ 2) (hu : 0 < 1 + κ * u ^ 2) : 0 < 1 - κ * t * u

Under a bound that is not positive, two numbers within the bound have a step.

theorem ParallelPostulate.HyperbolicPlane.step_within {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {κ t u : K} (hκ : κ ≤ 0) (ht : 0 < 1 + κ * t ^ 2) (hu : 0 < 1 + κ * u ^ 2) : 0 < 1 + κ * step κ t u ^ 2

The step of two numbers within the bound is within the bound.

theorem ParallelPostulate.HyperbolicPlane.within_neg {K : Type u_1} [Field K] [LinearOrder K] {κ t : K} (ht : 0 < 1 + κ * t ^ 2) : 0 < 1 + κ * (-t) ^ 2

The step back of a number within the bound is within the bound.

theorem ParallelPostulate.HyperbolicPlane.within_zero {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (κ : K) : 0 < 1 + κ * 0 ^ 2

The zero is within the bound.

theorem ParallelPostulate.HyperbolicPlane.step_assoc {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {κ t u v : K} (hκ : κ ≤ 0) (ht : 0 < 1 + κ * t ^ 2) (hu : 0 < 1 + κ * u ^ 2) (hv : 0 < 1 + κ * v ^ 2) : step κ (step κ t u) v = step κ t (step κ u v)

Steps can be taken in any grouping.

theorem ParallelPostulate.HyperbolicPlane.step_edge_self {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {κ e : K} (he : 1 + κ * e ^ 2 = 0) : step κ e e = e

A number on the edge is its own double.

theorem ParallelPostulate.HyperbolicPlane.apart_pos {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {κ : K} {P Q : K × K} (hP : P ∈ plane κ) (hQ : Q ∈ plane κ) (hPQ : P ≠ Q) : 0 < apart κ P Q

Two different points of the plane are apart.

theorem ParallelPostulate.HyperbolicPlane.shift_den_pos {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {κ a : K} (hκ : κ ≤ 0) (ha : 0 < 1 + κ * a ^ 2) {p : K × K} (hp : p ∈ plane κ) : 0 < 1 - κ * a * p.1

Under a bound that is not positive, the motion is defined at every point of the plane.

theorem ParallelPostulate.HyperbolicPlane.shift_mem_plane {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {κ a w : K} (hκ : κ ≤ 0) (hw : w ^ 2 = 1 + κ * a ^ 2) (hw0 : w ≠ 0) {p : K × K} (hp : p ∈ plane κ) : shift κ a w p ∈ plane κ

The motion takes points of the plane to points of the plane.

theorem ParallelPostulate.HyperbolicPlane.shift_neg_shift {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {κ a w : K} (hκ : κ ≤ 0) (hw : w ^ 2 = 1 + κ * a ^ 2) (hw0 : w ≠ 0) {p : K × K} (hp : p ∈ plane κ) : shift κ (-a) w (shift κ a w p) = p

The motion back, at a point of the plane.

theorem ParallelPostulate.HyperbolicPlane.shift_bijOn {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {κ a w : K} (hκ : κ ≤ 0) (hw : w ^ 2 = 1 + κ * a ^ 2) (hw0 : w ≠ 0) : Set.BijOn (shift κ a w) (plane κ) (plane κ)

The motion takes the plane onto itself, and different points to different points.

theorem ParallelPostulate.HyperbolicPlane.shift_keeps_left {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {κ a w : K} (hκ : κ ≤ 0) (hw : w ^ 2 = 1 + κ * a ^ 2) (hw0 : 0 < w) {A B C : K × K} (hA : A ∈ plane κ) (hB : B ∈ plane κ) (hC : C ∈ plane κ) : (0 < Pairs.cross ((shift κ a w B).1 - (shift κ a w A).1, (shift κ a w B).2 - (shift κ a w A).2) ((shift κ a w C).1 - (shift κ a w A).1, (shift κ a w C).2 - (shift κ a w A).2) ↔ 0 < Pairs.cross (B.1 - A.1, B.2 - A.2) (C.1 - A.1, C.2 - A.2)) ∧ (Pairs.cross ((shift κ a w B).1 - (shift κ a w A).1, (shift κ a w B).2 - (shift κ a w A).2) ((shift κ a w C).1 - (shift κ a w A).1, (shift κ a w C).2 - (shift κ a w A).2) < 0 ↔ Pairs.cross (B.1 - A.1, B.2 - A.2) (C.1 - A.1, C.2 - A.2) < 0) ∧ (Pairs.cross ((shift κ a w B).1 - (shift κ a w A).1, (shift κ a w B).2 - (shift κ a w A).2) ((shift κ a w C).1 - (shift κ a w A).1, (shift κ a w C).2 - (shift κ a w A).2) = 0 ↔ Pairs.cross (B.1 - A.1, B.2 - A.2) (C.1 - A.1, C.2 - A.2) = 0)

With w positive the motion keeps left and right. For three points of the plane, the cross product is positive, negative or zero after the motion as it was before.

theorem ParallelPostulate.HyperbolicPlane.shift_apart_plane {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {κ a w : K} (hκ : κ ≤ 0) (hw : w ^ 2 = 1 + κ * a ^ 2) (hw0 : w ≠ 0) {P Q : K × K} (hP : P ∈ plane κ) (hQ : Q ∈ plane κ) : apart κ (shift κ a w P) (shift κ a w Q) = apart κ P Q

The motion along the first axis keeps how far apart two points of the plane are.

theorem ParallelPostulate.HyperbolicPlane.shift_isLine {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {κ a w : K} (hκ : κ ≤ 0) (hw : w ^ 2 = 1 + κ * a ^ 2) (hw0 : w ≠ 0) {S : Set (K × K)} (hS : IsLine (plane κ) S) : IsLine (plane κ) (shift κ a w '' S)

The motion takes lines of the plane to lines of the plane.

theorem ParallelPostulate.HyperbolicPlane.rot_mem_plane {K : Type u_1} [Field K] [LinearOrder K] {c s : K} (h : c ^ 2 + s ^ 2 = 1) {κ : K} {p : K × K} : rot c s p ∈ plane κ ↔ p ∈ plane κ

Turning takes points of the plane to points of the plane, and no others.

theorem ParallelPostulate.HyperbolicPlane.rot_bijOn {K : Type u_1} [Field K] [LinearOrder K] {c s : K} (h : c ^ 2 + s ^ 2 = 1) (κ : K) : Set.BijOn (rot c s) (plane κ) (plane κ)

Turning takes the plane onto itself, and different points to different points.

theorem ParallelPostulate.HyperbolicPlane.rot_isLine {K : Type u_1} [Field K] [LinearOrder K] {c s : K} (h : c ^ 2 + s ^ 2 = 1) {κ : K} {S : Set (K × K)} (hS : IsLine (plane κ) S) : IsLine (plane κ) (rot c s '' S)

Turning takes lines of the plane to lines of the plane.

Angles in the plane of a bound

The inner product at a pair, kleinInner, and the angle it gives, kleinAngle. The motions keep it (Theorem H13). They take every point to (0, 0), where it is the angle of Euclid, so it is the only angle with these two properties (Theorem H15).

Contents

• Theorem H13, the motions keep angles: kleinInner, kleinInner_zero_bound, kleinInner_centre, kleinInner_self_pos, shift_kleinInner, rot_kleinInner, kleinAngle, kleinAngle_zero_bound, kleinAngle_centre, shift_kleinAngle, rot_kleinAngle
• Theorem H15, the motions take every point to (0, 0), and the angle they keep: exists_motion_to_centre, kleinAngle_unique
• steps of the proofs: kleinInner_aux, kleinAngle_aux

The inner product at a pair

def ParallelPostulate.HyperbolicPlane.kleinInner {K : Type u_1} [Field K] (κ : K) (P A B : K × K) : K

The inner product at a pair, under the bound κ: at the pair P, of the direction from P to A and the direction from P to B. It is the inner product of Euclid and one more term, κ times two cross products. With the bound 0, or at (0, 0), that term is zero. Divided by (1 + κ (P.1² + P.2²))² it is Klein's metric at P, on the directions A - P and B - P: kleinMetric_sub.

Equations

• ParallelPostulate.HyperbolicPlane.kleinInner κ P A B = (A.1 - P.1) * (B.1 - P.1) + (A.2 - P.2) * (B.2 - P.2) + κ * ParallelPostulate.Pairs.cross P A * ParallelPostulate.Pairs.cross P B

theorem ParallelPostulate.HyperbolicPlane.kleinInner_zero_bound {K : Type u_1} [Field K] (P A B : K × K) : kleinInner 0 P A B = (A.1 - P.1) * (B.1 - P.1) + (A.2 - P.2) * (B.2 - P.2)

With the bound 0 it is the inner product of Euclid.

theorem ParallelPostulate.HyperbolicPlane.kleinInner_centre {K : Type u_1} [Field K] (κ : K) (A B : K × K) : kleinInner κ (0, 0) A B = A.1 * B.1 + A.2 * B.2

At (0, 0) it is the inner product of Euclid, under any bound.

theorem ParallelPostulate.HyperbolicPlane.kleinInner_aux {K : Type u_1} [Field K] (κ a w xP yP xA yA xB yB XP YP XA YA XB YB : K) (hw : w ^ 2 = 1 + κ * a ^ 2) (hXP : XP * (1 - κ * a * xP) = xP + a) (hYP : YP * (1 - κ * a * xP) = w * yP) (hXA : XA * (1 - κ * a * xA) = xA + a) (hYA : YA * (1 - κ * a * xA) = w * yA) (hXB : XB * (1 - κ * a * xB) = xB + a) (hYB : YB * (1 - κ * a * xB) = w * yB) : ((XA - XP) * (XB - XP) + (YA - YP) * (YB - YP) + κ * (XP * YA - YP * XA) * (XP * YB - YP * XB)) * ((1 - κ * a * xP) ^ 2 * (1 - κ * a * xA) * (1 - κ * a * xB)) = w ^ 4 * ((xA - xP) * (xB - xP) + (yA - yP) * (yB - yP) + κ * (xP * yA - yP * xA) * (xP * yB - yP * xB))

The algebra of the next theorem, with the divisions taken out.

theorem ParallelPostulate.HyperbolicPlane.shift_kleinInner {K : Type u_1} [Field K] {κ a w : K} (hw : w ^ 2 = 1 + κ * a ^ 2) {P A B : K × K} (hP : 1 - κ * a * P.1 ≠ 0) (hA : 1 - κ * a * A.1 ≠ 0) (hB : 1 - κ * a * B.1 ≠ 0) : kleinInner κ (shift κ a w P) (shift κ a w A) (shift κ a w B) = w ^ 4 * kleinInner κ P A B / ((1 - κ * a * P.1) ^ 2 * (1 - κ * a * A.1) * (1 - κ * a * B.1))

The motion along the first axis keeps the inner product at a pair, up to a factor. The factor is the same for every direction from the pair once each direction is divided by its own denominator, and so the motion keeps angles: see shift_kleinAngle.

theorem ParallelPostulate.HyperbolicPlane.rot_kleinInner {K : Type u_1} [Field K] {c s : K} (h : c ^ 2 + s ^ 2 = 1) (κ : K) (P A B : K × K) : kleinInner κ (rot c s P) (rot c s A) (rot c s B) = kleinInner κ P A B

Turning keeps the inner product at a pair.

theorem ParallelPostulate.HyperbolicPlane.kleinInner_self_pos {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {κ : K} {P A : K × K} (hP : P ∈ plane κ) (hA : A ≠ P) : 0 < kleinInner κ P A A

At a point of the plane the inner product is positive on every direction that is not zero. So it is an inner product, under any bound.

Angles

With the real numbers for numbers, the inner product at a pair gives an angle, as the inner product of Euclid gives the angle of Mathlib.

noncomputable def ParallelPostulate.HyperbolicPlane.kleinAngle (κ : ℝ) (P A B : ℝ × ℝ) : ℝ

The angle at a pair, under the bound κ: the angle at P between the direction from P to A and the direction from P to B. It is made from kleinInner as Mathlib makes the angle of Euclid from the inner product.

Equations

• One or more equations did not get rendered due to their size.

theorem ParallelPostulate.HyperbolicPlane.kleinAngle_zero_bound (P A B : ℝ × ℝ) : kleinAngle 0 P A B = InnerProductGeometry.angle !₂[A.1 - P.1, A.2 - P.2] !₂[B.1 - P.1, B.2 - P.2]

With the bound 0 it is the angle of Euclid, in Mathlib's sense.

theorem ParallelPostulate.HyperbolicPlane.kleinAngle_centre (κ : ℝ) (A B : ℝ × ℝ) : kleinAngle κ (0, 0) A B = InnerProductGeometry.angle !₂[A.1, A.2] !₂[B.1, B.2]

At (0, 0) it is the angle of Euclid, under any bound.

theorem ParallelPostulate.HyperbolicPlane.kleinAngle_aux {g g₁ g₂ m u v : ℝ} (hm : 0 < m) (huv : 0 < u * v) : Real.arccos (m * u * v * g / (√(m * u ^ 2 * g₁) * √(m * v ^ 2 * g₂))) = Real.arccos (g / (√g₁ * √g₂))

The last step of the next theorem: an angle does not change when the inner products are multiplied as a motion multiplies them.

theorem ParallelPostulate.HyperbolicPlane.shift_kleinAngle {κ a w : ℝ} (hκ : κ ≤ 0) (hw : w ^ 2 = 1 + κ * a ^ 2) (hw0 : w ≠ 0) {P A B : ℝ × ℝ} (hP : P ∈ plane κ) (hA : A ∈ plane κ) (hB : B ∈ plane κ) : kleinAngle κ (shift κ a w P) (shift κ a w A) (shift κ a w B) = kleinAngle κ P A B

Theorem H13. The motion along the first axis keeps angles. For three points of the plane, the angle at the first between the two others is the same after the motion.

theorem ParallelPostulate.HyperbolicPlane.rot_kleinAngle {c s : ℝ} (h : c ^ 2 + s ^ 2 = 1) (κ : ℝ) (P A B : ℝ × ℝ) : kleinAngle κ (rot c s P) (rot c s A) (rot c s B) = kleinAngle κ P A B

Theorem H13. Turning keeps angles.

theorem ParallelPostulate.HyperbolicPlane.exists_motion_to_centre {κ : ℝ} {P : ℝ × ℝ} (hP : P ∈ plane κ) : ∃ (c : ℝ) (s : ℝ) (a : ℝ) (w : ℝ), c ^ 2 + s ^ 2 = 1 ∧ w ^ 2 = 1 + κ * a ^ 2 ∧ 0 < w ∧ shift κ a w (rot c s P) = (0, 0)

Theorem H15. The motions take every point of the plane to (0, 0). A turn takes the point to the number r of the first axis, where r is its distance from (0, 0) in Euclid's sense, and the motion along the first axis with a = -r takes it on to (0, 0).

theorem ParallelPostulate.HyperbolicPlane.kleinAngle_unique {κ : ℝ} (hκ : κ ≤ 0) (θ : ℝ × ℝ → ℝ × ℝ → ℝ × ℝ → ℝ) (hshift : ∀ (a w : ℝ), w ^ 2 = 1 + κ * a ^ 2 → 0 < w → ∀ (P A B : ℝ × ℝ), P ∈ plane κ → A ∈ plane κ → B ∈ plane κ → θ (shift κ a w P) (shift κ a w A) (shift κ a w B) = θ P A B) (hrot : ∀ (c s : ℝ), c ^ 2 + s ^ 2 = 1 → ∀ (P A B : ℝ × ℝ), P ∈ plane κ → A ∈ plane κ → B ∈ plane κ → θ (rot c s P) (rot c s A) (rot c s B) = θ P A B) (hcentre : ∀ (A B : ℝ × ℝ), A ∈ plane κ → B ∈ plane κ → θ (0, 0) A B = InnerProductGeometry.angle !₂[A.1, A.2] !₂[B.1, B.2]) {P A B : ℝ × ℝ} (hP : P ∈ plane κ) (hA : A ∈ plane κ) (hB : B ∈ plane κ) : θ P A B = kleinAngle κ P A B

kleinAngle is the only angle that the motions keep and that is the angle of Euclid at (0, 0). Let θ give a number to three points of the plane. If turning and the motion along the first axis keep θ, and at (0, 0) it is the angle of Euclid in Mathlib's sense, then it is kleinAngle. The proof moves the vertex to (0, 0) with Theorem H15.

Klein's metric

kleinMetric is the metric of Klein's model, as the books write it. The two motions keep it: moved by the derivative of a motion, in Mathlib's sense, two directions have the metric they had before (Theorem H16). kleinAngle is the angle of this metric.

Contents

• Theorem H16, Klein's metric, and the motions keep it: kleinMetric, kleinMetric_zero_bound, kleinMetric_sub, kleinMetric_pos, shiftDeriv, shift_kleinMetric, rot_kleinMetric, shift_differentiableAt, shift_hasLineDerivAt, fderiv_shift, fderiv_rot, shift_kleinMetric_fderiv, rot_kleinMetric_fderiv, kleinAngle_eq_metric
• a step of the proofs: kleinMetric_aux

The metric

def ParallelPostulate.HyperbolicPlane.kleinMetric {K : Type u_1} [Field K] (κ : K) (P u v : K × K) : K

Klein's metric, under the bound κ: at the pair P, of the directions u and v. It is the metric of Klein's model as the books write it: under the bound -1, ds² = (|dx|² (1 - |x|²) + (x · dx)²) / (1 - |x|²)². With the bound 0 it is the inner product of Euclid.

Equations

• ParallelPostulate.HyperbolicPlane.kleinMetric κ P u v = (u.1 * v.1 + u.2 * v.2 + κ * ParallelPostulate.Pairs.cross P u * ParallelPostulate.Pairs.cross P v) / (1 + κ * (P.1 ^ 2 + P.2 ^ 2)) ^ 2

theorem ParallelPostulate.HyperbolicPlane.kleinMetric_zero_bound {K : Type u_1} [Field K] (P u v : K × K) : kleinMetric 0 P u v = u.1 * v.1 + u.2 * v.2

With the bound 0 it is the inner product of Euclid, at every pair.

theorem ParallelPostulate.HyperbolicPlane.kleinMetric_sub {K : Type u_1} [Field K] (κ : K) (P A B : K × K) : kleinMetric κ P (A - P) (B - P) = kleinInner κ P A B / (1 + κ * (P.1 ^ 2 + P.2 ^ 2)) ^ 2

On the directions from P to A and from P to B, it is the inner product at P, divided by the square of the bound at P.

def ParallelPostulate.HyperbolicPlane.shiftDeriv {K : Type u_1} [Field K] (κ a w : K) (P u : K × K) : K × K

The derivative of the motion along the first axis at the pair P, on the direction u. That it is the derivative in Mathlib's sense is fderiv_shift.

Equations

• ParallelPostulate.HyperbolicPlane.shiftDeriv κ a w P u = ((1 + κ * a ^ 2) * u.1 / (1 - κ * a * P.1) ^ 2, w * (κ * a * P.2 * u.1 + (1 - κ * a * P.1) * u.2) / (1 - κ * a * P.1) ^ 2)

theorem ParallelPostulate.HyperbolicPlane.kleinMetric_aux {K : Type u_1} [Field K] (κ a w x y u1 u2 v1 v2 : K) (hw : w ^ 2 = 1 + κ * a ^ 2) : (1 + κ * a ^ 2) ^ 2 * (u1 * v1) + w ^ 2 * ((κ * a * y * u1 + (1 - κ * a * x) * u2) * (κ * a * y * v1 + (1 - κ * a * x) * v2)) + κ * w ^ 2 * (((x + a) * u2 - y * u1) * ((x + a) * v2 - y * v1)) = w ^ 4 * (u1 * v1 + u2 * v2 + κ * (x * u2 - y * u1) * (x * v2 - y * v1))

The algebra of the next theorem, with the divisions taken out.

theorem ParallelPostulate.HyperbolicPlane.shift_kleinMetric {K : Type u_1} [Field K] {κ a w : K} (hw : w ^ 2 = 1 + κ * a ^ 2) (hw0 : w ≠ 0) {P : K × K} (hD : 1 - κ * a * P.1 ≠ 0) (hP : 1 + κ * (P.1 ^ 2 + P.2 ^ 2) ≠ 0) (u v : K × K) : kleinMetric κ (shift κ a w P) (shiftDeriv κ a w P u) (shiftDeriv κ a w P v) = kleinMetric κ P u v

The motion along the first axis keeps Klein's metric. At the pair to which it moves P, the metric of the two directions to which its derivative moves u and v is the metric of u and v at P.

theorem ParallelPostulate.HyperbolicPlane.rot_kleinMetric {K : Type u_1} [Field K] {c s : K} (h : c ^ 2 + s ^ 2 = 1) (κ : K) (P u v : K × K) : kleinMetric κ (rot c s P) (rot c s u) (rot c s v) = kleinMetric κ P u v

Turning keeps Klein's metric. Turning is its own derivative.

theorem ParallelPostulate.HyperbolicPlane.kleinMetric_pos {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {κ : K} {P u : K × K} (hP : P ∈ plane κ) (hu : u ≠ 0) : 0 < kleinMetric κ P u u

At a point of the plane Klein's metric is positive on every direction that is not zero.

The motions keep Klein's metric

With the real numbers for numbers, the derivatives of the two motions are derivatives in Mathlib's sense, and the motions keep Klein's metric.

theorem ParallelPostulate.HyperbolicPlane.shift_differentiableAt {κ a w : ℝ} {P : ℝ × ℝ} (hD : 1 - κ * a * P.1 ≠ 0) : DifferentiableAt ℝ (shift κ a w) P

The motion along the first axis has a derivative wherever it is defined.

theorem ParallelPostulate.HyperbolicPlane.shift_hasLineDerivAt {κ a w : ℝ} {P : ℝ × ℝ} (hD : 1 - κ * a * P.1 ≠ 0) (u : ℝ × ℝ) : HasLineDerivAt ℝ (shift κ a w) (shiftDeriv κ a w P u) P u

Along the direction u from P, the motion along the first axis has the derivative shiftDeriv.

theorem ParallelPostulate.HyperbolicPlane.fderiv_shift {κ a w : ℝ} {P : ℝ × ℝ} (hD : 1 - κ * a * P.1 ≠ 0) (u : ℝ × ℝ) : (fderiv ℝ (shift κ a w) P) u = shiftDeriv κ a w P u

shiftDeriv is the derivative of the motion along the first axis, in Mathlib's sense.

theorem ParallelPostulate.HyperbolicPlane.fderiv_rot (c s : ℝ) (P u : ℝ × ℝ) : (fderiv ℝ (rot c s) P) u = rot c s u

Turning is its own derivative, in Mathlib's sense.

theorem ParallelPostulate.HyperbolicPlane.shift_kleinMetric_fderiv {κ a w : ℝ} (hκ : κ ≤ 0) (hw : w ^ 2 = 1 + κ * a ^ 2) (hw0 : w ≠ 0) {P : ℝ × ℝ} (hP : P ∈ plane κ) (u v : ℝ × ℝ) : kleinMetric κ (shift κ a w P) ((fderiv ℝ (shift κ a w) P) u) ((fderiv ℝ (shift κ a w) P) v) = kleinMetric κ P u v

Theorem H16. The motion along the first axis keeps Klein's metric. At every point of the plane, the metric of two directions after the motion, moved by the derivative of the motion in Mathlib's sense, is their metric before it.

theorem ParallelPostulate.HyperbolicPlane.rot_kleinMetric_fderiv {c s : ℝ} (h : c ^ 2 + s ^ 2 = 1) (κ : ℝ) (P u v : ℝ × ℝ) : kleinMetric κ (rot c s P) ((fderiv ℝ (rot c s) P) u) ((fderiv ℝ (rot c s) P) v) = kleinMetric κ P u v

Theorem H16. Turning keeps Klein's metric.

theorem ParallelPostulate.HyperbolicPlane.kleinAngle_eq_metric {κ : ℝ} {P : ℝ × ℝ} (hP : P ∈ plane κ) (A B : ℝ × ℝ) : kleinAngle κ P A B = Real.arccos (kleinMetric κ P (A - P) (B - P) / (√(kleinMetric κ P (A - P) (A - P)) * √(kleinMetric κ P (B - P) (B - P))))

kleinAngle is the angle of Klein's metric. At a point of the plane, the angle between the directions to A and to B is made from kleinMetric as Mathlib makes the angle of Euclid from the inner product.

The curvature of Klein's metric

Mathlib has no curvature for a metric given by its coefficients, so gaussCurvature is Brioschi's formula, with Mathlib's derivatives along the two axes. For Klein's metric it is κ at every point of the plane, under every bound (Theorem H17); for the upper half plane of Poincaré it is -1, a check of the formula.

Contents

• Theorem H17, the curvature of Klein's metric is κ: partialX, partialY, gaussCurvature, kleinE, kleinF, kleinG, kleinMetric_coords, kleinMetric_curvature, halfPlane_curvature
• derivatives and determinants: hasDerivAt_cubic, hasDerivAt_div_sq, hasDerivAt_div_cube, det_three

The curvature of Klein's metric

Mathlib has no curvature for a metric given by its coefficients, so the curvature here is Brioschi's formula, with Mathlib's derivatives along the two axes.

noncomputable def ParallelPostulate.HyperbolicPlane.partialX (f : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : ℝ

The derivative of f along the first axis at p.

Equations

• ParallelPostulate.HyperbolicPlane.partialX f p = deriv (fun (t : ℝ) => f (t, p.2)) p.1

noncomputable def ParallelPostulate.HyperbolicPlane.partialY (f : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : ℝ

The derivative of f along the second axis at p.

Equations

• ParallelPostulate.HyperbolicPlane.partialY f p = deriv (fun (t : ℝ) => f (p.1, t)) p.2

noncomputable def ParallelPostulate.HyperbolicPlane.gaussCurvature (E F G : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : ℝ

The curvature of a metric, E dx² + 2 F dx dy + G dy², at p, by Brioschi's formula, with the derivatives of Mathlib.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ParallelPostulate.HyperbolicPlane.kleinE (κ : ℝ) (p : ℝ × ℝ) : ℝ

The coefficient of dx² in Klein's metric.

Equations

• ParallelPostulate.HyperbolicPlane.kleinE κ p = (1 + κ * p.2 ^ 2) / (1 + κ * (p.1 ^ 2 + p.2 ^ 2)) ^ 2

noncomputable def ParallelPostulate.HyperbolicPlane.kleinF (κ : ℝ) (p : ℝ × ℝ) : ℝ

The coefficient of dx dy in Klein's metric, taken twice.

Equations

• ParallelPostulate.HyperbolicPlane.kleinF κ p = -κ * p.1 * p.2 / (1 + κ * (p.1 ^ 2 + p.2 ^ 2)) ^ 2

noncomputable def ParallelPostulate.HyperbolicPlane.kleinG (κ : ℝ) (p : ℝ × ℝ) : ℝ

The coefficient of dy² in Klein's metric.

Equations

• ParallelPostulate.HyperbolicPlane.kleinG κ p = (1 + κ * p.1 ^ 2) / (1 + κ * (p.1 ^ 2 + p.2 ^ 2)) ^ 2

theorem ParallelPostulate.HyperbolicPlane.kleinMetric_coords (κ : ℝ) (p u v : ℝ × ℝ) : kleinMetric κ p u v = kleinE κ p * u.1 * v.1 + kleinF κ p * (u.1 * v.2 + u.2 * v.1) + kleinG κ p * u.2 * v.2

Klein's metric is E dx² + 2 F dx dy + G dy², with kleinE, kleinF and kleinG.

theorem ParallelPostulate.HyperbolicPlane.hasDerivAt_cubic (c0 c1 c2 c3 : ℝ) {f : ℝ → ℝ} (hf : ∀ (s : ℝ), f s = c0 + c1 * s + c2 * s ^ 2 + c3 * s ^ 3) (t : ℝ) : HasDerivAt f (c1 + 2 * c2 * t + 3 * c3 * t ^ 2) t

The derivative of a polynomial of degree at most 3.

theorem ParallelPostulate.HyperbolicPlane.hasDerivAt_div_sq {f b : ℝ → ℝ} {f' b' t : ℝ} (hf : HasDerivAt f f' t) (hb : HasDerivAt b b' t) (h : b t ≠ 0) : HasDerivAt (fun (s : ℝ) => f s / b s ^ 2) ((f' * b t - 2 * f t * b') / b t ^ 3) t

The derivative of a quotient by a square.

theorem ParallelPostulate.HyperbolicPlane.hasDerivAt_div_cube {f b : ℝ → ℝ} {f' b' t : ℝ} (hf : HasDerivAt f f' t) (hb : HasDerivAt b b' t) (h : b t ≠ 0) : HasDerivAt (fun (s : ℝ) => f s / b s ^ 3) ((f' * b t - 3 * f t * b') / b t ^ 4) t

The derivative of a quotient by a cube.

theorem ParallelPostulate.HyperbolicPlane.det_three (a b c d e f g h i : ℝ) : !![a, b, c; d, e, f; g, h, i].det = a * e * i - a * f * h - b * d * i + b * f * g + c * d * h - c * e * g

The determinant of a 3 × 3 matrix.

theorem ParallelPostulate.HyperbolicPlane.kleinMetric_curvature {κ : ℝ} {P : ℝ × ℝ} (hP : P ∈ plane κ) : gaussCurvature (kleinE κ) (kleinF κ) (kleinG κ) P = κ

Theorem H17. The curvature of Klein's metric is κ, at every point of the plane, and under every bound: negative, 0 or positive.

theorem ParallelPostulate.HyperbolicPlane.halfPlane_curvature {p : ℝ × ℝ} (hp : 0 < p.2) : gaussCurvature (fun (q : ℝ × ℝ) => 1 / q.2 ^ 2) (fun (x : ℝ × ℝ) => 0) (fun (q : ℝ × ℝ) => 1 / q.2 ^ 2) p = -1

A check of gaussCurvature: the upper half plane of Poincaré has the curvature -1. Its metric is (dx² + dy²) / y², and its curvature is known to be -1.

Klein's distance

kleinDist is the least length of a path between two points, the length measured with Klein's metric: the infimum of the lengths of the maps of [0, 1] into the plane with a continuous derivative. The two motions keep it, and under a negative bound apart is sinh² (√(-κ) d) / (-κ), where d is the distance (Theorem H18).

Contents

• Theorem H18, Klein's distance, and apart as a function of it: IsKleinPath, kleinLength, kleinDist, kleinLength_nonneg, segment_isKleinPath, kleinDist_nonempty, kleinDist_bddBelow, kleinLength_integrand_continuousOn, isKleinPath_map, kleinDist_map_le, shift_contDiffOn, shift_kleinDist, rot_kleinDist, axisDist, axisDist_zero, hasDerivAt_axisDist, axis_le_metric, axisDist_sub_le_kleinLength, axis_isKleinPath, axis_kleinLength, kleinDist_axis, exists_rot_to_axis, kleinDist_eq_arsinh, apart_eq_sinh_kleinDist

Klein's distance

Klein's distance is the least length of a path, the length measured with Klein's metric. Under a negative bound, apart is a function of it.

def ParallelPostulate.HyperbolicPlane.IsKleinPath (κ : ℝ) (γ : ℝ → ℝ × ℝ) (P Q : ℝ × ℝ) : Prop

A path of the plane from P to Q: a map of [0, 1] into the plane, with a continuous derivative, from P to Q.

Equations

• ParallelPostulate.HyperbolicPlane.IsKleinPath κ γ P Q = (ContDiffOn ℝ 1 γ (Set.Icc 0 1) ∧ Set.MapsTo γ (Set.Icc 0 1) (ParallelPostulate.HyperbolicPlane.plane κ) ∧ γ 0 = P ∧ γ 1 = Q)

noncomputable def ParallelPostulate.HyperbolicPlane.kleinLength (κ : ℝ) (γ : ℝ → ℝ × ℝ) : ℝ

The length of a path in Klein's metric: the integral, over [0, 1], of the square root of the metric of its derivative.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ParallelPostulate.HyperbolicPlane.kleinDist (κ : ℝ) (P Q : ℝ × ℝ) : ℝ

Klein's distance between two points: the least length of a path from the one to the other, as an infimum.

Equations

• ParallelPostulate.HyperbolicPlane.kleinDist κ P Q = sInf (ParallelPostulate.HyperbolicPlane.kleinLength κ '' {γ : ℝ → ℝ × ℝ | ParallelPostulate.HyperbolicPlane.IsKleinPath κ γ P Q})

theorem ParallelPostulate.HyperbolicPlane.kleinLength_nonneg (κ : ℝ) (γ : ℝ → ℝ × ℝ) : 0 ≤ kleinLength κ γ

A length is not negative.

theorem ParallelPostulate.HyperbolicPlane.segment_isKleinPath {κ : ℝ} {P Q : ℝ × ℝ} (hP : P ∈ plane κ) (hQ : Q ∈ plane κ) : IsKleinPath κ { zero := P, one := Q }.pt P Q

The segment from P to Q is a path of the plane.

theorem ParallelPostulate.HyperbolicPlane.kleinDist_nonempty {κ : ℝ} {P Q : ℝ × ℝ} (hP : P ∈ plane κ) (hQ : Q ∈ plane κ) : (kleinLength κ '' {γ : ℝ → ℝ × ℝ | IsKleinPath κ γ P Q}).Nonempty

Two points of the plane have a path between them.

theorem ParallelPostulate.HyperbolicPlane.kleinDist_bddBelow (κ : ℝ) (P Q : ℝ × ℝ) : BddBelow (kleinLength κ '' {γ : ℝ → ℝ × ℝ | IsKleinPath κ γ P Q})

The lengths are bounded below, by 0.

theorem ParallelPostulate.HyperbolicPlane.kleinLength_integrand_continuousOn {κ : ℝ} {γ : ℝ → ℝ × ℝ} {P Q : ℝ × ℝ} (h : IsKleinPath κ γ P Q) : ContinuousOn (fun (t : ℝ) => √(kleinMetric κ (γ t) (derivWithin γ (Set.Icc 0 1) t) (derivWithin γ (Set.Icc 0 1) t))) (Set.Icc 0 1)

The integrand of the length is continuous.

theorem ParallelPostulate.HyperbolicPlane.isKleinPath_map {κ : ℝ} {M : ℝ × ℝ → ℝ × ℝ} (hM : ContDiffOn ℝ 1 M (plane κ)) (hMp : Set.MapsTo M (plane κ) (plane κ)) (hMd : ∀ p ∈ plane κ, DifferentiableAt ℝ M p) (hMg : ∀ p ∈ plane κ, ∀ (v : ℝ × ℝ), kleinMetric κ (M p) ((fderiv ℝ M p) v) ((fderiv ℝ M p) v) = kleinMetric κ p v v) {γ : ℝ → ℝ × ℝ} {P Q : ℝ × ℝ} (h : IsKleinPath κ γ P Q) : IsKleinPath κ (M ∘ γ) (M P) (M Q) ∧ kleinLength κ (M ∘ γ) = kleinLength κ γ

A motion that keeps the plane and Klein's metric keeps paths and their lengths.

theorem ParallelPostulate.HyperbolicPlane.kleinDist_map_le {κ : ℝ} {M : ℝ × ℝ → ℝ × ℝ} (hM : ContDiffOn ℝ 1 M (plane κ)) (hMp : Set.MapsTo M (plane κ) (plane κ)) (hMd : ∀ p ∈ plane κ, DifferentiableAt ℝ M p) (hMg : ∀ p ∈ plane κ, ∀ (v : ℝ × ℝ), kleinMetric κ (M p) ((fderiv ℝ M p) v) ((fderiv ℝ M p) v) = kleinMetric κ p v v) {P Q : ℝ × ℝ} (hP : P ∈ plane κ) (hQ : Q ∈ plane κ) : kleinDist κ (M P) (M Q) ≤ kleinDist κ P Q

A motion that keeps the plane and Klein's metric does not make distances longer.

theorem ParallelPostulate.HyperbolicPlane.shift_contDiffOn {κ a w : ℝ} (hκ : κ ≤ 0) (ha : 0 < 1 + κ * a ^ 2) : ContDiffOn ℝ 1 (shift κ a w) (plane κ)

The motion along the first axis has a continuous derivative on the plane.

theorem ParallelPostulate.HyperbolicPlane.shift_kleinDist {κ a w : ℝ} (hκ : κ ≤ 0) (hw : w ^ 2 = 1 + κ * a ^ 2) (hw0 : w ≠ 0) {P Q : ℝ × ℝ} (hP : P ∈ plane κ) (hQ : Q ∈ plane κ) : kleinDist κ (shift κ a w P) (shift κ a w Q) = kleinDist κ P Q

The motion along the first axis keeps Klein's distance.

theorem ParallelPostulate.HyperbolicPlane.rot_kleinDist {κ c s : ℝ} (h : c ^ 2 + s ^ 2 = 1) {P Q : ℝ × ℝ} (hP : P ∈ plane κ) (hQ : Q ∈ plane κ) : kleinDist κ (rot c s P) (rot c s Q) = kleinDist κ P Q

Turning keeps Klein's distance.

noncomputable def ParallelPostulate.HyperbolicPlane.axisDist (κ x : ℝ) : ℝ

Klein's distance from (0, 0) to the number x of the first axis, under a negative bound.

Equations

• ParallelPostulate.HyperbolicPlane.axisDist κ x = Real.arsinh (√(-κ) * x / √(1 + κ * x ^ 2)) / √(-κ)

theorem ParallelPostulate.HyperbolicPlane.axisDist_zero (κ : ℝ) : axisDist κ 0 = 0

The distance from (0, 0) to itself is 0.

theorem ParallelPostulate.HyperbolicPlane.hasDerivAt_axisDist {κ x : ℝ} (hκ : κ < 0) (hx : 0 < 1 + κ * x ^ 2) : HasDerivAt (axisDist κ) (1 / (1 + κ * x ^ 2)) x

The derivative of axisDist is 1 / (1 + κ x²).

theorem ParallelPostulate.HyperbolicPlane.axis_le_metric {κ : ℝ} (hκ : κ ≤ 0) {p : ℝ × ℝ} (hp : p ∈ plane κ) (v : ℝ × ℝ) : 1 / (1 + κ * p.1 ^ 2) * v.1 ≤ √(kleinMetric κ p v v)

Along the first axis, a direction is no longer in Klein's metric than its first entry, divided by 1 + κ x². The proof is the identity c N - B v₁² = (κ x y v₁ - c v₂)², where c = 1 + κ x², B is the bound at the point and N is the numerator of the metric.

theorem ParallelPostulate.HyperbolicPlane.axisDist_sub_le_kleinLength {κ : ℝ} (hκ : κ < 0) {γ : ℝ → ℝ × ℝ} {P Q : ℝ × ℝ} (h : IsKleinPath κ γ P Q) : axisDist κ Q.1 - axisDist κ P.1 ≤ kleinLength κ γ

Every path is at least as long as the distance along the first axis between the first entries of its ends.

theorem ParallelPostulate.HyperbolicPlane.axis_isKleinPath {κ r : ℝ} (hκ : κ ≤ 0) (hr : (r, 0) ∈ plane κ) : IsKleinPath κ (fun (t : ℝ) => (t * r, 0)) (0, 0) (r, 0)

The path along the first axis from (0, 0) to (r, 0).

theorem ParallelPostulate.HyperbolicPlane.axis_kleinLength {κ r : ℝ} (hκ : κ < 0) (hr0 : 0 ≤ r) (hr : (r, 0) ∈ plane κ) : (kleinLength κ fun (t : ℝ) => (t * r, 0)) = axisDist κ r

The path along the first axis has the length axisDist.

theorem ParallelPostulate.HyperbolicPlane.kleinDist_axis {κ r : ℝ} (hκ : κ < 0) (hr0 : 0 ≤ r) (hr : (r, 0) ∈ plane κ) : kleinDist κ (0, 0) (r, 0) = axisDist κ r

Klein's distance from (0, 0) to (r, 0) is axisDist.

theorem ParallelPostulate.HyperbolicPlane.exists_rot_to_axis (Q : ℝ × ℝ) : ∃ (c : ℝ) (s : ℝ) (r : ℝ), c ^ 2 + s ^ 2 = 1 ∧ 0 ≤ r ∧ rot c s Q = (r, 0)

A turn takes every pair to the first axis, on the side of the positive numbers.

theorem ParallelPostulate.HyperbolicPlane.kleinDist_eq_arsinh {κ : ℝ} (hκ : κ < 0) {P Q : ℝ × ℝ} (hP : P ∈ plane κ) (hQ : Q ∈ plane κ) : kleinDist κ P Q = Real.arsinh √(-κ * apart κ P Q) / √(-κ)

Theorem H18. Klein's distance, under a negative bound, between two points of the plane: arsinh √(-κ apart) / √(-κ).

theorem ParallelPostulate.HyperbolicPlane.apart_eq_sinh_kleinDist {κ : ℝ} (hκ : κ < 0) {P Q : ℝ × ℝ} (hP : P ∈ plane κ) (hQ : Q ∈ plane κ) : apart κ P Q = Real.sinh (√(-κ) * kleinDist κ P Q) ^ 2 / -κ

Theorem H18. apart is a function of Klein's distance: apart = sinh² (√(-κ) d) / (-κ), under a negative bound.

Hilbert's axioms of congruence in the plane of a bound

With the real numbers and a negative bound, a segment is measured by Klein's distance and an angle by kleinAngle, and two segments, or two angles, are congruent when their measures are equal. This file proves Hilbert's six axioms of congruence, C1 to C6 (Theorem H19). It also proves C1, C3 and C6 with apart for the bound 0, and so for every bound that is not positive, for the Hilbert planes of the Hilbert model section.

Contents

• Theorem H19, Hilbert's axioms of congruence: OnRay, SameSide, segment_construction (C1), segment_congruence_trans (C2), segment_addition (C3), angle_construction (C4), angle_congruence_trans (C5), side_angle_side (C6), kleinDist_comm, kleinAngle_comm, kleinAngle_onRay, kleinDist_nonneg, kleinDist_pos, sinh_kleinDist, cosh_kleinDist, cos_kleinAngle, law_of_cosines, kleinDist_add_of_between
• steps of the proofs of congruence: apart_eq_kleinInner, one_add_dot_pos, kleinInner_gram, kleinAngle_eq_arccos_cos, apart_ray, apart_ray_lt, exists_onRay_apart, sin_kleinAngle_pos
• a ray, as Hilbert has it: onRay_of_between, between_of_onRay
• Euclid's plane, with apart: mem_plane_zero, apart_zero_nonneg, apart_zero_eq_kleinInner, euclid_segment_construction, euclid_sqrt_apart_add, euclid_segment_addition, euclid_law_of_cosines, euclid_sas
• C1, C3 and C6 with apart, under a bound that is not positive: apart_eq_iff_kleinDist_eq, segment_construction_apart, segment_addition_apart, sas_apart

Hilbert's axioms of congruence

With the real numbers and a negative bound, a segment is measured by Klein's distance and an angle by kleinAngle, and two segments, or two angles, are congruent when their measures are equal. This section proves Hilbert's six axioms of congruence, C1 to C6, for the plane.

theorem ParallelPostulate.HyperbolicPlane.apart_eq_kleinInner (κ : ℝ) (P Q : ℝ × ℝ) : apart κ P Q = kleinInner κ P Q Q / ((1 + κ * (P.1 ^ 2 + P.2 ^ 2)) * (1 + κ * (Q.1 ^ 2 + Q.2 ^ 2)))

apart is the inner product at P of the direction to Q with itself, divided by the bounds at the two pairs.

theorem ParallelPostulate.HyperbolicPlane.one_add_dot_pos {κ : ℝ} (hκ : κ ≤ 0) {P Q : ℝ × ℝ} (hP : P ∈ plane κ) (hQ : Q ∈ plane κ) : 0 < 1 + κ * (P.1 * Q.1 + P.2 * Q.2)

Under a bound that is not positive, two points of the plane have 1 + κ (P · Q) positive.

theorem ParallelPostulate.HyperbolicPlane.kleinDist_nonneg {κ : ℝ} {P Q : ℝ × ℝ} (hP : P ∈ plane κ) (hQ : Q ∈ plane κ) : 0 ≤ kleinDist κ P Q

Klein's distance is not negative.

theorem ParallelPostulate.HyperbolicPlane.kleinDist_comm {κ : ℝ} (hκ : κ < 0) {P Q : ℝ × ℝ} (hP : P ∈ plane κ) (hQ : Q ∈ plane κ) : kleinDist κ P Q = kleinDist κ Q P

Klein's distance does not depend on the order of the two points.

theorem ParallelPostulate.HyperbolicPlane.kleinDist_pos {κ : ℝ} (hκ : κ < 0) {P Q : ℝ × ℝ} (hP : P ∈ plane κ) (hQ : Q ∈ plane κ) (hPQ : P ≠ Q) : 0 < kleinDist κ P Q

Two different points of the plane are a positive distance apart.

theorem ParallelPostulate.HyperbolicPlane.sinh_kleinDist {κ : ℝ} (hκ : κ < 0) {P Q : ℝ × ℝ} (hP : P ∈ plane κ) (hQ : Q ∈ plane κ) : Real.sinh (√(-κ) * kleinDist κ P Q) = √(-κ) * √(kleinInner κ P Q Q) / (√(1 + κ * (P.1 ^ 2 + P.2 ^ 2)) * √(1 + κ * (Q.1 ^ 2 + Q.2 ^ 2)))

The hyperbolic sine of Klein's distance.

theorem ParallelPostulate.HyperbolicPlane.cosh_kleinDist {κ : ℝ} (hκ : κ < 0) {P Q : ℝ × ℝ} (hP : P ∈ plane κ) (hQ : Q ∈ plane κ) : Real.cosh (√(-κ) * kleinDist κ P Q) = (1 + κ * (P.1 * Q.1 + P.2 * Q.2)) / (√(1 + κ * (P.1 ^ 2 + P.2 ^ 2)) * √(1 + κ * (Q.1 ^ 2 + Q.2 ^ 2)))

The hyperbolic cosine of Klein's distance.

theorem ParallelPostulate.HyperbolicPlane.kleinInner_gram (κ : ℝ) (P A B : ℝ × ℝ) : kleinInner κ P A A * kleinInner κ P B B - kleinInner κ P A B ^ 2 = (1 + κ * (P.1 ^ 2 + P.2 ^ 2)) * { zero := P, one := A }.side B ^ 2

The Gram identity for the inner product at a pair.

theorem ParallelPostulate.HyperbolicPlane.cos_kleinAngle {κ : ℝ} {P A B : ℝ × ℝ} (hP : P ∈ plane κ) (hA : A ≠ P) (hB : B ≠ P) : Real.cos (kleinAngle κ P A B) = kleinInner κ P A B / (√(kleinInner κ P A A) * √(kleinInner κ P B B))

The cosine of kleinAngle. At a point of the plane the quotient is between -1 and 1, and kleinAngle is its arccosine.

theorem ParallelPostulate.HyperbolicPlane.kleinAngle_eq_arccos_cos (κ : ℝ) (P A B : ℝ × ℝ) : kleinAngle κ P A B = Real.arccos (Real.cos (kleinAngle κ P A B))

kleinAngle is between 0 and π, so it is the arccosine of its cosine.

theorem ParallelPostulate.HyperbolicPlane.law_of_cosines {κ : ℝ} (hκ : κ < 0) {P A B : ℝ × ℝ} (hP : P ∈ plane κ) (hA : A ∈ plane κ) (hB : B ∈ plane κ) (hAP : A ≠ P) (hBP : B ≠ P) : Real.cosh (√(-κ) * kleinDist κ P A) * Real.cosh (√(-κ) * kleinDist κ P B) - Real.cosh (√(-κ) * kleinDist κ A B) = Real.sinh (√(-κ) * kleinDist κ P A) * Real.sinh (√(-κ) * kleinDist κ P B) * Real.cos (kleinAngle κ P A B)

The law of cosines in the plane of a negative bound, with Klein's distance and kleinAngle, at the vertex P.

def ParallelPostulate.HyperbolicPlane.OnRay (O A X : ℝ × ℝ) : Prop

X is on the ray from O through A: X = O + t (A - O) with t positive.

Equations

• ParallelPostulate.HyperbolicPlane.OnRay O A X = ∃ (t : ℝ), 0 < t ∧ X = { zero := O, one := A }.pt t

def ParallelPostulate.HyperbolicPlane.SameSide (O A X Y : ℝ × ℝ) : Prop

X and Y are on the same side of the line through O and A.

Equations

• ParallelPostulate.HyperbolicPlane.SameSide O A X Y = (0 < { zero := O, one := A }.side X * { zero := O, one := A }.side Y)

theorem ParallelPostulate.HyperbolicPlane.kleinAngle_comm (κ : ℝ) (P A B : ℝ × ℝ) : kleinAngle κ P A B = kleinAngle κ P B A

An angle does not depend on the order of its two rays.

theorem ParallelPostulate.HyperbolicPlane.kleinAngle_onRay {κ : ℝ} {P A B A' B' : ℝ × ℝ} (hA : OnRay P A A') (hB : OnRay P B B') : kleinAngle κ P A' B' = kleinAngle κ P A B

An angle depends only on its two rays.

theorem ParallelPostulate.HyperbolicPlane.side_angle_side {κ : ℝ} (hκ : κ < 0) {A B C D E F : ℝ × ℝ} (hA : A ∈ plane κ) (hB : B ∈ plane κ) (hC : C ∈ plane κ) (hD : D ∈ plane κ) (hE : E ∈ plane κ) (hF : F ∈ plane κ) (hAB : A ≠ B) (hAC : A ≠ C) (hBC : B ≠ C) (hDE : D ≠ E) (hDF : D ≠ F) (hEF : E ≠ F) (h1 : kleinDist κ A B = kleinDist κ D E) (h2 : kleinDist κ A C = kleinDist κ D F) (h3 : kleinAngle κ A B C = kleinAngle κ D E F) : kleinDist κ B C = kleinDist κ E F ∧ kleinAngle κ B A C = kleinAngle κ E D F ∧ kleinAngle κ C A B = kleinAngle κ F D E

Theorem H19, C6: side, angle, side. Let two triangles have two sides and the angle between them congruent. Then the third sides are congruent, and so are the two other pairs of angles.

theorem ParallelPostulate.HyperbolicPlane.kleinDist_add_of_between {κ : ℝ} (hκ : κ < 0) {A B C : ℝ × ℝ} (hA : A ∈ plane κ) (hC : C ∈ plane κ) (h : Between A B C) : B ∈ plane κ ∧ kleinDist κ A C = kleinDist κ A B + kleinDist κ B C

Klein's distance adds along a segment. If B is between A and C, it is a point of the plane, and the distance from A to C is the sum of the distances from A to B and from B to C.

theorem ParallelPostulate.HyperbolicPlane.segment_addition {κ : ℝ} (hκ : κ < 0) {A B C D E F : ℝ × ℝ} (hA : A ∈ plane κ) (hC : C ∈ plane κ) (hD : D ∈ plane κ) (hF : F ∈ plane κ) (hABC : Between A B C) (hDEF : Between D E F) (h1 : kleinDist κ A B = kleinDist κ D E) (h2 : kleinDist κ B C = kleinDist κ E F) : kleinDist κ A C = kleinDist κ D F

Theorem H19, C3: addition of segments.

theorem ParallelPostulate.HyperbolicPlane.segment_congruence_trans {κ : ℝ} {A B C D E F : ℝ × ℝ} (h1 : kleinDist κ A B = kleinDist κ C D) (h2 : kleinDist κ A B = kleinDist κ E F) : kleinDist κ C D = kleinDist κ E F

Theorem H19, C2. Two segments congruent to a third are congruent to each other.

theorem ParallelPostulate.HyperbolicPlane.angle_congruence_trans {κ : ℝ} {A B C D E F P Q R : ℝ × ℝ} (h1 : kleinAngle κ A B C = kleinAngle κ D E F) (h2 : kleinAngle κ A B C = kleinAngle κ P Q R) : kleinAngle κ D E F = kleinAngle κ P Q R

Theorem H19, C5. Two angles congruent to a third are congruent to each other.

theorem ParallelPostulate.HyperbolicPlane.apart_ray (κ : ℝ) (O D : ℝ × ℝ) (t : ℝ) : apart κ O ({ zero := O, one := D }.pt t) = t ^ 2 * kleinInner κ O D D / ((1 + κ * (O.1 ^ 2 + O.2 ^ 2)) * (1 + κ * (({ zero := O, one := D }.pt t).1 ^ 2 + ({ zero := O, one := D }.pt t).2 ^ 2)))

Along the ray from O through D, apart from O.

theorem ParallelPostulate.HyperbolicPlane.apart_ray_lt {κ : ℝ} (hκ : κ < 0) {O D : ℝ × ℝ} (hO : O ∈ plane κ) (hOD : O ≠ D) {s t : ℝ} (hs : 0 < s) (hst : s < t) (hXs : { zero := O, one := D }.pt s ∈ plane κ) (hXt : { zero := O, one := D }.pt t ∈ plane κ) : apart κ O ({ zero := O, one := D }.pt s) < apart κ O ({ zero := O, one := D }.pt t)

Along a ray, apart from its origin grows.

theorem ParallelPostulate.HyperbolicPlane.exists_onRay_apart {κ : ℝ} (hκ : κ < 0) {O D : ℝ × ℝ} (hO : O ∈ plane κ) (hOD : O ≠ D) {α : ℝ} (hα : 0 < α) : ∃ (t : ℝ), 0 < t ∧ { zero := O, one := D }.pt t ∈ plane κ ∧ apart κ O ({ zero := O, one := D }.pt t) = α

On a ray from a point of the plane, apart from the origin takes every positive value. Under a negative bound.

theorem ParallelPostulate.HyperbolicPlane.segment_construction {κ : ℝ} (hκ : κ < 0) {A B O D : ℝ × ℝ} (hA : A ∈ plane κ) (hB : B ∈ plane κ) (hO : O ∈ plane κ) (hAB : A ≠ B) (hOD : O ≠ D) : ∃! X : ℝ × ℝ, X ∈ plane κ ∧ OnRay O D X ∧ kleinDist κ A B = kleinDist κ O X

Theorem H19, C1: construction of segments. On a ray from O there is one point, and only one, whose distance from O is the length of a given segment.

theorem ParallelPostulate.HyperbolicPlane.sin_kleinAngle_pos {κ : ℝ} {A B C : ℝ × ℝ} (hA : A ∈ plane κ) (hABC : { zero := A, one := B }.side C ≠ 0) : 0 < Real.sin (kleinAngle κ A B C)

An angle with two rays that are not on one line is strictly between 0 and π, so its sine is positive.

theorem ParallelPostulate.HyperbolicPlane.angle_construction {κ : ℝ} {A B C D F G : ℝ × ℝ} (hA : A ∈ plane κ) (hD : D ∈ plane κ) (hABC : { zero := A, one := B }.side C ≠ 0) (hDF : D ≠ F) (hG : { zero := D, one := F }.side G ≠ 0) : (∃ E ∈ plane κ, SameSide D F E G ∧ kleinAngle κ D F E = kleinAngle κ A B C) ∧ ∀ (E E' : ℝ × ℝ), E ∈ plane κ → SameSide D F E G → kleinAngle κ D F E = kleinAngle κ A B C → E' ∈ plane κ → SameSide D F E' G → kleinAngle κ D F E' = kleinAngle κ A B C → OnRay D E E'

Theorem H19, C4: construction of angles. Given an angle, a ray from D through F, and a side of the line DF, there is a ray from D on that side that makes the given angle with the ray DF, and only one. This holds under any bound.

A ray, as Hilbert has it

theorem ParallelPostulate.HyperbolicPlane.onRay_of_between {O A X : ℝ × ℝ} (h : X = A ∨ Between O X A ∨ Between O A X) : OnRay O A X

A point on the ray, as Hilbert has it, is on the ray as OnRay has it.

theorem ParallelPostulate.HyperbolicPlane.between_of_onRay {O A X : ℝ × ℝ} (hOA : O ≠ A) (h : OnRay O A X) : X = A ∨ Between O X A ∨ Between O A X

A point on the ray as OnRay has it is on the ray, as Hilbert has it.

Euclid's plane: congruence with apart under the bound 0

theorem ParallelPostulate.HyperbolicPlane.mem_plane_zero (p : ℝ × ℝ) : p ∈ plane 0

theorem ParallelPostulate.HyperbolicPlane.apart_zero_nonneg (P Q : ℝ × ℝ) : 0 ≤ apart 0 P Q

theorem ParallelPostulate.HyperbolicPlane.apart_zero_eq_kleinInner (P Q : ℝ × ℝ) : apart 0 P Q = kleinInner 0 P Q Q

theorem ParallelPostulate.HyperbolicPlane.euclid_segment_construction {A B O D : ℝ × ℝ} (hAB : A ≠ B) (hOD : O ≠ D) : ∃! X : ℝ × ℝ, X ∈ plane 0 ∧ OnRay O D X ∧ apart 0 A B = apart 0 O X

Under the bound 0, on a ray there is one point at a given apart from its origin.

theorem ParallelPostulate.HyperbolicPlane.euclid_sqrt_apart_add {A B C : ℝ × ℝ} (h : Between A B C) : √(apart 0 A C) = √(apart 0 A B) + √(apart 0 B C)

Under the bound 0, the square roots of apart add along a segment.

theorem ParallelPostulate.HyperbolicPlane.euclid_segment_addition {A B C D E F : ℝ × ℝ} (hABC : Between A B C) (hDEF : Between D E F) (h1 : apart 0 A B = apart 0 D E) (h2 : apart 0 B C = apart 0 E F) : apart 0 A C = apart 0 D F

Addition of segments under the bound 0.

theorem ParallelPostulate.HyperbolicPlane.euclid_law_of_cosines {A B C : ℝ × ℝ} (hB : B ≠ A) (hC : C ≠ A) : apart 0 B C = apart 0 A B + apart 0 A C - 2 * (√(apart 0 A B) * √(apart 0 A C)) * Real.cos (kleinAngle 0 A B C)

The law of cosines under the bound 0.

theorem ParallelPostulate.HyperbolicPlane.euclid_sas {A B C D E F : ℝ × ℝ} (hAB : A ≠ B) (hAC : A ≠ C) (hBC : B ≠ C) (hDE : D ≠ E) (hDF : D ≠ F) (hEF : E ≠ F) (h1 : apart 0 A B = apart 0 D E) (h2 : apart 0 A C = apart 0 D F) (h3 : kleinAngle 0 A B C = kleinAngle 0 D E F) : apart 0 B C = apart 0 E F ∧ kleinAngle 0 B A C = kleinAngle 0 E D F ∧ kleinAngle 0 C A B = kleinAngle 0 F D E

Side, angle, side under the bound 0.

The plane of a bound that is not positive: congruence with apart

theorem ParallelPostulate.HyperbolicPlane.apart_eq_iff_kleinDist_eq {κ : ℝ} (hκ : κ < 0) {A B C D : ℝ × ℝ} (hA : A ∈ plane κ) (hB : B ∈ plane κ) (hC : C ∈ plane κ) (hD : D ∈ plane κ) : apart κ A B = apart κ C D ↔ kleinDist κ A B = kleinDist κ C D

theorem ParallelPostulate.HyperbolicPlane.segment_construction_apart {κ : ℝ} (hκ : κ ≤ 0) {A B O D : ℝ × ℝ} (hA : A ∈ plane κ) (hB : B ∈ plane κ) (hO : O ∈ plane κ) (hAB : A ≠ B) (hOD : O ≠ D) : ∃! X : ℝ × ℝ, X ∈ plane κ ∧ OnRay O D X ∧ apart κ A B = apart κ O X

C1 with apart, under a bound that is not positive.

theorem ParallelPostulate.HyperbolicPlane.segment_addition_apart {κ : ℝ} (hκ : κ ≤ 0) {A B C D E F : ℝ × ℝ} (hA : A ∈ plane κ) (hC : C ∈ plane κ) (hD : D ∈ plane κ) (hF : F ∈ plane κ) (hABC : Between A B C) (hDEF : Between D E F) (h1 : apart κ A B = apart κ D E) (h2 : apart κ B C = apart κ E F) : apart κ A C = apart κ D F

C3 with apart, under a bound that is not positive.

theorem ParallelPostulate.HyperbolicPlane.sas_apart {κ : ℝ} (hκ : κ ≤ 0) {A B C D E F : ℝ × ℝ} (hA : A ∈ plane κ) (hB : B ∈ plane κ) (hC : C ∈ plane κ) (hD : D ∈ plane κ) (hE : E ∈ plane κ) (hF : F ∈ plane κ) (hAB : A ≠ B) (hAC : A ≠ C) (hBC : B ≠ C) (hDE : D ≠ E) (hDF : D ≠ F) (hEF : E ≠ F) (h1 : apart κ A B = apart κ D E) (h2 : apart κ A C = apart κ D F) (h3 : kleinAngle κ A B C = kleinAngle κ D E F) : apart κ B C = apart κ E F ∧ kleinAngle κ B A C = kleinAngle κ E D F ∧ kleinAngle κ C A B = kleinAngle κ F D E

C6 with apart, under a bound that is not positive.

The figure of the three-dimensions section under the bound -1

Example H10 lays the figure of the three-dimensions section in the plane of the bound -1, with fractions for numbers: it meets the hypotheses of the postulate there, and its lines b and c meet only outside the plane. Theorem H14 lays the same figure among the pairs of real numbers, measures its two interior angles with kleinAngle, a right angle and the angle whose cosine is 3 / √409, and so shows that Euclid's fifth postulate, as he states it, fails under the bound -1.

Contents

• Example H10, the figure of the three-dimensions section under the bound -1: leaningFigure, leaningFigure_within, leaningFigure_values, leaningFigure_hypotheses, leaningFigure_numbers, leaningFigure_meets_beyond, leaningFigure_never_meets, leaningFigure_angles
• Theorem H14, Euclid's fifth postulate fails under the bound -1: EuclidFifth, realLeaningFigure, realLeaningFigure_within, realLeaningFigure_sides, realLeaningFigure_angle_a0, realLeaningFigure_angle_a1, realLeaningFigure_angle_a1_lt, realLeaningFigure_angles, realLeaningFigure_never_meets, not_euclidFifth

The figure of the three-dimensions section under the bound

def ParallelPostulate.HyperbolicPlane.leaningFigure : Pairs.Figure ℚ

A figure within the bound -1. a runs from (0, 0) to (3/5, 0), b leaves a0 straight up, and c leaves a1 leaning toward b.

Equations

• One or more equations did not get rendered due to their size.

theorem ParallelPostulate.HyperbolicPlane.leaningFigure_within : leaningFigure.a.zero ∈ plane (-1) ∧ leaningFigure.a.one ∈ plane (-1) ∧ leaningFigure.b.one ∈ plane (-1) ∧ leaningFigure.c.one ∈ plane (-1)

Its zeros and its 1s are points of the plane of the bound -1.

theorem ParallelPostulate.HyperbolicPlane.leaningFigure_values : leaningFigure.a.side leaningFigure.b.one = 3 / 10 ∧ leaningFigure.a.side leaningFigure.c.one = 3 / 10 ∧ Pairs.cross leaningFigure.b.dir leaningFigure.c.dir = 3 / 100

The sides of b1 and of c1, and the cross product of the directions of b and c.

theorem ParallelPostulate.HyperbolicPlane.leaningFigure_hypotheses : 0 < leaningFigure.a.side leaningFigure.b.one ∧ 0 < leaningFigure.a.side leaningFigure.c.one ∧ 0 < Pairs.cross leaningFigure.b.dir leaningFigure.c.dir

It meets the three hypotheses of Theorem E4 (the three-dimensions section).

theorem ParallelPostulate.HyperbolicPlane.leaningFigure_numbers : Pairs.cross leaningFigure.a.dir leaningFigure.c.dir / Pairs.cross leaningFigure.b.dir leaningFigure.c.dir = 10 ∧ Pairs.cross leaningFigure.a.dir leaningFigure.b.dir / Pairs.cross leaningFigure.b.dir leaningFigure.c.dir = 10

The two numbers at which Theorem E4 (the three-dimensions section) has b and c meet are both 10.

theorem ParallelPostulate.HyperbolicPlane.leaningFigure_meets_beyond : leaningFigure.b.pt 10 = (0, 5) ∧ leaningFigure.c.pt 10 = (0, 5) ∧ (0, 5) ∉ plane (-1)

As dimensions, b and c meet at the number 10 of each, at the pair (0, 5), which is not a point of the plane.

theorem ParallelPostulate.HyperbolicPlane.leaningFigure_never_meets : leaningFigure.b.points ∩ plane (-1) ∩ (leaningFigure.c.points ∩ plane (-1)) = ∅

In the plane of the bound -1 the lines of b and c do not meet.

theorem ParallelPostulate.HyperbolicPlane.leaningFigure_angles : leaningFigure.a.dir.1 * leaningFigure.b.dir.1 + leaningFigure.a.dir.2 * leaningFigure.b.dir.2 = 0 ∧ (4 / 5) ^ 2 = 1 + -1 * (-3 / 5) ^ 2 ∧ shift (-1) (-3 / 5) (4 / 5) leaningFigure.a.one = (0, 0) ∧ shift (-1) (-3 / 5) (4 / 5) leaningFigure.a.zero = (-3 / 5, 0) ∧ shift (-1) (-3 / 5) (4 / 5) leaningFigure.c.one = (-15 / 169, 100 / 169) ∧ 0 < -15 / 169 * (-3 / 5) + 100 / 169 * 0

The two interior angles of the figure, as far as numbers can show them. At a0, which is (0, 0), the directions of a and b have the inner product 0. The motion along the first axis with a = -3/5 and w = 4/5 takes a1 to (0, 0), a0 to (-3/5, 0), and c1 to (-15/169, 100/169). So after the motion c leaves (0, 0), and the inner product of its direction with the direction of a run backwards is positive.

Euclid's fifth postulate under the bound -1

The figure of Example H10, with real numbers, and its two interior angles measured with kleinAngle.

def ParallelPostulate.HyperbolicPlane.EuclidFifth (κ : ℝ) : Prop

Euclid's fifth postulate in the plane of the bound κ, with the angles of kleinAngle. Let a fall on b and c, with its zero, its 1, and b1 and c1 points of the plane. Let b1 and c1 lie on the left of a, and let the two interior angles on that side be together less than two right angles. Then b and c, produced on that side, meet at a point of the plane, on that side.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ParallelPostulate.HyperbolicPlane.realLeaningFigure : Pairs.Figure ℝ

The figure of Example H10, with real numbers.

Equations

• One or more equations did not get rendered due to their size.

theorem ParallelPostulate.HyperbolicPlane.realLeaningFigure_within : realLeaningFigure.a.zero ∈ plane (-1) ∧ realLeaningFigure.a.one ∈ plane (-1) ∧ realLeaningFigure.b.one ∈ plane (-1) ∧ realLeaningFigure.c.one ∈ plane (-1)

Its zeros and its 1s are points of the plane of the bound -1.

theorem ParallelPostulate.HyperbolicPlane.realLeaningFigure_sides : 0 < realLeaningFigure.a.side realLeaningFigure.b.one ∧ 0 < realLeaningFigure.a.side realLeaningFigure.c.one

b1 and c1 lie on the left of a.

theorem ParallelPostulate.HyperbolicPlane.realLeaningFigure_angle_a0 : kleinAngle (-1) realLeaningFigure.a.zero realLeaningFigure.a.one realLeaningFigure.b.one = Real.pi / 2

The interior angle at a0 is a right angle.

theorem ParallelPostulate.HyperbolicPlane.realLeaningFigure_angle_a1 : kleinAngle (-1) realLeaningFigure.a.one realLeaningFigure.a.zero realLeaningFigure.c.one = Real.arccos (3 / √409)

The interior angle at a1 is the angle whose cosine is 3 / √409, about 81.5 degrees. With the angles of Euclid it would be the angle whose cosine is 3 / √634.

theorem ParallelPostulate.HyperbolicPlane.realLeaningFigure_angle_a1_lt : kleinAngle (-1) realLeaningFigure.a.one realLeaningFigure.a.zero realLeaningFigure.c.one < Real.pi / 2

The interior angle at a1 is less than a right angle.

theorem ParallelPostulate.HyperbolicPlane.realLeaningFigure_angles : kleinAngle (-1) realLeaningFigure.a.zero realLeaningFigure.a.one realLeaningFigure.b.one + kleinAngle (-1) realLeaningFigure.a.one realLeaningFigure.a.zero realLeaningFigure.c.one < Real.pi

The two interior angles are together less than two right angles.

theorem ParallelPostulate.HyperbolicPlane.realLeaningFigure_never_meets : realLeaningFigure.b.points ∩ plane (-1) ∩ (realLeaningFigure.c.points ∩ plane (-1)) = ∅

In the plane of the bound -1 the lines of b and c do not meet, on either side of a. As dimensions they meet at the pair (0, 5), which is not a point of the plane.

theorem ParallelPostulate.HyperbolicPlane.not_euclidFifth : ¬EuclidFifth (-1)

Theorem H14. Euclid's fifth postulate fails in the plane of the bound -1. The figure of Example H10 meets every hypothesis: its points are points of the plane, b1 and c1 lie on the left of a, and the two interior angles on that side, a right angle and the angle whose cosine is 3 / √409, are together less than two right angles. But b and c have no point of the plane in common.

The plane of a bound as a Hilbert plane

model κ makes a Hilbert plane of the plane of a bound κ that is not positive: its points and its lines, its Between, apart for segments and kleinAngle for angles.

Contents

• the model: Pt, Ln, mlies, mbtw, msegCong, mangCong, lineThrough, model_I1 to model_I3, model_B1 to model_B4, model_onRay, model_onRay_of, model_C1, model_side_ne_zero, model_sameSide_iff, model_C4, model_C6, model

The plane of a bound as a Hilbert plane

@[reducible, inline]

abbrev ParallelPostulate.Hilbert.Pt (κ : ℝ) : Type

The points of the plane of the bound κ.

Equations

• ParallelPostulate.Hilbert.Pt κ = { p : ℝ × ℝ // p ∈ ParallelPostulate.HyperbolicPlane.plane κ }

@[reducible, inline]

abbrev ParallelPostulate.Hilbert.Ln (κ : ℝ) : Type

The lines of the plane of the bound κ.

Equations

• ParallelPostulate.Hilbert.Ln κ = { S : Set (ℝ × ℝ) // ParallelPostulate.HyperbolicPlane.IsLine (ParallelPostulate.HyperbolicPlane.plane κ) S }

def ParallelPostulate.Hilbert.mlies (κ : ℝ) (p : Pt κ) (l : Ln κ) : Prop

A point lies on a line.

Equations

• ParallelPostulate.Hilbert.mlies κ p l = (↑p ∈ ↑l)

def ParallelPostulate.Hilbert.mbtw (κ : ℝ) (A B C : Pt κ) : Prop

Betweenness is the file's Between.

Equations

• ParallelPostulate.Hilbert.mbtw κ A B C = ParallelPostulate.HyperbolicPlane.Between ↑A ↑B ↑C

def ParallelPostulate.Hilbert.msegCong (κ : ℝ) (A B C D : Pt κ) : Prop

Two segments are congruent when apart is the same for both.

Equations

• ParallelPostulate.Hilbert.msegCong κ A B C D = (ParallelPostulate.HyperbolicPlane.apart κ ↑A ↑B = ParallelPostulate.HyperbolicPlane.apart κ ↑C ↑D)

def ParallelPostulate.Hilbert.mangCong (κ : ℝ) (A B C D E F : Pt κ) : Prop

The angle ABC is congruent to DEF when kleinAngle is the same at B and at E.

Equations

• ParallelPostulate.Hilbert.mangCong κ A B C D E F = (ParallelPostulate.HyperbolicPlane.kleinAngle κ ↑B ↑A ↑C = ParallelPostulate.HyperbolicPlane.kleinAngle κ ↑E ↑D ↑F)

def ParallelPostulate.Hilbert.lineThrough {κ : ℝ} (A B : Pt κ) (h : ↑A ≠ ↑B) : Ln κ

The line through two different points of the plane.

Equations

• ParallelPostulate.Hilbert.lineThrough A B h = ⟨{ zero := ↑A, one := ↑B }.points ∩ ParallelPostulate.HyperbolicPlane.plane κ, ⋯⟩

theorem ParallelPostulate.Hilbert.lies_lineThrough_left {κ : ℝ} (A B : Pt κ) (h : ↑A ≠ ↑B) : mlies κ A (lineThrough A B h)

theorem ParallelPostulate.Hilbert.lies_lineThrough_right {κ : ℝ} (A B : Pt κ) (h : ↑A ≠ ↑B) : mlies κ B (lineThrough A B h)

theorem ParallelPostulate.Hilbert.model_I1 (κ : ℝ) (A B : Pt κ) : A ≠ B → ∃! l : Ln κ, mlies κ A l ∧ mlies κ B l

theorem ParallelPostulate.Hilbert.model_I2 (κ : ℝ) (l : Ln κ) : ∃ (A : Pt κ) (B : Pt κ), A ≠ B ∧ mlies κ A l ∧ mlies κ B l

theorem ParallelPostulate.Hilbert.model_I3 (κ : ℝ) : ∃ (A : Pt κ) (B : Pt κ) (C : Pt κ), ¬Collinear (mlies κ) A B C

theorem ParallelPostulate.Hilbert.model_B1 (κ : ℝ) (A B C : Pt κ) : mbtw κ A B C → A ≠ B ∧ B ≠ C ∧ A ≠ C ∧ Collinear (mlies κ) A B C ∧ mbtw κ C B A

theorem ParallelPostulate.Hilbert.model_B2 (κ : ℝ) (A B : Pt κ) : A ≠ B → ∃ (C : Pt κ), mbtw κ A B C

theorem ParallelPostulate.Hilbert.model_B3 (κ : ℝ) (A B C : Pt κ) : A ≠ B → B ≠ C → A ≠ C → Collinear (mlies κ) A B C → (mbtw κ A B C ∨ mbtw κ B A C ∨ mbtw κ A C B) ∧ ¬(mbtw κ A B C ∧ mbtw κ B A C) ∧ ¬(mbtw κ A B C ∧ mbtw κ A C B) ∧ ¬(mbtw κ B A C ∧ mbtw κ A C B)

theorem ParallelPostulate.Hilbert.model_B4 (κ : ℝ) (A B C : Pt κ) (l : Ln κ) : ¬Collinear (mlies κ) A B C → ¬mlies κ A l → ¬mlies κ B l → ¬mlies κ C l → (∃ (D : Pt κ), mlies κ D l ∧ mbtw κ A D B) → ∃ (E : Pt κ), mlies κ E l ∧ (mbtw κ A E C ∨ mbtw κ B E C)

theorem ParallelPostulate.Hilbert.model_onRay {κ : ℝ} {O A X : Pt κ} (h : OnRay (mbtw κ) O A X) : HyperbolicPlane.OnRay ↑O ↑A ↑X

A point on a ray, as Hilbert has it, in the plane of a bound.

theorem ParallelPostulate.Hilbert.model_onRay_of {κ : ℝ} {O A X : Pt κ} (hOA : ↑O ≠ ↑A) (h : HyperbolicPlane.OnRay ↑O ↑A ↑X) : OnRay (mbtw κ) O A X

theorem ParallelPostulate.Hilbert.model_C1 (κ : ℝ) (hκ : κ ≤ 0) (A B C R : Pt κ) : A ≠ B → C ≠ R → ∃! D : Pt κ, OnRay (mbtw κ) C R D ∧ msegCong κ A B C D

theorem ParallelPostulate.Hilbert.model_side_ne_zero {κ : ℝ} {A B C : Pt κ} (h : ¬Collinear (mlies κ) A B C) : { zero := ↑B, one := ↑A }.side ↑C ≠ 0

Three points of the plane that are not on one line give a side that is not 0.

theorem ParallelPostulate.Hilbert.model_sameSide_iff {κ : ℝ} {D F : Pt κ} {l : Ln κ} (hD : mlies κ D l) (hF : mlies κ F l) (hDF : ↑D ≠ ↑F) (E G : Pt κ) : SameSide (mlies κ) (mbtw κ) l E G ↔ HyperbolicPlane.SameSide ↑D ↑F ↑E ↑G

Hilbert's sides of a line, in the plane of a bound, are the signs of side.

theorem ParallelPostulate.Hilbert.model_C4 (κ : ℝ) (A B C D F G : Pt κ) (l : Ln κ) : ¬Collinear (mlies κ) A B C → D ≠ F → mlies κ D l → mlies κ F l → ¬mlies κ G l → (∃ (E : Pt κ), SameSide (mlies κ) (mbtw κ) l E G ∧ mangCong κ A B C E D F) ∧ ∀ (E E' : Pt κ), SameSide (mlies κ) (mbtw κ) l E G → mangCong κ A B C E D F → SameSide (mlies κ) (mbtw κ) l E' G → mangCong κ A B C E' D F → OnRay (mbtw κ) D E E'

theorem ParallelPostulate.Hilbert.model_C6 (κ : ℝ) (hκ : κ ≤ 0) (A B C D E F : Pt κ) : ¬Collinear (mlies κ) A B C → ¬Collinear (mlies κ) D E F → msegCong κ A B D E → msegCong κ A C D F → mangCong κ B A C E D F → msegCong κ B C E F ∧ mangCong κ A B C D E F ∧ mangCong κ A C B D F E

noncomputable def ParallelPostulate.Hilbert.model (κ : ℝ) (hκ : κ ≤ 0) : HilbertPlane (Pt κ) (Ln κ)

The plane of a bound that is not positive is a Hilbert plane.

Equations

• One or more equations did not get rendered due to their size.

The axioms of continuity in the plane of a bound

The plane of every bound that is not positive meets Dedekind's axiom and Archimedes' axiom. A line is an interval of numbers, so Dedekind's axiom is the least upper bound of the real numbers. Archimedes' axiom follows from a length of segments that adds along a segment: Klein's distance under a negative bound, and the square root of apart under the bound 0.

Contents

• a cut of an interval of real numbers: cut_point_ordered, cut_point
• Dedekind's axiom in the plane of a bound: model_dedekind
• Archimedes' axiom in the plane of a bound: archimedes_of_length, model_archimedes

A cut of an interval of real numbers

theorem ParallelPostulate.Hilbert.cut_point_ordered {I S T : Set ℝ} (hI : ∀ a ∈ I, ∀ b ∈ I, ∀ (c : ℝ), a ≤ c → c ≤ b → c ∈ I) (hST : ∀ (t : ℝ), t ∈ I ↔ t ∈ S ∨ t ∈ T) (hSne : S.Nonempty) (hTne : T.Nonempty) (hsep : ∀ s ∈ S, ∀ t ∈ T, s < t) : ∃! c : ℝ, c ∈ I ∧ ∀ a ∈ S, ∀ b ∈ T, a ≠ c → b ≠ c → HyperbolicPlane.StrictBetween a c b

A cut of an interval, with the first part below the second, has one cut point.

theorem ParallelPostulate.Hilbert.cut_point {I S T : Set ℝ} (hI : ∀ a ∈ I, ∀ b ∈ I, ∀ (c : ℝ), a ≤ c → c ≤ b → c ∈ I) (hST : ∀ (t : ℝ), t ∈ I ↔ t ∈ S ∨ t ∈ T) (hdisj : ∀ t ∈ S, t ∉ T) (hSne : S.Nonempty) (hTne : T.Nonempty) (hS : ∀ x ∈ S, ∀ y ∈ T, ∀ z ∈ T, ¬HyperbolicPlane.StrictBetween y x z) (hT : ∀ x ∈ T, ∀ y ∈ S, ∀ z ∈ S, ¬HyperbolicPlane.StrictBetween y x z) : ∃! c : ℝ, c ∈ I ∧ ∀ a ∈ S, ∀ b ∈ T, a ≠ c → b ≠ c → HyperbolicPlane.StrictBetween a c b

A cut of an interval of real numbers has one cut point.

Dedekind's axiom in the plane of a bound

theorem ParallelPostulate.Hilbert.model_dedekind (κ : ℝ) (hκ : κ ≤ 0) : (model κ hκ).Dedekind

Dedekind's axiom holds in the plane of a bound that is not positive.

Archimedes' axiom in the plane of a bound

theorem ParallelPostulate.Hilbert.archimedes_of_length {κ : ℝ} (hκ : κ ≤ 0) (len : ℝ × ℝ → ℝ × ℝ → ℝ) (hcong : ∀ {P Q R S : ℝ × ℝ}, P ∈ HyperbolicPlane.plane κ → Q ∈ HyperbolicPlane.plane κ → R ∈ HyperbolicPlane.plane κ → S ∈ HyperbolicPlane.plane κ → (HyperbolicPlane.apart κ P Q = HyperbolicPlane.apart κ R S ↔ len P Q = len R S)) (hadd : ∀ {A B C : ℝ × ℝ}, A ∈ HyperbolicPlane.plane κ → C ∈ HyperbolicPlane.plane κ → HyperbolicPlane.Between A B C → len A C = len A B + len B C) (hpos : ∀ {P Q : ℝ × ℝ}, P ∈ HyperbolicPlane.plane κ → Q ∈ HyperbolicPlane.plane κ → P ≠ Q → 0 < len P Q) (hzero : ∀ {P : ℝ × ℝ}, P ∈ HyperbolicPlane.plane κ → len P P = 0) (hexist : ∀ {O D : ℝ × ℝ}, O ∈ HyperbolicPlane.plane κ → O ≠ D → ∀ (d : ℝ), 0 < d → ∃ (t : ℝ), 0 < t ∧ { zero := O, one := D }.pt t ∈ HyperbolicPlane.plane κ ∧ len O ({ zero := O, one := D }.pt t) = d) : (model κ hκ).Archimedes

Archimedes' axiom, from a length. Suppose a length of segments of the plane is 0 for a point and positive for two different points, adds along a segment, is equal for two segments exactly when apart is, and takes every positive value on every ray. Then the plane meets Archimedes' axiom.

theorem ParallelPostulate.Hilbert.model_archimedes (κ : ℝ) (hκ : κ ≤ 0) : (model κ hκ).Archimedes

Archimedes' axiom holds in the plane of a bound that is not positive. Under a negative bound the length is Klein's distance; under the bound 0 it is the square root of apart.

The independence of the parallel postulate

euclidPlane, the plane of the bound 0, and kleinPlane, the plane of the bound -1, are Hilbert planes that meet the axioms of continuity. Playfair's axiom holds in the first and fails in the second, so it is independent of Hilbert's axioms, with continuity or without it.

Contents

• the two planes: euclidPlane, kleinPlane, euclidPlane_playfair, kleinPlane_not_playfair
• the independence: playfair_independent, playfair_not_consequence, not_playfair_not_consequence, playfair_independent_continuous

@[reducible, inline]

noncomputable abbrev ParallelPostulate.Hilbert.euclidPlane : HilbertPlane (Pt 0) (Ln 0)

Euclid's plane: the plane of the bound 0.

Equations

• ParallelPostulate.Hilbert.euclidPlane = ParallelPostulate.Hilbert.model 0 ParallelPostulate.Hilbert.euclidPlane._proof_1

@[reducible, inline]

noncomputable abbrev ParallelPostulate.Hilbert.kleinPlane : HilbertPlane (Pt (-1)) (Ln (-1))

Klein's plane: the plane of the bound -1.

Equations

• ParallelPostulate.Hilbert.kleinPlane = ParallelPostulate.Hilbert.model (-1) ParallelPostulate.Hilbert.kleinPlane._proof_1

theorem ParallelPostulate.Hilbert.euclidPlane_playfair : euclidPlane.Playfair

Playfair's axiom holds in Euclid's plane.

theorem ParallelPostulate.Hilbert.kleinPlane_not_playfair : ¬kleinPlane.Playfair

Playfair's axiom fails in Klein's plane.

theorem ParallelPostulate.Hilbert.playfair_independent : (∃ (P : Type) (L : Type) (H : HilbertPlane P L), H.Playfair) ∧ ∃ (P : Type) (L : Type) (H : HilbertPlane P L), ¬H.Playfair

The parallel postulate is independent of the axioms of a Hilbert plane. There is a Hilbert plane in which Playfair's axiom holds, and one in which it fails.

theorem ParallelPostulate.Hilbert.playfair_not_consequence : ¬∀ (P L : Type) (H : HilbertPlane P L), H.Playfair

Playfair's axiom does not follow from the axioms of a Hilbert plane.

theorem ParallelPostulate.Hilbert.not_playfair_not_consequence : ¬∀ (P L : Type) (H : HilbertPlane P L), ¬H.Playfair

Nor does its negation.

The independence, with continuity

theorem ParallelPostulate.Hilbert.playfair_independent_continuous : (∃ (P : Type) (L : Type) (H : HilbertPlane P L), H.Archimedes ∧ H.Dedekind ∧ H.Playfair) ∧ ∃ (P : Type) (L : Type) (H : HilbertPlane P L), H.Archimedes ∧ H.Dedekind ∧ ¬H.Playfair

The parallel postulate is independent of Hilbert's axioms, with continuity. Both planes meet Archimedes' axiom and Dedekind's axiom; Playfair's axiom holds in the one and fails in the other.