Coordinate incidence, order, and parallels

ParallelPostulate.Pairs develops dimensions and figures over commutative rings and fields. ParallelPostulate.HyperbolicPlane develops bounded affine planes, line incidence, Pasch order, and the number of parallels over ordered fields. This module uses no calculus, curvature, or path-distance imports. Analytic geometry and the concrete Hilbert models are in LeanPool/ParallelPostulate.lean; the synthetic axiom bundle is in Hilbert.lean.

Dimensions laid among the pairs of numbers

A dimension is a number line with its own zero and its own 1, laid among the pairs of numbers of a ring K: Dim, with its direction Dim.dir, its pairs Dim.pt and Dim.points, and the side Dim.side of a pair. cross is the cross product of two directions. A figure, Figure, is three dimensions a, b, c with the two constraints

a0 = b0        a1 = c0

so that a is the line that falls on the two others. The entry module and the bounded-plane section build on these, in the namespace ParallelPostulate.Pairs.

Contents

• a dimension, its direction, its pairs, its sides: Dim, Dim.dir, Dim.pt, Dim.points, Dim.side, cross
• a dimension with its zero moved: Dim.rebase, Dim.rebase_dir, Dim.rebase_points, Dim.rebase_zero_ne_one, Dim.cross_rebase
• small facts about a dimension: Dim.pt_zero, Dim.pt_one, Dim.zero_mem, Dim.one_mem, Dim.dir_ne_zero, Dim.zero_ne_one_of_dir, Dim.side_eq_zero_of_mem, Dim.side_through, Dim.through_subset
• the figure, with the two constraints: Figure, Figure.a0_eq_b0, Figure.a1_eq_c0, Figure.a_meets_b, Figure.a_meets_c, Figure.side_b_one, Figure.side_c_one, Figure.side_b_pt
• two right angles, and the figure with a run backwards: Figure.never_meet_of_two_right_angles, Figure.reverse, Figure.reverse_side, Figure.reverse_dir, Figure.reverse_cross
• with fractions: cramer_aux, Figure.meet_eq, Figure.meet_unique, exists_mul_of_cross_eq_zero, Dim.pt_injective, Dim.mem_points_of_side_eq_zero, Dim.points_eq_through

structure ParallelPostulate.Pairs.Dim (K : Type u_2) : Type u_2

A dimension laid in the plane: a number line with its own zero and its own 1.

• zero : K × K

  The point where the dimension has its zero.

• one : K × K

  The point where the dimension has its 1.

def ParallelPostulate.Pairs.cross {K : Type u_1} [CommRing K] (u v : K × K) : K

The cross product of two directions. It is positive when the second is a turn to the left of the first, by less than two right angles.

Equations

• ParallelPostulate.Pairs.cross u v = u.1 * v.2 - u.2 * v.1

def ParallelPostulate.Pairs.Dim.dir {K : Type u_1} [CommRing K] (L : Dim K) : K × K

The direction of a dimension, from its zero to its 1.

Equations

• L.dir = (L.one.1 - L.zero.1, L.one.2 - L.zero.2)

def ParallelPostulate.Pairs.Dim.pt {K : Type u_1} [CommRing K] (L : Dim K) (t : K) : K × K

The point of the dimension at the number t.

Equations

• L.pt t = (L.zero.1 + t * (L.one.1 - L.zero.1), L.zero.2 + t * (L.one.2 - L.zero.2))

def ParallelPostulate.Pairs.Dim.side {K : Type u_1} [CommRing K] (L : Dim K) (P : K × K) : K

The side of the dimension on which a point lies: positive on its left, negative on its right, and zero on the dimension itself.

Equations

• L.side P = ParallelPostulate.Pairs.cross L.dir (P.1 - L.zero.1, P.2 - L.zero.2)

def ParallelPostulate.Pairs.Dim.points {K : Type u_1} [CommRing K] (L : Dim K) : Set (K × K)

The points of a dimension.

Equations

• L.points = Set.range L.pt

def ParallelPostulate.Pairs.Dim.rebase {K : Type u_1} [CommRing K] (M : Dim K) (P : K × K) : Dim K

The dimension M with its zero moved to the point P. It keeps its direction.

Equations

• M.rebase P = { zero := P, one := (P.1 + (M.one.1 - M.zero.1), P.2 + (M.one.2 - M.zero.2)) }

theorem ParallelPostulate.Pairs.Dim.pt_zero {K : Type u_1} [CommRing K] (L : Dim K) : L.pt 0 = L.zero

theorem ParallelPostulate.Pairs.Dim.pt_one {K : Type u_1} [CommRing K] (L : Dim K) : L.pt 1 = L.one

theorem ParallelPostulate.Pairs.Dim.zero_mem {K : Type u_1} [CommRing K] (L : Dim K) : L.zero ∈ L.points

theorem ParallelPostulate.Pairs.Dim.one_mem {K : Type u_1} [CommRing K] (L : Dim K) : L.one ∈ L.points

theorem ParallelPostulate.Pairs.Dim.dir_ne_zero {K : Type u_1} [CommRing K] (L : Dim K) (hL : L.zero ≠ L.one) : L.dir ≠ (0, 0)

theorem ParallelPostulate.Pairs.Dim.zero_ne_one_of_dir {K : Type u_1} [CommRing K] (L : Dim K) (h : L.dir ≠ (0, 0)) : L.zero ≠ L.one

