structure ProjectivePascal.Conic (k : Type u_1) [Field k] : Type u_1

A projective conic on P^2: a function on k^3 that is homogeneous of degree 2.

• eval : (Fin 3 → k) → k
• homog (c : k) (v : Fin 3 → k) : self.eval (c • v) = c ^ 2 * self.eval v

structure ProjectivePascal.Line (k : Type u_1) [Field k] : Type u_1

A projective line on P^2: a k-linear function k^3 → k.

• eval : (Fin 3 → k) → k
• map_add (v w : Fin 3 → k) : self.eval (v + w) = self.eval v + self.eval w
• map_smul (c : k) (v : Fin 3 → k) : self.eval (c • v) = c * self.eval v

def ProjectivePascal.Conic.IsIrreducible {k : Type u_1} [Field k] (Q : Conic k) : Prop

A conic is irreducible if its defining function is not a product of two linear forms (i.e. it is not the union of two projective lines).

def ProjectivePascal.OnConic {k : Type u_1} [Field k] (Q : Conic k) (P : Fin 3 → k) : Prop

The point P (in k^3) lies on the conic Q if Q vanishes on P.

def ProjectivePascal.Line.ThroughPair {k : Type u_1} [Field k] (L : Line k) (P₁ P₂ : Fin 3 → k) : Prop

A line passes through a pair of points P_1, P_2 if it vanishes on both and is not identically zero.

def ProjectivePascal.IsIntersectionOf {k : Type u_1} [Field k] (R : Fin 3 → k) (L₁ L₂ : Line k) : Prop

The point R is an intersection of two lines L_1 and L_2 if it lies on both and is a nonzero vector.

def ProjectivePascal.AreCollinear {k : Type u_1} [Field k] (R₁ R₂ R₃ : Fin 3 → k) : Prop

Three points are collinear if there exists a nonzero line passing through all three.

def ProjectivePascal.PairwiseProjectivelyDistinct {k : Type u_1} [Field k] (P : Fin 6 → Fin 3 → k) : Prop

Six points (as vectors in k^3) are pairwise projectively distinct if no two represent the same point of projective space.

def ProjectivePascal.AllNonzero {k : Type u_1} [Field k] (P : Fin 6 → Fin 3 → k) : Prop

All six points are nonzero vectors (so represent honest projective points).

def ProjectivePascal.AllOnConic {k : Type u_1} [Field k] (Q : Conic k) (P : Fin 6 → Fin 3 → k) : Prop

All six points lie on the conic Q.

