Paper
Non-linear Transformations of Divergent and Slowly Convergent Sequences, 1955. Journal of Mathematics and Physics 34 (1955), pp. 1–42. Read the paper scan and transcription.
Connection to the paper
This is the k = 2 case of Shanks’s determinant transformation in equation (2) and the finite-transient exactness discussion in equations (17)–(23), near the end of the introduction. The implementation uses a window starting at n rather than Shanks’s centered index. Its 3 × 3 determinants have the same first-difference rows. The factorization lemmas make the singularity conditions explicit.
The result
If sₙ = L + a rⁿ + b qⁿ, with nonzero amplitudes and distinct ratios different from 0 and 1, Shanks’s second-order transformation recovers L from every five consecutive samples. Convergence of the input sequence is not required.
sₙ = L + a rⁿ + b qⁿ ⇒ T₂(sₙ, …, sₙ₊₄) = L D₀ = ab(r − 1)²(q − 1)²(r − q)²
Proof in plain English
- Build two determinants. The denominator has a top row of ones; the numerator uses the first three samples instead. Both share two rows of successive first differences.
- Factor exactly. For the two-mode model, the denominator is ab(r − 1)²(q − 1)²(r − q)². The numerator is L times that same expression.
- Cancel and shift. The assumptions make the factor nonzero, so the quotient is L. Shifting the window replaces a and b with arⁿ and bqⁿ, which proves exactness for the whole sequence.
Scope & assumptions
Six checked theorems over arbitrary fields: denominator and numerator factorizations, exact recovery from five samples, the window-shift identity, exactness at every natural-number index, and singularity for a single-mode input. The 3 × 3 determinant is implemented by its explicit six-term formula. Higher orders, repeated-root transients, Padé approximation, asymptotic convergence, and the paper’s separate rules for singular quotients are outside this artifact.
Both amplitudes are nonzero; the two ratios are distinct and neither is 1. For exactness at every sequence index, neither ratio is 0. The local five-sample theorem also allows zero ratios when its other conditions hold. No positivity or |r| < 1 assumption is needed: the same algebra applies to growing and oscillating modes. A single-mode sequence gives a zero denominator; this file does not implement the paper’s order-reduction rule for that case.
Notation in Lean
| Meaning | Lean |
|---|---|
| Expanded 3 × 3 determinant | det3 |
| Shanks’s equation (2), order two | numerator / denominator |
| All local degeneracies | denominator_factor |
| Exact recovery at every index | sequence_exact |
| Why lower-order input needs a separate rule | single_mode_singular |
Prior work
No matching formalization found in the bounded search on 2026-09-09. Searched the pinned and current Mathlib sources and publicly indexed proof-assistant results for the Shanks sequence transformation. Results about the unrelated Tonelli–Shanks algorithm were excluded. Priority remains unconfirmed; this is a new implementation here, not a certified first formalization.
Read the search recordLean proof
import Mathlib.Algebra.Field.Basic
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Ring
/-!
# Shanks's second-order sequence transformation
Daniel Shanks, Non-linear Transformations of Divergent and Slowly Convergent
Sequences, Journal of Mathematics and Physics 34 (1955), 1–42.
DOI: 10.1002/sapm19553411.
Scope: equation (2) at order k = 2 and the two-mode instance of the
finite-transient exactness argument in equations (17)–(23). We use a window
starting at n instead of Shanks's centered index. The determinants are
written explicitly, including all the difference rows. Additional lemmas
factor the denominator and establish exactness at every sequence index.
No claim about general-order transforms, floating-point stability, arbitrary
convergence, or Shanks's rules for singular quotients is made.
Lean / Mathlib 4.33.1. Run: lake env lean -DwarningAsError=true Shanks.lean
License: MIT. See the website's bounded prior-work search before claiming novelty.
-/
namespace PaperToLean.Shanks
variable {K : Type*} [Field K]
/-- The ordinary 3 by 3 determinant, expanded to six products. -/
def det3 (a b c d e f g h i : K) : K :=
a * (e * i - f * h) - b * (d * i - f * g) + c * (d * h - e * g)
/-- Bottom rows are successive first differences from a five-sample window. -/
def denominator (s0 s1 s2 s3 s4 : K) : K :=
det3 1 1 1 (s1 - s0) (s2 - s1) (s3 - s2)
(s2 - s1) (s3 - s2) (s4 - s3)
def numerator (s0 s1 s2 s3 s4 : K) : K :=
det3 s0 s1 s2 (s1 - s0) (s2 - s1) (s3 - s2)
(s2 - s1) (s3 - s2) (s4 - s3)
/-- Shanks's order-two determinant quotient, on nonsingular windows. -/
def transform (s0 s1 s2 s3 s4 : K) : K :=
numerator s0 s1 s2 s3 s4 / denominator s0 s1 s2 s3 s4
/-- Samples of a target plus two independent geometric error modes. -/
def sample (L a b r q : K) (n : Nat) : K := L + a * r ^ n + b * q ^ n
/-- Explicit factorization identifies all degeneracies in this window. -/
theorem denominator_factor (L a b r q : K) :
denominator (L + a + b) (L + a*r + b*q) (L + a*r^2 + b*q^2)
(L + a*r^3 + b*q^3) (L + a*r^4 + b*q^4) =
a * b * (r - 1)^2 * (q - 1)^2 * (r - q)^2 := by
unfold denominator det3
ring
/-- Cancellation in the numerator is an identity, before any division. -/
theorem numerator_factor (L a b r q : K) :
numerator (L + a + b) (L + a*r + b*q) (L + a*r^2 + b*q^2)
(L + a*r^3 + b*q^3) (L + a*r^4 + b*q^4) =
L * (a * b * (r - 1)^2 * (q - 1)^2 * (r - q)^2) := by
unfold numerator det3
ring
/-- Five samples recover L exactly, even for growing or oscillating modes. -/
theorem two_mode_exact (L a b r q : K)
(ha : a ≠ 0) (hb : b ≠ 0) (hr : r ≠ 1) (hq : q ≠ 1) (hrq : r ≠ q) :
transform (L + a + b) (L + a*r + b*q) (L + a*r^2 + b*q^2)
(L + a*r^3 + b*q^3) (L + a*r^4 + b*q^4) = L := by
have hd : a * b * (r - 1)^2 * (q - 1)^2 * (r - q)^2 ≠ 0 :=
mul_ne_zero (mul_ne_zero (mul_ne_zero (mul_ne_zero ha hb)
(pow_ne_zero _ (sub_ne_zero.mpr hr))) (pow_ne_zero _ (sub_ne_zero.mpr hq)))
(pow_ne_zero _ (sub_ne_zero.mpr hrq))
unfold transform
rw [numerator_factor, denominator_factor]
exact mul_div_cancel_right₀ L hd
/-- A shift of the window only rescales the two error amplitudes. -/
theorem sample_shift (L a b r q : K) (n k : Nat) :
sample L a b r q (n + k) = sample L (a * r^n) (b * q^n) r q k := by
unfold sample
simp only [pow_add]
ring
/-- A complete sequence-level statement, for every natural-number index. -/
theorem sequence_exact (L a b r q : K)
(ha : a ≠ 0) (hb : b ≠ 0) (hr0 : r ≠ 0) (hq0 : q ≠ 0)
(hr1 : r ≠ 1) (hq1 : q ≠ 1) (hrq : r ≠ q) (n : Nat) :
transform (sample L a b r q n) (sample L a b r q (n+1))
(sample L a b r q (n+2)) (sample L a b r q (n+3))
(sample L a b r q (n+4)) = L := by
have h := two_mode_exact L (a*r^n) (b*q^n) r q
(mul_ne_zero ha (pow_ne_zero _ hr0)) (mul_ne_zero hb (pow_ne_zero _ hq0))
hr1 hq1 hrq
simpa [sample, pow_add, mul_assoc] using h
/-- A single geometric mode makes the order-two denominator singular.
The raw quotient cannot replace Shanks's separate order-reduction rule. -/
theorem single_mode_singular (L a r : K) :
denominator (L+a) (L+a*r) (L+a*r^2) (L+a*r^3) (L+a*r^4) = 0 := by
simpa using denominator_factor L a 0 r 0
#print axioms denominator_factor
#print axioms numerator_factor
#print axioms two_mode_exact
#print axioms sample_shift
#print axioms sequence_exact
#print axioms single_mode_singular
end PaperToLean.Shanks
Inspect the verification record
The exactness results use propext, Classical.choice, and Quot.sound. The polynomial identities and singularity lemma use only propext and Quot.sound. Every advertised theorem is audited individually. There are no custom axioms, sorry placeholders, or native_decide proofs.
Lean 4.33.1
Dependencies: Mathlib 4.33.1 (see bundled lake-manifest.json)
File: Shanks.lean
SHA-256: 0dd4b0b9d09ce379bb11d5bc19cb728119a46f13ea9fa644b45452aa4015ed46
Result: passed
'PaperToLean.Shanks.denominator_factor' depends on axioms: [propext, Quot.sound]
'PaperToLean.Shanks.numerator_factor' depends on axioms: [propext, Quot.sound]
'PaperToLean.Shanks.two_mode_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Shanks.sample_shift' depends on axioms: [propext, Quot.sound]
'PaperToLean.Shanks.sequence_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Shanks.single_mode_singular' depends on axioms: [propext, Quot.sound]
SHA-256: 0dd4b0b9d09ce379bb11d5bc19cb728119a46f13ea9fa644b45452aa4015ed46
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 Shanks.lean