Halley’s cubic square-root step

Paper

Methodus Nova Accurata et Facilis Inveniendi Radices AEquationum Quarumcumque Generaliter, Sine Praevia Reductione, 1694. Philosophical Transactions 18, pp. 136–148. Read Gander’s derivation of the rational formula.

The result

Specializing Halley’s rational method to a positive square root gives an exact cubic error identity. For a positive starting value, the ratio (x − r)/(x + r) is cubed at every iteration.

H(x) = x(x² + 3r²)/(3x² + r²) H(x) − r = (x − r)³/(3x² + r²) q(xₙ) = q(x₀)^(3ⁿ), q(x) = (x − r)/(x + r)

Scope & assumptions

8 checked theorems. Denominator positivity, positive iterates, exact cubic error, an upper bracket, a cubic error bound, and the cubed ratio at every step. No general differentiable-function convergence theorem or limit proof.

Exact real arithmetic and r > 0. The ratio identity assumes x₀ > 0. The bracket and bound assume x ≥ r and give r ≤ H(x) ≤ x and H(x) − r ≤ (x − r)³/(4r²).

Prior work

No matching named formalization was located in the bounded search of two Mathlib revisions and indexed web results on 2026-09-10. Related library ingredients already exist. First-formalization status is unconfirmed; this does not establish priority.

Lean proof

Lean + Mathlib 4.33.1 · 8 checked theorems

import Mathlib.Data.Real.Basic
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Ring
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Positivity

/-! Halley (1694), square-root specialization of the rational iteration.
Exact arithmetic, positive target root. Cubic error identities are proved;
the general smooth-function convergence theorem is outside this file. -/
namespace PaperToLean.Halley
noncomputable section
def step (a x : ℝ) : ℝ := x * (x ^ 2 + 3 * a) / (3 * x ^ 2 + a)
def ratio (r x : ℝ) : ℝ := (x - r) / (x + r)
def iterate (a x : ℝ) : ℕ → ℝ
  | 0 => x
  | n + 1 => step a (iterate a x n)

theorem denominator_pos (r x : ℝ) (hr : 0 < r) : 0 < 3 * x ^ 2 + r ^ 2 := by
  positivity

theorem positive_step (r x : ℝ) (hr : 0 < r) (hx : 0 < x) : 0 < step (r ^ 2) x := by
  unfold step
  positivity

theorem cubic_error (r x : ℝ) (hr : 0 < r) :
    step (r ^ 2) x - r = (x - r) ^ 3 / (3 * x ^ 2 + r ^ 2) := by
  have hd := ne_of_gt (denominator_pos r x hr)
  unfold step
  field_simp
  ring

theorem bracket (r x : ℝ) (hr : 0 < r) (hx : r ≤ x) :
    r ≤ step (r ^ 2) x ∧ step (r ^ 2) x ≤ x := by
  have hd := denominator_pos r x hr
  constructor
  · have he := cubic_error r x hr
    have hp : 0 ≤ (x - r) ^ 3 / (3 * x ^ 2 + r ^ 2) := by positivity
    linarith
  · unfold step
    apply (div_le_iff₀ hd).mpr
    have hx0 : 0 ≤ x := le_trans (le_of_lt hr) hx
    nlinarith [mul_nonneg hx0 (show 0 ≤ x ^ 2 - r ^ 2 by nlinarith)]

theorem cubic_bound (r x : ℝ) (hr : 0 < r) (hx : r ≤ x) :
    step (r ^ 2) x - r ≤ (x - r) ^ 3 / (4 * r ^ 2) := by
  rw [cubic_error r x hr]
  apply div_le_div_of_nonneg_left (by positivity) (by positivity)
  nlinarith

theorem ratio_cubed (r x : ℝ) (hr : 0 < r) (hx : 0 < x) :
    ratio r (step (r ^ 2) x) = (ratio r x) ^ 3 := by
  have hd := ne_of_gt (denominator_pos r x hr)
  have hs : x + r ≠ 0 := ne_of_gt (add_pos hx hr)
  have hc : x ^ 3 + 3 * x ^ 2 * r + 3 * x * r ^ 2 + r ^ 3 ≠ 0 := by positivity
  unfold ratio step
  field_simp
  ring

theorem iterate_positive (r x : ℝ) (hr : 0 < r) (hx : 0 < x) (n : ℕ) :
    0 < iterate (r ^ 2) x n := by
  induction n with
  | zero => exact hx
  | succ n ih => exact positive_step r _ hr ih

theorem ratio_at_every_step (r x : ℝ) (hr : 0 < r) (hx : 0 < x) (n : ℕ) :
    ratio r (iterate (r ^ 2) x n) = (ratio r x) ^ (3 ^ n) := by
  induction n with
  | zero => simp [iterate]
  | succ n ih =>
    rw [iterate, ratio_cubed r _ hr (iterate_positive r x hr hx n), ih,
      ← pow_mul, pow_succ]

#print axioms denominator_pos
#print axioms positive_step
#print axioms cubic_error
#print axioms bracket
#print axioms cubic_bound
#print axioms ratio_cubed
#print axioms iterate_positive
#print axioms ratio_at_every_step
end
end PaperToLean.Halley

Lean 4.33.1
Dependencies: Mathlib 4.33.1 (see bundled lake-manifest.json)
File: Halley.lean
SHA-256: c51faf612bca380035e0049661ec13da9bf3ced2d8f0371678c78c7456e3dfcc
Result: passed

'PaperToLean.Halley.denominator_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Halley.positive_step' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Halley.cubic_error' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Halley.bracket' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Halley.cubic_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Halley.ratio_cubed' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Halley.iterate_positive' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Halley.ratio_at_every_step' depends on axioms: [propext, Classical.choice, Quot.sound]

Run it

Install Lean with elan and Git. Download the project ZIP, extract it, and run these commands in that folder. The first command downloads the pinned Mathlib dependencies.

python3 prepare.py
lake env lean -DwarningAsError=true Halley.lean

A successful check prints the axiom dependencies and exits without errors.