theorem ParallelPostulate.Pairs.Dim.rebase_dir {K : Type u_1} [CommRing K] (M : Dim K) (P : K × K) : (M.rebase P).dir = M.dir

theorem ParallelPostulate.Pairs.Dim.rebase_points {K : Type u_1} [CommRing K] (M : Dim K) {P : K × K} (hP : P ∈ M.points) : (M.rebase P).points = M.points

A dimension can be given its zero at any of its points: it keeps its points.

theorem ParallelPostulate.Pairs.Dim.rebase_zero_ne_one {K : Type u_1} [CommRing K] (L : Dim K) (hL : L.zero ≠ L.one) (P : K × K) : (L.rebase P).zero ≠ (L.rebase P).one

theorem ParallelPostulate.Pairs.Dim.cross_rebase {K : Type u_1} [CommRing K] (L : Dim K) (P : K × K) : cross L.dir (L.rebase P).dir = 0

The moved dimension has the direction of the dimension it was made from.

theorem ParallelPostulate.Pairs.Dim.side_eq_zero_of_mem {K : Type u_1} [CommRing K] (L : Dim K) {P : K × K} (hP : P ∈ L.points) : L.side P = 0

The side of a pair of the dimension is zero.

theorem ParallelPostulate.Pairs.Dim.side_through {K : Type u_1} [CommRing K] (L : Dim K) (A C : K × K) (u : K) : L.side ({ zero := A, one := C }.pt u) = (1 - u) * L.side A + u * L.side C

Along the dimension from A to C, the side changes evenly from the side of A to the side of C.

theorem ParallelPostulate.Pairs.Dim.through_subset {K : Type u_1} [CommRing K] (L : Dim K) {A B : K × K} (hA : A ∈ L.points) (hB : B ∈ L.points) : { zero := A, one := B }.points ⊆ L.points

The dimension through two pairs of L has its pairs among those of L.

structure ParallelPostulate.Pairs.Figure (K : Type u_2) : Type u_2

The figure: three dimensions with a0 = b0 and a1 = c0, read as points.

• a : Dim K

  The straight line that falls on the two others.

• b : Dim K

  The line that leaves a at a0.

• c : Dim K

  The line that leaves a at a1.

• a0_eq_b0 : self.a.zero = self.b.zero

  The first constraint.

• a1_eq_c0 : self.a.one = self.c.zero

  The second constraint.

theorem ParallelPostulate.Pairs.Figure.a_meets_b {K : Type u_1} [CommRing K] (F : Figure K) : F.a.pt 0 = F.b.pt 0

a meets b where a has its zero.

theorem ParallelPostulate.Pairs.Figure.a_meets_c {K : Type u_1} [CommRing K] (F : Figure K) : F.a.pt 1 = F.c.pt 0

a meets c where a has its 1.

theorem ParallelPostulate.Pairs.Figure.side_b_one {K : Type u_1} [CommRing K] (F : Figure K) : F.a.side F.b.one = cross F.a.dir F.b.dir

theorem ParallelPostulate.Pairs.Figure.side_c_one {K : Type u_1} [CommRing K] (F : Figure K) : F.a.side F.c.one = cross F.a.dir F.c.dir

theorem ParallelPostulate.Pairs.Figure.side_b_pt {K : Type u_1} [CommRing K] (F : Figure K) (t : K) : F.a.side (F.b.pt t) = t * cross F.a.dir F.b.dir

theorem ParallelPostulate.Pairs.Figure.never_meet_of_two_right_angles {K : Type u_1} [CommRing K] (F : Figure K) (hc : F.a.side F.c.one ≠ 0) (hsum : cross F.b.dir F.c.dir = 0) (t u : K) : F.b.pt t ≠ F.c.pt u

Two right angles: the lines never meet. If the side of c1 is not zero, and the cross product of the directions of b and c is zero, the two lines have no point in common.

def ParallelPostulate.Pairs.Figure.reverse {K : Type u_1} (F : Figure K) : Figure K

The same figure with a run backwards. It starts at a1 and ends at a0, so the line that leaves its zero is c and the line that leaves its 1 is b. Left and right of a change places.

Equations

• F.reverse = { a := { zero := F.a.one, one := F.a.zero }, b := F.c, c := F.b, a0_eq_b0 := ⋯, a1_eq_c0 := ⋯ }

theorem ParallelPostulate.Pairs.Figure.reverse_side {K : Type u_1} [CommRing K] (F : Figure K) (P : K × K) : F.reverse.a.side P = -F.a.side P

theorem ParallelPostulate.Pairs.Figure.reverse_dir {K : Type u_1} [CommRing K] (F : Figure K) : F.reverse.a.dir = -F.a.dir

theorem ParallelPostulate.Pairs.Figure.reverse_cross {K : Type u_1} [CommRing K] (F : Figure K) : cross F.reverse.b.dir F.reverse.c.dir = -cross F.b.dir F.c.dir

theorem ParallelPostulate.Pairs.cramer_aux {K : Type u_1} [Field K] (o a' p x n m D : K) (hD : D ≠ 0) (h : (a' - o) * D = p * n - x * m) : o + n / D * p = a' + m / D * x

