Lin McMullin's theorem: inflection points of a quartic and the golden ratio

Let p be a real quartic whose second derivative vanishes at a ≠ b (its two inflection points). The line through (a, p a) and (b, p b) meets the graph exactly at a, b, φa − b/φ and φb − a/φ, φ the golden ratio. If a < b these are ordered φa − b/φ < a < b < φb − a/φ, and b − a = φ (a − (φa − b/φ)) = φ ((φb − a/φ) − b). Proof: p'' = 12c (X − a)(X − b), so p = c (X⁴ − 2(a + b)X³ + 6ab X²) + dX + e, and p − line = c (X − a)(X − b)(X² − (a + b)X + a² + b² − 3ab), whose quadratic factor has roots φa − b/φ, φb − a/φ because φ² = φ + 1.

Main results

• McMullin.line_inter_iff: the line through the inflection points meets the quartic exactly at a, b, φa − b/φ, φb − a/φ
• McMullin.order: if a < b: φa − b/φ < a < b < φb − a/φ
• McMullin.golden_ratio_gaps: b − a = φ (a − P) = φ (Q − b)

References

• R. Whitty, Theorem of the Day, «Lin McMullin's Theorem» (Analysis/McMullin).
• L. McMullin (2004); A. Bogomolny, cut-the-knot, «Fourth Degree Polynomials and the Golden Ratio».

theorem McMullin.div_golden (y : ℝ) : y / Real.goldenRatio = y * (Real.goldenRatio - 1)

y / φ = y (φ − 1).

theorem McMullin.line_inter_iff (p : Polynomial ℝ) (hp : p.natDegree = 4) (a b : ℝ) (hab : a ≠ b) (ha : Polynomial.eval a (Polynomial.derivative (Polynomial.derivative p)) = 0) (hb : Polynomial.eval b (Polynomial.derivative (Polynomial.derivative p)) = 0) (x : ℝ) : Polynomial.eval x p = Polynomial.eval a p + (Polynomial.eval b p - Polynomial.eval a p) / (b - a) * (x - a) ↔ x = a ∨ x = b ∨ x = Real.goldenRatio * a - b / Real.goldenRatio ∨ x = Real.goldenRatio * b - a / Real.goldenRatio

Lin McMullin's theorem. Let p be a real polynomial of degree 4 whose second derivative vanishes at two distinct points a ≠ b (the two inflection points A, B). The line through (a, p a) and (b, p b) meets the graph exactly at the abscissae a, b, φa - b/φ and φb - a/φ (φ the golden ratio).

theorem McMullin.order (a b : ℝ) (hab : a < b) : Real.goldenRatio * a - b / Real.goldenRatio < a ∧ a < b ∧ b < Real.goldenRatio * b - a / Real.goldenRatio

If a < b: φa − b/φ < a < b < φb − a/φ.

theorem McMullin.golden_ratio_gaps (a b : ℝ) : b - a = Real.goldenRatio * (a - (Real.goldenRatio * a - b / Real.goldenRatio)) ∧ b - a = Real.goldenRatio * (Real.goldenRatio * b - a / Real.goldenRatio - b)

The gaps are in the golden ratio: b − a = φ (a − P) = φ (Q − b).