Pascal's and Pappus's hexagon theorems

TheoremPascal's theorem in an affine plane#✓fully proved

Let \(k\) be a field of characteristic different from \(2\) and let \(P\) be an affine plane over \(k\), that is, an affine space whose space of translations \(V\) is a \(k\)-vector space of dimension \(2\). Fix a point \(O \in P\) and a nondegenerate symmetric bilinear form \(\beta\) on \(V \times k\), and call the set of points \(x \in P\) with \(\beta((x - O, 1), (x - O, 1)) = 0\) the conic. Let \(v_0, v_1, \dots, v_5\) be six distinct points of the conic such that, for each of the three pairs of opposite sides \((v_0 v_1, v_3 v_4)\), \((v_1 v_2, v_4 v_5)\) and \((v_2 v_3, v_5 v_0)\) of the hexagon \(v_0 v_1 v_2 v_3 v_4 v_5\), the four endpoints are not collinear, so that the two lines are distinct. If \(q_1\) lies on the lines \(v_0 v_1\) and \(v_3 v_4\), \(q_2\) lies on the lines \(v_1 v_2\) and \(v_4 v_5\), and \(q_3\) lies on the lines \(v_2 v_3\) and \(v_5 v_0\), then \(q_1\), \(q_2\), \(q_3\) are collinear.

MetaMathlibExt.pascal_theorem · 15 lines

theorem pascal_theorem {k V P : Type*} [Field k] [AddCommGroup V]
    [Module k V] [AddTorsor V P] [FiniteDimensional k V]
    (hDim : Module.finrank k V = 2) (hChar : (2 : k) ≠ 0) (O : P) (v : Fin 6 → P)
    (B3 : LinearMap.BilinForm k (V × k))
    (hB3_symm : B3.IsSymm) (hB3_nondeg : B3.Nondegenerate)
    (q₁ q₂ q₃ : P)
    (hConic : ∀ i, B3 ((v i -ᵥ O), 1) ((v i -ᵥ O), 1) = 0)
    (hInj : Function.Injective v)
    (hLine₁ : ¬ Collinear k {v 0, v 1, v 3, v 4})
    (hLine₂ : ¬ Collinear k {v 1, v 2, v 4, v 5})
    (hLine₃ : ¬ Collinear k {v 2, v 3, v 5, v 0})
    (hMeet₁ : Collinear k {v 0, v 1, q₁} ∧ Collinear k {v 3, v 4, q₁})
    (hMeet₂ : Collinear k {v 1, v 2, q₂} ∧ Collinear k {v 4, v 5, q₂})
    (hMeet₃ : Collinear k {v 2, v 3, q₃} ∧ Collinear k {v 5, v 0, q₃}) :
    Collinear k {q₁, q₂, q₃}

Sources

• https://en.wikipedia.org/wiki/Pascal%27s_theorem.

DefinitionSame projective point#✓fully proved

Two vectors \(v, w \in \mathbb{R}^3\) represent the same point of the real projective plane when \(w = c v\) for some real number \(c \ne 0\).

def SamePoint (v w : Fin 3 → ℝ) : Prop := ∃ c : ℝ, c ≠ 0 ∧ w = c • v

Used by 1

Used byPascal's theorem for real projective conics

DefinitionPoints on a conic#✓fully proved

For a real \(3 \times 3\) matrix \(M\), a vector \(v \in \mathbb{R}^3\) lies on the conic \(x^\top M x = 0\) when \(v^\top M v = 0\).

def OnConic (M : Matrix (Fin 3) (Fin 3) ℝ) (v : Fin 3 → ℝ) : Prop :=
  v ⬝ᵥ (M *ᵥ v) = 0

Used by 1

Used byPascal's theorem for real projective conics

DefinitionMeet of two lines#✓fully proved

Writing \(\times\) for the cross product on \(\mathbb{R}^3\), the meet of the line through \(a\) and \(b\) with the line through \(c\) and \(d\), for \(a, b, c, d \in \mathbb{R}^3\), is the vector \((a \times b) \times (c \times d)\).

When \(a \times b\) and \(c \times d\) are nonzero and not proportional, this vector represents the intersection point of the two projective lines.

def meet (a b c d : Fin 3 → ℝ) : Fin 3 → ℝ := (a ⨯₃ b) ⨯₃ (c ⨯₃ d)

Used by 1

Used byPascal's theorem for real projective conics

DefinitionCollinear projective points#✓fully proved

Writing \(\cdot\) and \(\times\) for the dot and cross products on \(\mathbb{R}^3\), three vectors \(p, q, r \in \mathbb{R}^3\) represent collinear points of the real projective plane when their triple product vanishes: \(p \cdot (q \times r) = 0\).

def Collinear3 (p q r : Fin 3 → ℝ) : Prop := p ⬝ᵥ (q ⨯₃ r) = 0

Used by 1

Used byPascal's theorem for real projective conics

TheoremPascal's theorem for real projective conics#●ready to prove

Let \(M\) be a real symmetric \(3 \times 3\) matrix with \(\det M \ne 0\), and let \(a_1, a_2, a_3, b_1, b_2, b_3 \in \mathbb{R}^3\) be nonzero vectors on the conic \(x^\top M x = 0\), no two of which represent the same projective point. Writing \(\cdot\) and \(\times\) for the dot and cross products on \(\mathbb{R}^3\), let \(p = (a_1 \times b_2) \times (a_2 \times b_1)\), \(q = (a_1 \times b_3) \times (a_3 \times b_1)\) and \(r = (a_2 \times b_3) \times (a_3 \times b_2)\) be the meets of the opposite sides of the hexagon \(a_1 b_2 a_3 b_1 a_2 b_3\). Then \(p\), \(q\) and \(r\) are collinear: \(p \cdot (q \times r) = 0\).

public theorem_wanted pascal
    (M : Matrix (Fin 3) (Fin 3) ℝ) (hMsymm : M.IsSymm) (hMdet : M.det ≠ 0)
    (a₁ a₂ a₃ b₁ b₂ b₃ : Fin 3 → ℝ)
    (ha₁ : a₁ ≠ 0) (ha₂ : a₂ ≠ 0) (ha₃ : a₃ ≠ 0)
    (hb₁ : b₁ ≠ 0) (hb₂ : b₂ ≠ 0) (hb₃ : b₃ ≠ 0)
    (hdist : [a₁, a₂, a₃, b₁, b₂, b₃].Pairwise (fun v w => ¬ SamePoint v w))
    (hA₁ : OnConic M a₁) (hA₂ : OnConic M a₂) (hA₃ : OnConic M a₃)
    (hB₁ : OnConic M b₁) (hB₂ : OnConic M b₂) (hB₃ : OnConic M b₃) :
    Collinear3 (meet a₁ b₂ a₂ b₁) (meet a₁ b₃ a₃ b₁) (meet a₂ b₃ a₃ b₂)

Sources

• B. Pascal, Essay pour les coniques (1640). Knill, Some fundamental theorems in mathematics, §146. Problem pascal of the lean-eval benchmark.

Uses 4

Statement usesCollinear projective points · Points on a conic · Same projective point · Meet of two lines

5 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.