The one step that divides. If (a' - o) D = p n - x m, the point at n / D along p from o is the point at m / D along x from a'.

theorem ParallelPostulate.Pairs.Figure.meet_eq {K : Type u_1} [Field K] (F : Figure K) (hne : cross F.b.dir F.c.dir ≠ 0) : F.b.pt (cross F.a.dir F.c.dir / cross F.b.dir F.c.dir) = F.c.pt (cross F.a.dir F.b.dir / cross F.b.dir F.c.dir)

Where b and c meet, when the cross product of their directions is not zero.

theorem ParallelPostulate.Pairs.Figure.meet_unique {K : Type u_1} [Field K] (F : Figure K) (hne : cross F.b.dir F.c.dir ≠ 0) {t u t' u' : K} (h : F.b.pt t = F.c.pt u) (h' : F.b.pt t' = F.c.pt u') : t = t' ∧ u = u'

And they meet at one point only.

theorem ParallelPostulate.Pairs.exists_mul_of_cross_eq_zero {K : Type u_1} [Field K] {v w : K × K} (hv : v ≠ (0, 0)) (h : cross v w = 0) : ∃ (l : K), w = (l * v.1, l * v.2)

A direction with cross product zero against v is a multiple of v.

theorem ParallelPostulate.Pairs.Dim.pt_injective {K : Type u_1} [Field K] (M : Dim K) (hM : M.zero ≠ M.one) : Function.Injective M.pt

A dimension is a number line: different numbers are at different pairs.

theorem ParallelPostulate.Pairs.Dim.mem_points_of_side_eq_zero {K : Type u_1} [Field K] (L : Dim K) (hL : L.zero ≠ L.one) (P : K × K) (h : L.side P = 0) : P ∈ L.points

A pair whose side is zero is a pair of the dimension.

theorem ParallelPostulate.Pairs.Dim.points_eq_through {K : Type u_1} [Field K] (L : Dim K) {A B : K × K} (hA : A ∈ L.points) (hB : B ∈ L.points) (hAB : A ≠ B) : L.points = { zero := A, one := B }.points

Two different pairs of a dimension give the dimension: it has the pairs of the dimension from the one to the other.

The plane of a bound: lines, order and parallels

A plane is a set of pairs of numbers, and a line of a plane is what a dimension has in it. The plane of the bound κ, plane κ, has the pairs (x, y) with 0 < 1 + κ (x² + y²). This file proves Hilbert's statements on incidence and on order for it (Proposition H4 and between_trichotomy), and counts the parallels: one exactly when the bound is not negative, and infinitely many under a negative bound.

Contents

• a plane: any Set (K × K)
• what two dimensions have in common: common_of_cross_ne_zero, points_eq_of_two_common, no_common_of_cross_eq_zero, points_subset_of_cross_eq_zero, points_eq_of_cross_eq_zero
• a line of a plane, a plane open along the dimensions: IsLine, OpenAlong
• a line through P that does not meet L: Misses
• Euclid's line, the line toward a number of L: euclid, toward
• Theorem H1, the lines through P that do not meet L: miss_iff, misses_iff, euclid_misses, toward_misses, one_parallel_of_all_within
• Theorem H2, one parallel exactly when: toward_injective, euclid_ne_toward, one_parallel_iff, two_parallels_of_beyond, infinitely_many_parallels
• the choice, the bound: plane, mem_plane
• Proposition H3, the plane of a bound: plane_eq_univ, plane_zero, plane_stretch, plane_beyond, plane_beyond_infinite, zero_mem_plane, plane_mono, mem_plane_scale, plane_open_forward, plane_openAlong, plane_convex, bound_along, quad_pos, quad_nonpos
• a sum of two squares: sq_add_sq_pos
• Proposition H4, points, lines and order: line_through, IsLine.two_points, IsLine.exists_within, exists_three_points, exists_line_and_point, plane_exists_line_and_point, Between, Between.symm, Between.mem, Between.ne, Between.not_left, Between.not_right, exists_beyond, crosses, pasch
• Theorem H5, the parallels under a negative bound: hyperbolic_parallel_property, hyperbolic_two_parallels, hyperbolic_parallels
• Theorem H6, the plane of the three-dimensions section from the same choice: euclid_one_parallel, fifth_postulate_of_nonneg_bound
• Theorem H7, exactly when: one_parallel_iff_bound
• three points on a line: between_trichotomy, ne_of_side_ne_zero, IsLine.subset_plane, IsLine.eq_through
• the order of the numbers of a dimension: StrictBetween, between_pt_of_strictBetween, strictBetween_of_between_pt, pt_mem_plane_of_le

With fractions: what two dimensions have in common

theorem ParallelPostulate.HyperbolicPlane.common_of_cross_ne_zero {K : Type u_1} [Field K] (L M : Pairs.Dim K) (h : Pairs.cross L.dir M.dir ≠ 0) : ∃ Q ∈ L.points, Q ∈ M.points

Two dimensions have a pair in common if the cross product of their directions is not zero.

theorem ParallelPostulate.HyperbolicPlane.points_eq_of_two_common {K : Type u_1} [Field K] (L M : Pairs.Dim K) {A B : K × K} (hAB : A ≠ B) (hA : A ∈ L.points) (hB : B ∈ L.points) (hA' : A ∈ M.points) (hB' : B ∈ M.points) : L.points = M.points

Two dimensions with two different pairs in common have the same pairs.

theorem ParallelPostulate.HyperbolicPlane.no_common_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) {P : K × K} (hP : P ∈ M.points) (hPL : P ∉ L.points) {Q : K × K} (hQL : Q ∈ L.points) (hQM : Q ∈ M.points) : False

If the direction of M is a multiple of the direction of L, and M has a pair that is not a pair of L, the two have no pair in common.

theorem ParallelPostulate.HyperbolicPlane.points_subset_of_cross_eq_zero {K : Type u_1} [Field K] (L M M' : Pairs.Dim K) (hL : L.zero ≠ L.one) (hM' : M'.zero ≠ M'.one) (h : Pairs.cross L.dir M.dir = 0) (h' : Pairs.cross L.dir M'.dir = 0) {P : K × K} (hP : P ∈ M.points) (hP' : P ∈ M'.points) : M.points ⊆ M'.points

Let two dimensions pass through one pair, each with a direction that is a multiple of the direction of L. Then the pairs of the first are pairs of the second.

theorem ParallelPostulate.HyperbolicPlane.points_eq_of_cross_eq_zero {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) (h : Pairs.cross L.dir M.dir = 0) (h' : Pairs.cross L.dir M'.dir = 0) {P : K × K} (hP : P ∈ M.points) (hP' : P ∈ M'.points) : M.points = M'.points

Two dimensions through one pair, each with a direction that is a multiple of the direction of L, have the same pairs.

A plane, its lines, and the lines through a point that miss a line

A plane is any set of pairs: the pairs that are taken for points. Nothing is asked of it here, and no order of the numbers is used.

def ParallelPostulate.HyperbolicPlane.IsLine {K : Type u_1} [Field K] (Pl S : Set (K × K)) : Prop

A line of the plane Pl: what a dimension has in the plane, if it has anything there.

Equations

• ParallelPostulate.HyperbolicPlane.IsLine Pl S = ∃ (M : ParallelPostulate.Pairs.Dim K), M.zero ≠ M.one ∧ S = M.points ∩ Pl ∧ S.Nonempty

def ParallelPostulate.HyperbolicPlane.Misses {K : Type u_1} [Field K] (Pl : Set (K × K)) (L : Pairs.Dim K) (P : K × K) (S : Set (K × K)) : Prop

S is a line of the plane through P that does not meet the line of L.

Equations

• ParallelPostulate.HyperbolicPlane.Misses Pl L P S = (ParallelPostulate.HyperbolicPlane.IsLine Pl S ∧ P ∈ S ∧ S ∩ (L.points ∩ Pl) = ∅)

def ParallelPostulate.HyperbolicPlane.euclid {K : Type u_1} [Field K] (Pl : Set (K × K)) (L : Pairs.Dim K) (P : K × K) : Set (K × K)

Euclid's line: what the dimension through P with the direction of L has in the plane.

Equations

• ParallelPostulate.HyperbolicPlane.euclid Pl L P = (L.rebase P).points ∩ Pl

def ParallelPostulate.HyperbolicPlane.toward {K : Type u_1} [Field K] (Pl : Set (K × K)) (L : Pairs.Dim K) (P : K × K) (t : K) : Set (K × K)

What the dimension from P to the pair of L at the number t has in the plane.

Equations

• ParallelPostulate.HyperbolicPlane.toward Pl L P t = { zero := P, one := L.pt t }.points ∩ Pl

def ParallelPostulate.HyperbolicPlane.OpenAlong {K : Type u_1} [Field K] (Pl : Set (K × K)) : Prop

The plane is open along the dimensions: a dimension with its zero in the plane has another of its numbers in the plane.

Equations

• ParallelPostulate.HyperbolicPlane.OpenAlong Pl = ∀ (M : ParallelPostulate.Pairs.Dim K), M.zero ∈ Pl → ∃ (t : K), t ≠ 0 ∧ M.pt t ∈ Pl

theorem ParallelPostulate.HyperbolicPlane.line_through {K : Type u_1} [Field K] (Pl : Set (K × K)) {A B : K × K} (hA : A ∈ Pl) (hB : B ∈ Pl) (hAB : A ≠ B) : ∃! S : Set (K × K), IsLine Pl S ∧ A ∈ S ∧ B ∈ S

Two points are on one line, and on one only.

theorem ParallelPostulate.HyperbolicPlane.IsLine.exists_within {K : Type u_1} [Field K] {Pl S : Set (K × K)} (hopen : OpenAlong Pl) (hS : IsLine Pl S) : ∃ (M : Pairs.Dim K), M.zero ∈ Pl ∧ M.one ∈ Pl ∧ M.zero ≠ M.one ∧ S = M.points ∩ Pl

Every line of the plane is a dimension with its zero and its 1 in the plane, as far as it lies in the plane.

theorem ParallelPostulate.HyperbolicPlane.IsLine.two_points {K : Type u_1} [Field K] {Pl S : Set (K × K)} (hopen : OpenAlong Pl) (hS : IsLine Pl S) : ∃ (A : K × K) (B : K × K), A ≠ B ∧ A ∈ S ∧ B ∈ S

A line of the plane has two different points.

theorem ParallelPostulate.HyperbolicPlane.exists_line_and_point {K : Type u_1} [Field K] {Pl : Set (K × K)} (hopen : OpenAlong Pl) {A : K × K} (hA : A ∈ Pl) : ∃ (S : Set (K × K)) (P : K × K), IsLine Pl S ∧ P ∈ Pl ∧ P ∉ S

A plane that is open along the dimensions, and has a point, has a line and a point that is not on it.

theorem ParallelPostulate.HyperbolicPlane.miss_iff {K : Type u_1} [Field K] (Pl : Set (K × K)) (L M : Pairs.Dim K) (hL : L.zero ≠ L.one) {P : K × K} (hP : P ∈ M.points) (hPL : P ∉ L.points) : M.points ∩ Pl ∩ (L.points ∩ Pl) = ∅ ↔ Pairs.cross L.dir M.dir = 0 ∨ ∃ Q ∈ L.points, Q ∈ M.points ∧ Q ∉ Pl

When two lines of the plane do not meet. Let M pass through a pair that is not a pair of L. What M and L have in the plane has no point in common exactly when M has the direction of L, or the two dimensions meet at a pair that is not a point of the plane.

theorem ParallelPostulate.HyperbolicPlane.euclid_misses {K : Type u_1} [Field K] (Pl : Set (K × K)) (L : Pairs.Dim K) (hL : L.zero ≠ L.one) {P : K × K} (hP : P ∈ Pl) (hPL : P ∉ L.points) : Misses Pl L P (euclid Pl L P)

Euclid's line passes through P and does not meet L, in any plane.

theorem ParallelPostulate.HyperbolicPlane.toward_misses {K : Type u_1} [Field K] (Pl : Set (K × K)) (L : Pairs.Dim K) (hL : L.zero ≠ L.one) {P : K × K} (hP : P ∈ Pl) (hPL : P ∉ L.points) {t : K} (ht : L.pt t ∉ Pl) : Misses Pl L P (toward Pl L P t)

The line from P toward a pair of L that is not a point of the plane passes through P and does not meet L.

theorem ParallelPostulate.HyperbolicPlane.misses_iff {K : Type u_1} [Field K] (Pl : Set (K × K)) (L : Pairs.Dim K) (hL : L.zero ≠ L.one) {P : K × K} (hP : P ∈ Pl) (hPL : P ∉ L.points) (S : Set (K × K)) : Misses Pl L P S ↔ S = euclid Pl L P ∨ ∃ (t : K), L.pt t ∉ Pl ∧ S = toward Pl L P t

The lines through P that do not meet L. They are Euclid's line, and one line for each number of L whose pair is not a point of the plane. There are no others.

theorem ParallelPostulate.HyperbolicPlane.toward_injective {K : Type u_1} [Field K] (Pl : Set (K × K)) (hopen : OpenAlong Pl) (L : Pairs.Dim K) (hL : L.zero ≠ L.one) {P : K × K} (hP : P ∈ Pl) (hPL : P ∉ L.points) : Function.Injective (toward Pl L P)

Lines from P toward different numbers of L are different lines of the plane.

theorem ParallelPostulate.HyperbolicPlane.euclid_ne_toward {K : Type u_1} [Field K] (Pl : Set (K × K)) (hopen : OpenAlong Pl) (L : Pairs.Dim K) (hL : L.zero ≠ L.one) {P : K × K} (hP : P ∈ Pl) (hPL : P ∉ L.points) (t : K) : euclid Pl L P ≠ toward Pl L P t

Euclid's line is none of the lines toward a pair of L.

theorem ParallelPostulate.HyperbolicPlane.one_parallel_of_all_within {K : Type u_1} [Field K] (Pl : Set (K × K)) (L : Pairs.Dim K) (hL : L.zero ≠ L.one) {P : K × K} (hP : P ∈ Pl) (hPL : P ∉ L.points) (hall : ∀ (t : K), L.pt t ∈ Pl) : ∃! S : Set (K × K), Misses Pl L P S

If every number of L is a point of the plane, one line through P does not meet L, and only one.

theorem ParallelPostulate.HyperbolicPlane.two_parallels_of_beyond {K : Type u_1} [Field K] (Pl : Set (K × K)) (hopen : OpenAlong Pl) (L : Pairs.Dim K) (hL : L.zero ≠ L.one) {P : K × K} (hP : P ∈ Pl) (hPL : P ∉ L.points) {t : K} (ht : L.pt t ∉ Pl) : ∃ (S₁ : Set (K × K)) (S₂ : Set (K × K)), S₁ ≠ S₂ ∧ Misses Pl L P S₁ ∧ Misses Pl L P S₂

If a number of L is not a point of the plane, two different lines through P do not meet L.

theorem ParallelPostulate.HyperbolicPlane.one_parallel_iff {K : Type u_1} [Field K] (Pl : Set (K × K)) (hopen : OpenAlong Pl) (L : Pairs.Dim K) (hL : L.zero ≠ L.one) {P : K × K} (hP : P ∈ Pl) (hPL : P ∉ L.points) : (∃! S : Set (K × K), Misses Pl L P S) ↔ ∀ (t : K), L.pt t ∈ Pl

Playfair's postulate holds for L exactly when every number of L is a point of the plane.

theorem ParallelPostulate.HyperbolicPlane.infinitely_many_parallels {K : Type u_1} [Field K] (Pl : Set (K × K)) (hopen : OpenAlong Pl) (L : Pairs.Dim K) (hL : L.zero ≠ L.one) {P : K × K} (hP : P ∈ Pl) (hPL : P ∉ L.points) (hbeyond : {t : K | L.pt t ∉ Pl}.Infinite) : {S : Set (K × K) | Misses Pl L P S}.Infinite

If infinitely many numbers of L are not points of the plane, infinitely many lines through P do not meet L.

Identities that need no order

theorem ParallelPostulate.HyperbolicPlane.bound_along {K : Type u_1} [CommRing K] (κ : K) (M : Pairs.Dim K) (t : K) : 1 + κ * ((M.pt t).1 ^ 2 + (M.pt t).2 ^ 2) = 1 + κ * (M.zero.1 ^ 2 + M.zero.2 ^ 2) + 2 * κ * (M.zero.1 * M.dir.1 + M.zero.2 * M.dir.2) * t - -κ * (M.dir.1 ^ 2 + M.dir.2 ^ 2) * t ^ 2

The bound along a dimension is a quadratic in the number.

The choice: the bound

theorem ParallelPostulate.HyperbolicPlane.quad_pos {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (α β γ : K) (hα : 0 < α) (hγ : 0 ≤ γ) : ∃ (t : K), 0 < t ∧ 0 < α + β * t - γ * t ^ 2

Near its zero a quadratic is positive, if it is positive at its zero.

theorem ParallelPostulate.HyperbolicPlane.quad_nonpos {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (α β γ : K) (hγ : 0 < γ) : ∃ (T : K), ∀ (t : K), T ≤ t → α + β * t - γ * t ^ 2 ≤ 0

Far enough along, a quadratic that opens downward is not positive.

theorem ParallelPostulate.HyperbolicPlane.sq_add_sq_pos {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {v : K × K} (hv : v ≠ (0, 0)) : 0 < v.1 ^ 2 + v.2 ^ 2

def ParallelPostulate.HyperbolicPlane.plane {K : Type u_1} [Field K] [LinearOrder K] (κ : K) : Set (K × K)

The choice. The plane of the bound κ: the pairs (x, y) with 0 < 1 + κ (x² + y²).

Equations

• ParallelPostulate.HyperbolicPlane.plane κ = {p : K × K | 0 < 1 + κ * (p.1 ^ 2 + p.2 ^ 2)}

theorem ParallelPostulate.HyperbolicPlane.mem_plane {K : Type u_1} [Field K] [LinearOrder K] {κ : K} {p : K × K} : p ∈ plane κ ↔ 0 < 1 + κ * (p.1 ^ 2 + p.2 ^ 2)

theorem ParallelPostulate.HyperbolicPlane.plane_eq_univ {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {κ : K} (hκ : 0 ≤ κ) : plane κ = Set.univ

With the bound 0, or any bound that is not negative, every pair is a point. This is the plane of the three-dimensions section.

theorem ParallelPostulate.HyperbolicPlane.plane_zero {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] : plane 0 = Set.univ

theorem ParallelPostulate.HyperbolicPlane.zero_mem_plane {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (κ : K) : (0, 0) ∈ plane κ

The pair (0, 0) is a point, whatever the bound.

theorem ParallelPostulate.HyperbolicPlane.plane_mono {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {κ κ' : K} (h : κ ≤ κ') : plane κ ⊆ plane κ'

A smaller bound gives a smaller plane.

theorem ParallelPostulate.HyperbolicPlane.mem_plane_scale {K : Type u_1} [Field K] [LinearOrder K] (κ s : K) (p : K × K) : p ∈ plane (κ * s ^ 2) ↔ (s * p.1, s * p.2) ∈ plane κ

The bound κ s² is the bound κ with every pair made s times as large.

theorem ParallelPostulate.HyperbolicPlane.plane_open_forward {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (κ : K) (M : Pairs.Dim K) (hM : M.zero ∈ plane κ) : ∃ (t : K), 0 < t ∧ M.pt t ∈ plane κ

From a point of the plane, every dimension has a further number in the plane.

theorem ParallelPostulate.HyperbolicPlane.plane_openAlong {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (κ : K) : OpenAlong (plane κ)

The plane of a bound is open along the dimensions.

theorem ParallelPostulate.HyperbolicPlane.plane_beyond {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {κ : K} (hκ : κ < 0) (L : Pairs.Dim K) (hL : L.zero ≠ L.one) : ∃ (T : K), ∀ (t : K), T ≤ t → L.pt t ∉ plane κ

Under a negative bound every dimension leaves the plane. From some number on, none of its numbers is a point.

theorem ParallelPostulate.HyperbolicPlane.plane_beyond_infinite {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {κ : K} (hκ : κ < 0) (L : Pairs.Dim K) (hL : L.zero ≠ L.one) : {t : K | L.pt t ∉ plane κ}.Infinite

theorem ParallelPostulate.HyperbolicPlane.plane_stretch {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {κ : K} (hκ : κ < 0) (L : Pairs.Dim K) (hL : L.zero ≠ L.one) : ∃ (T : K), ∀ (t : K), L.pt t ∈ plane κ → -T < t ∧ t < T

Under a negative bound a dimension has a bounded stretch of its numbers in the plane.

theorem ParallelPostulate.HyperbolicPlane.plane_convex {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (κ : K) {A B : K × K} (hA : A ∈ plane κ) (hB : B ∈ plane κ) {u : K} (h0 : 0 ≤ u) (h1 : u ≤ 1) : { zero := A, one := B }.pt u ∈ plane κ

The plane of a bound is in one piece along every dimension. Between two points of the plane, every number of the dimension from the one to the other is a point of the plane.

Points and lines

theorem ParallelPostulate.HyperbolicPlane.exists_three_points {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (κ : K) : ∃ (A : K × K) (B : K × K) (C : K × K), A ∈ plane κ ∧ B ∈ plane κ ∧ C ∈ plane κ ∧ ∀ (S : Set (K × K)), IsLine (plane κ) S → ¬(A ∈ S ∧ B ∈ S ∧ C ∈ S)

There are three points of the plane that are not on one line.

theorem ParallelPostulate.HyperbolicPlane.plane_exists_line_and_point {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (κ : K) : ∃ (S : Set (K × K)) (P : K × K), IsLine (plane κ) S ∧ P ∈ plane κ ∧ P ∉ S

The plane of a bound has a line and a point that is not on it.

def ParallelPostulate.HyperbolicPlane.Between {K : Type u_1} [Field K] [LinearOrder K] (A B C : K × K) : Prop

B is between A and C: the two are different, and B is at a number between 0 and 1 of the dimension from A to C.

Equations

• ParallelPostulate.HyperbolicPlane.Between A B C = (A ≠ C ∧ ∃ (u : K), 0 < u ∧ u < 1 ∧ { zero := A, one := C }.pt u = B)

theorem ParallelPostulate.HyperbolicPlane.Between.symm {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {A B C : K × K} (h : Between A B C) : Between C B A

If B is between A and C, it is between C and A.

theorem ParallelPostulate.HyperbolicPlane.Between.mem {K : Type u_1} [Field K] [LinearOrder K] {A B C : K × K} (h : Between A B C) : B ∈ { zero := A, one := C }.points

A pair between A and C is a pair of the dimension from A to C.

theorem ParallelPostulate.HyperbolicPlane.Between.ne {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {A B C : K × K} (h : Between A B C) : A ≠ B ∧ B ≠ C ∧ A ≠ C

If B is between A and C, the three are different.

theorem ParallelPostulate.HyperbolicPlane.Between.not_left {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {A B C : K × K} (h : Between A B C) : ¬Between B A C

Of three pairs of a dimension, one only is between the other two. If B is between A and C, then A is not between B and C.

theorem ParallelPostulate.HyperbolicPlane.Between.not_right {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {A B C : K × K} (h : Between A B C) : ¬Between A C B

And C is not between A and B.

theorem ParallelPostulate.HyperbolicPlane.exists_beyond {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (κ : K) {A C : K × K} (hAC : A ≠ C) (hC : C ∈ plane κ) : ∃ B ∈ plane κ, Between A C B

A line can be produced. Beyond a point C of the plane, as seen from another pair A, there is a point of the plane.

theorem ParallelPostulate.HyperbolicPlane.crosses {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (κ : K) (M : Pairs.Dim K) (hM : M.zero ≠ M.one) {P Q : K × K} (hP : P ∈ plane κ) (hQ : Q ∈ plane κ) (h : M.side P * M.side Q < 0) : ∃ Y ∈ M.points, Y ∈ plane κ ∧ Between P Y Q

Two points of the plane on opposite sides of a dimension: between them the dimension has a point of the plane.

theorem ParallelPostulate.HyperbolicPlane.pasch {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (κ : K) {A B C : K × K} (hA : A ∈ plane κ) (hB : B ∈ plane κ) (hC : C ∈ plane κ) (M : Pairs.Dim K) (hM : M.zero ≠ M.one) (hAM : A ∉ M.points) (hBM : B ∉ M.points) (hCM : C ∉ M.points) {X : K × K} (hX : X ∈ M.points) (hAXB : Between A X B) : ∃ Y ∈ M.points, Y ∈ plane κ ∧ (Between A Y C ∨ Between B Y C)

Pasch's axiom. Let A, B and C be points of the plane, and let a dimension pass through none of them. If it has a pair between A and B, it has a point of the plane between A and C, or between B and C.

The parallels

theorem ParallelPostulate.HyperbolicPlane.hyperbolic_parallels {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {κ : K} (hκ : κ < 0) {S : Set (K × K)} (hS : IsLine (plane κ) S) {P : K × K} (hP : P ∈ plane κ) (hPS : P ∉ S) : {M : Set (K × K) | IsLine (plane κ) M ∧ P ∈ M ∧ M ∩ S = ∅}.Infinite

Under a negative bound, through a point that is not on a line there are infinitely many lines that do not meet the line.

theorem ParallelPostulate.HyperbolicPlane.hyperbolic_two_parallels {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {κ : K} (hκ : κ < 0) {S : Set (K × K)} (hS : IsLine (plane κ) S) {P : K × K} (hP : P ∈ plane κ) (hPS : P ∉ S) : ∃ (M₁ : Set (K × K)) (M₂ : Set (K × K)), M₁ ≠ M₂ ∧ (IsLine (plane κ) M₁ ∧ P ∈ M₁ ∧ M₁ ∩ S = ∅) ∧ IsLine (plane κ) M₂ ∧ P ∈ M₂ ∧ M₂ ∩ S = ∅

Under a negative bound, through a point that is not on a line there are two different lines that do not meet the line.

theorem ParallelPostulate.HyperbolicPlane.hyperbolic_parallel_property {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {κ : K} (hκ : κ < 0) {S : Set (K × K)} (hS : IsLine (plane κ) S) {P : K × K} (hP : P ∈ plane κ) (hPS : P ∉ S) : (∃ (M₁ : Set (K × K)) (M₂ : Set (K × K)), M₁ ≠ M₂ ∧ (IsLine (plane κ) M₁ ∧ P ∈ M₁ ∧ M₁ ∩ S = ∅) ∧ IsLine (plane κ) M₂ ∧ P ∈ M₂ ∧ M₂ ∩ S = ∅) ∧ {M : Set (K × K) | IsLine (plane κ) M ∧ P ∈ M ∧ M ∩ S = ∅}.Infinite

The parallels under a negative bound. Under a negative bound, through a given point that is not on a line there are at least two different lines, and in fact infinitely many, that do not meet the given line.

theorem ParallelPostulate.HyperbolicPlane.euclid_one_parallel {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {κ : K} (hκ : 0 ≤ κ) {S : Set (K × K)} (hS : IsLine (plane κ) S) {P : K × K} (hPS : P ∉ S) : ∃! M : Set (K × K), IsLine (plane κ) M ∧ P ∈ M ∧ M ∩ S = ∅

With the bound 0, or any bound that is not negative, the plane is that of the three-dimensions section: through a point that is not on a line there is one line that does not meet the line, and only one.

theorem ParallelPostulate.HyperbolicPlane.fifth_postulate_of_nonneg_bound {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {κ : K} (hκ : 0 ≤ κ) (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 ∧ F.b.pt t ∈ plane κ ∧ 0 < F.a.side (F.b.pt t)

Theorem E4 (the three-dimensions section) holds in the plane of a bound that is not negative. In a figure, let b1 and c1 lie on the left of a, and let the cross product of the directions of b and c be positive. Then b and c meet at a point of the plane, on the left of a.

theorem ParallelPostulate.HyperbolicPlane.one_parallel_iff_bound {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {κ : K} {S : Set (K × K)} (hS : IsLine (plane κ) S) {P : K × K} (hP : P ∈ plane κ) (hPS : P ∉ S) : (∃! M : Set (K × K), IsLine (plane κ) M ∧ P ∈ M ∧ M ∩ S = ∅) ↔ 0 ≤ κ

One parallel exactly when the bound is not negative.

Three points on a line, and the numbers of a dimension

theorem ParallelPostulate.HyperbolicPlane.between_trichotomy {A B C : ℝ × ℝ} (hAB : A ≠ B) (hBC : B ≠ C) (hAC : A ≠ C) (hB : B ∈ { zero := A, one := C }.points) : Between A B C ∨ Between B A C ∨ Between A C B

Of three different points on a line, one is between the two others.

theorem ParallelPostulate.HyperbolicPlane.ne_of_side_ne_zero {X Y Z : ℝ × ℝ} (h : { zero := X, one := Y }.side Z ≠ 0) : X ≠ Y ∧ Z ≠ X ∧ Z ≠ Y

A pair of the plane off a line has a side that is not 0, and the three points that make the side not 0 are different.

theorem ParallelPostulate.HyperbolicPlane.IsLine.subset_plane {κ : ℝ} {S : Set (ℝ × ℝ)} (hS : IsLine (plane κ) S) : S ⊆ plane κ

A line of the plane is a set of points of the plane.

theorem ParallelPostulate.HyperbolicPlane.IsLine.eq_through {κ : ℝ} {S : Set (ℝ × ℝ)} (hS : IsLine (plane κ) S) {D F : ℝ × ℝ} (hD : D ∈ S) (hF : F ∈ S) (hDF : D ≠ F) : S = { zero := D, one := F }.points ∩ plane κ

A line of the plane through two different points of it is what the dimension through them has in the plane.

def ParallelPostulate.HyperbolicPlane.StrictBetween (a c b : ℝ) : Prop

c is strictly between a and b, on either side.

Equations

• ParallelPostulate.HyperbolicPlane.StrictBetween a c b = (a < c ∧ c < b ∨ b < c ∧ c < a)

theorem ParallelPostulate.HyperbolicPlane.between_pt_of_strictBetween (M : Pairs.Dim ℝ) (hM : M.zero ≠ M.one) {a b c : ℝ} (h : StrictBetween a c b) : Between (M.pt a) (M.pt c) (M.pt b)

Numbers in order give pairs in order.

theorem ParallelPostulate.HyperbolicPlane.strictBetween_of_between_pt (M : Pairs.Dim ℝ) (hM : M.zero ≠ M.one) {a b c : ℝ} (h : Between (M.pt a) (M.pt c) (M.pt b)) : StrictBetween a c b

Pairs in order come from numbers in order.

theorem ParallelPostulate.HyperbolicPlane.pt_mem_plane_of_le {κ : ℝ} (M : Pairs.Dim ℝ) {a b c : ℝ} (ha : M.pt a ∈ plane κ) (hb : M.pt b ∈ plane κ) (hac : a ≤ c) (hcb : c ≤ b) : M.pt c ∈ plane κ

The numbers of a dimension whose pairs are points of the plane make an interval.