theorem ProjectivePascal.bezout_pascal_configuration {k : Type u_1} [Field k] (Q : Conic k) (hQ : Q.IsIrreducible) (Pts : Fin 6 → Fin 3 → k) (hPts_nonzero : AllNonzero Pts) (hPts_distinct : PairwiseProjectivelyDistinct Pts) (hPts_on_conic : AllOnConic Q Pts) (A B C A' B' C' : Line k) (hA : A.ThroughPair (Pts 0) (Pts 1)) (hB : B.ThroughPair (Pts 2) (Pts 3)) (hC : C.ThroughPair (Pts 4) (Pts 5)) (hA' : A'.ThroughPair (Pts 3) (Pts 4)) (hB' : B'.ThroughPair (Pts 5) (Pts 0)) (hC' : C'.ThroughPair (Pts 1) (Pts 2)) (R₁ R₂ R₃ : Fin 3 → k) (hR₁ : IsIntersectionOf R₁ A A') (hR₂ : IsIntersectionOf R₂ C' C) (hR₃ : IsIntersectionOf R₃ B B') : ∃ (t : k) (L : Line k), L.eval ≠ 0 ∧ (∀ (v : Fin 3 → k), A.eval v * B.eval v * C.eval v - t * (A'.eval v * B'.eval v * C'.eval v) = Q.eval v * L.eval v) ∧ Q.eval R₁ ≠ 0 ∧ Q.eval R₂ ≠ 0 ∧ Q.eval R₃ ≠ 0

Bezout-style configuration lemma for the projective Pascal theorem: for six points on an irreducible conic Q with the triangle of opposite sides configuration, there is a scalar t and a linear form L such that the cubic ABC - t(A'B'C') equals QL.

theorem ProjectivePascal.pascal_theorem_projective {k : Type u_1} [Field k] (Q : Conic k) (hQ_irred : Q.IsIrreducible) (P : Fin 6 → Fin 3 → k) (hP_nonzero : AllNonzero P) (hP_distinct : PairwiseProjectivelyDistinct P) (hP_on_conic : AllOnConic Q P) (L₁₂ L₂₃ L₃₄ L₄₅ L₅₆ L₆₁ : Line k) (hL₁₂ : L₁₂.ThroughPair (P 0) (P 1)) (hL₂₃ : L₂₃.ThroughPair (P 1) (P 2)) (hL₃₄ : L₃₄.ThroughPair (P 2) (P 3)) (hL₄₅ : L₄₅.ThroughPair (P 3) (P 4)) (hL₅₆ : L₅₆.ThroughPair (P 4) (P 5)) (hL₆₁ : L₆₁.ThroughPair (P 5) (P 0)) (R₁ R₂ R₃ : Fin 3 → k) (hR₁ : IsIntersectionOf R₁ L₁₂ L₄₅) (hR₂ : IsIntersectionOf R₂ L₂₃ L₅₆) (hR₃ : IsIntersectionOf R₃ L₃₄ L₆₁) : AreCollinear R₁ R₂ R₃

Pascal's theorem (projective form, Theorem 5.3, Lecture 5): for a hexagon inscribed in an irreducible conic, the three pairs of opposite sides meet in three collinear points.

theorem PascalTheoremConics.natDegree_triple_linear_le {R : Type u_1} [CommRing R] {p₁ p₂ p₃ : Polynomial R} (h₁ : p₁.natDegree ≤ 1) (h₂ : p₂.natDegree ≤ 1) (h₃ : p₃.natDegree ≤ 1) : (p₁ * p₂ * p₃).natDegree ≤ 3

A product of three polynomials of degree ≤ 1 has degree ≤ 3.

theorem PascalTheoremConics.eval_cubic_vanish {k : Type u_1} [Field k] (p r s q u v : Polynomial k) (t x : k) (hp : Polynomial.eval x p = 0) (hq : Polynomial.eval x q = 0) : Polynomial.eval x (p * r * s - Polynomial.C t * (q * u * v)) = 0

If two factors of the cubic both vanish at x, then the cubic prs - t*(quv) vanishes at x.

theorem PascalTheoremConics.eval_factor_vanish {k : Type u_1} [Field k] (Q L : Polynomial k) (x : k) (hP : Polynomial.eval x (Q * L) = 0) (hQ : Polynomial.eval x Q ≠ 0) : Polynomial.eval x L = 0

If the product Q*L vanishes at x and Q does not, then L vanishes at x.

theorem PascalTheoremConics.monic_dvd_eq_mul_divByMonic {k : Type u_1} [Field k] (f g : Polynomial k) (hg : g.Monic) (h : g ∣ f) : f = g * (f /ₘ g)

For a monic divisor g of f, we have f = g * (f /ₘ g).

structure PascalTheoremConics.ProjectiveConic (k : Type u_1) [Field k] : Type u_1

A projective conic given by an irreducible monic polynomial of degree 2.

• poly : Polynomial k
• irred : Irreducible self.poly
• monic : self.poly.Monic
• deg : self.poly.natDegree = 2

structure PascalTheoremConics.InscribedHexagon (k : Type u_1) [Field k] (conic : ProjectiveConic k) : Type u_1

An inscribed hexagon in a conic: three "sides" and three "opposite sides", each a polynomial of degree ≤ 1, together with a scalar t making the cubic difference non-coprime to the conic.

• sideA : Polynomial k
• sideB : Polynomial k
• sideC : Polynomial k
• oppA : Polynomial k
• oppB : Polynomial k
• oppC : Polynomial k
• sideA_deg : self.sideA.natDegree ≤ 1
• sideB_deg : self.sideB.natDegree ≤ 1
• sideC_deg : self.sideC.natDegree ≤ 1
• oppA_deg : self.oppA.natDegree ≤ 1
• oppB_deg : self.oppB.natDegree ≤ 1
• oppC_deg : self.oppC.natDegree ≤ 1
• t : k
• not_coprime : ¬IsCoprime conic.poly (self.sideA * self.sideB * self.sideC - Polynomial.C self.t * (self.oppA * self.oppB * self.oppC))

noncomputable def PascalTheoremConics.InscribedHexagon.cubicP {k : Type u_1} [Field k] {conic : ProjectiveConic k} (hex : InscribedHexagon k conic) : Polynomial k

The cubic associated to an inscribed hexagon: side_A·side_B·side_C - t·opp_A·opp_B·opp_C.

theorem PascalTheoremConics.InscribedHexagon.cubicP_deg_le {k : Type u_1} [Field k] {conic : ProjectiveConic k} (hex : InscribedHexagon k conic) : hex.cubicP.natDegree ≤ 3

The hexagon cubic has degree at most 3.

theorem PascalTheoremConics.pascal_divisibility {k : Type u_1} [Field k] {conic : ProjectiveConic k} (hex : InscribedHexagon k conic) : conic.poly ∣ hex.cubicP

The conic divides the hexagon cubic, by the irreducibility / non-coprimality condition in InscribedHexagon.

noncomputable def PascalTheoremConics.InscribedHexagon.pascalLine {k : Type u_1} [Field k] {conic : ProjectiveConic k} (hex : InscribedHexagon k conic) : Polynomial k

The Pascal line of a hexagon: the quotient of the hexagon cubic by the conic.

theorem PascalTheoremConics.pascal_quotient_is_line {k : Type u_1} [Field k] {conic : ProjectiveConic k} (hex : InscribedHexagon k conic) : hex.pascalLine.natDegree ≤ 1

The Pascal line has degree ≤ 1, confirming it is indeed a (projective) line.

theorem PascalTheoremConics.pascal_factorization {k : Type u_1} [Field k] {conic : ProjectiveConic k} (hex : InscribedHexagon k conic) : hex.cubicP = conic.poly * hex.pascalLine

Factorization: the hexagon cubic equals the conic times the Pascal line.

theorem PascalTheoremConics.point_on_line_of_on_cubic_not_on_conic {k : Type u_1} [Field k] {conic : ProjectiveConic k} (hex : InscribedHexagon k conic) (x : k) (hP : Polynomial.eval x hex.cubicP = 0) (hQ : Polynomial.eval x conic.poly ≠ 0) : Polynomial.eval x hex.pascalLine = 0

If a point lies on the hexagon cubic but not on the conic, then it lies on the Pascal line.

theorem PascalTheoremConics.pascal_collinear_A {k : Type u_1} [Field k] {conic : ProjectiveConic k} (hex : InscribedHexagon k conic) (x : k) (h_sideA : Polynomial.eval x hex.sideA = 0) (h_oppA : Polynomial.eval x hex.oppA = 0) (h_not_on_conic : Polynomial.eval x conic.poly ≠ 0) : Polynomial.eval x hex.pascalLine = 0

The intersection point of side A and its opposite lies on the Pascal line.

theorem PascalTheoremConics.pascal_collinear_B {k : Type u_1} [Field k] {conic : ProjectiveConic k} (hex : InscribedHexagon k conic) (x : k) (h_sideB : Polynomial.eval x hex.sideB = 0) (h_oppB : Polynomial.eval x hex.oppB = 0) (h_not_on_conic : Polynomial.eval x conic.poly ≠ 0) : Polynomial.eval x hex.pascalLine = 0

The intersection point of side B and its opposite lies on the Pascal line.

theorem PascalTheoremConics.pascal_collinear_C {k : Type u_1} [Field k] {conic : ProjectiveConic k} (hex : InscribedHexagon k conic) (x : k) (h_sideC : Polynomial.eval x hex.sideC = 0) (h_oppC : Polynomial.eval x hex.oppC = 0) (h_not_on_conic : Polynomial.eval x conic.poly ≠ 0) : Polynomial.eval x hex.pascalLine = 0

The intersection point of side C and its opposite lies on the Pascal line.

theorem PascalTheoremConics.pascal_theorem_conics {k : Type u_1} [Field k] {conic : ProjectiveConic k} (hex : InscribedHexagon k conic) (xA xB xC : k) (hA_side : Polynomial.eval xA hex.sideA = 0) (hA_opp : Polynomial.eval xA hex.oppA = 0) (hB_side : Polynomial.eval xB hex.sideB = 0) (hB_opp : Polynomial.eval xB hex.oppB = 0) (hC_side : Polynomial.eval xC hex.sideC = 0) (hC_opp : Polynomial.eval xC hex.oppC = 0) (hA_conic : Polynomial.eval xA conic.poly ≠ 0) (hB_conic : Polynomial.eval xB conic.poly ≠ 0) (hC_conic : Polynomial.eval xC conic.poly ≠ 0) : Polynomial.eval xA hex.pascalLine = 0 ∧ Polynomial.eval xB hex.pascalLine = 0 ∧ Polynomial.eval xC hex.pascalLine = 0 ∧ hex.pascalLine.natDegree ≤ 1

Pascal's theorem for conics in the curve formulation: the three opposite-side intersection points x_A, x_B, x_C all lie on the Pascal line, which is a line of degree ≤ 1.