# Prior-work and source-correspondence record

Search date: 2026-09-09. Scope: the specific Aitken and order-two Shanks
results described on the artifact pages, with an emphasis on Lean.

**Result: no matching formalization located in this bounded search. Priority
is unconfirmed.** These are newly written proofs for this project, not newly
discovered mathematical theorems and not certified first formalizations.

## Direct library inspection

Searched the complete `Mathlib/` source tree, case-insensitively, at:

- The build's pinned Mathlib v4.33.1 revision:
  `0df444a360eaa60ab8c11dca51a86af692955474`.
- The upstream `master` revision fetched during this search:
  `ac7917d6a517b3b710987e9f8037bdcac522a461`.

Search expression:

```text
aitken|shanks|delta.?squared|delta.?2.process|convergence.?acceleration
```

Neither source tree returned a match. This is a name/comment search, not a
semantic comparison of every theorem statement. Generic field, determinant,
sequence, and limit lemmas already exist and are explicitly reused.

Sources:

- https://github.com/leanprover-community/mathlib4/tree/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib
- https://github.com/leanprover-community/mathlib4/tree/ac7917d6a517b3b710987e9f8037bdcac522a461/Mathlib

## Publicly indexed searches

Queries included:

```text
"Aitken" "delta" "Lean" formalization
"Aitken" "formalization" "Lean"
"Aitken" "delta" site:github.com lean
"Aitken" "formal" "Coq"
"Aitken" "delta" "formalised"
"Aitken" "delta" "Isabelle"
"Shanks transformation" "Lean"
"Shanks" "transformation" site:github.com lean
"Shanks" "transformation" "formalized"
"Shanks" "transformation" "Coq"
"Shanks" "Isabelle"
```

No matching checked proof was found in these results. Some hits concerned
ordinary numerical implementations, papers using Aitken acceleration without
formalizing it, people named Aitken, or the unrelated Tonelli–Shanks algorithm.
None establishes priority for this project. Native authenticated GitHub code
search and exhaustive searches of Coq, Isabelle, HOL, and Mizar libraries were
not performed. Unindexed repositories, private work, alternate terminology,
and equivalent statements under other names may have been missed.

## Candidates excluded

Initial searches for more familiar graph/combinatorial results found existing
formalization work, so these were not selected as novelty candidates:

- Sperner-related work: https://firsching.ch/FormalBook/blueprint/chapter28.html
- Motzkin–Straus-related work: https://github.com/ShengtongZhang-alt/SqOmega
- Goodman-related work: https://github.com/math-commons/graphons/blob/main/audit/FAITHFULNESS.md

These links are discovery evidence, not independent audits of those projects.

## Aitken: what was actually consulted

A. C. Aitken, *On Bernoulli's Numerical Solution of Algebraic Equations*,
Proceedings of the Royal Society of Edinburgh 46, pp. 289–305.

- Publisher record and abstract: https://doi.org/10.1017/S0370164600022070
- Cambridge dates the volume 1927; numerical-analysis literature commonly
  cites the work as 1926. The artifact retains 1926 with this discrepancy stated.
- The publisher's full paper was not accessible during this work. Therefore
  no page-by-page equivalence to the original proof is claimed.
- Shanks's 1955 paper, equation (3), gives the first-order transformation;
  its historical notes explicitly discuss Aitken's use of it. The public
  scan/transcription below was consulted.
- The ratio-limit theorem and the additional residual/equivariance lemmas
  are a modern development of that transformation, not attributed verbatim
  to a numbered theorem in Aitken's original paper.

## Shanks: precise scope in the original paper

Daniel Shanks, *Non-linear Transformations of Divergent and Slowly Convergent
Sequences*, Journal of Mathematics and Physics 34 (1955), pp. 1–42.

- Publisher record: https://doi.org/10.1002/sapm19553411
- Public scan/transcription consulted:
  https://www.scribd.com/document/817963139/Shanks-Transformation
- Equation (2): the determinant quotient. Our file takes k = 2 and uses a
  forward five-sample window instead of a centered index.
- Equations (17)–(23), in the introduction: the finite-transient model and
  recovery of its base. Our file proves the distinct two-mode case.
- The denominator/numerator factorization lemmas explicitly certify this
  case and its degeneracies. No claim is made to formalize all orders,
  repeated roots, the paper's later convergence theorems, or its rules (2b)
  and (2c) for singular cases.

The public transcription contains OCR errors; the formalization uses the
mathematical formulas, checks their polynomial expansions, and proves
nonvanishing before cancellation. The original papers are linked, not
redistributed with the artifact ZIPs.