Coalescing nodes
Pair-indexed interpolation rows are arranged so that three principal Lagrange coefficients approach A, -A, and 1. The selected row therefore has a large Lebesgue function.
A complete construction with pointwise-unbounded Lebesgue functions everywhere, yet a convergence point for every continuous function.
There exists a triangular array of distinct interpolation nodes in [-1, 1] whose Lebesgue functions λn satisfy
while for every continuous function f there is a point xf ∈ [-1, 1] such that
The second statement holds at the same point where the Lebesgue functions are unbounded along a subsequence.
Pair-indexed interpolation rows are arranged so that three principal Lagrange coefficients approach A, -A, and 1. The selected row therefore has a large Lebesgue function.
On the same small interval, every non-selected row has Lebesgue function at most 2. Exterior rows force growth outside the protected intervals.
With Nk = k2 + 1 sample values, two differ by at most 2‖f‖∞/k2. Choosing their branch makes the interpolation error tend to zero.
The public proposed proof used Nk = k3 + 1 cluster samples at stage k. The convergence estimate only requires Ak/(Nk - 1) → 0. Taking Ak = k shows that
This is not a claim of priority for the core coalescing-node idea. The work is presented as an independent verification and quantitative refinement of Liam Price's existing proof claim.
The 2,830-line formalisation was checked with Lean 4.33.0-rc1 and mathlib. It contains no sorry, admit, or custom axioms.
[propext, Classical.choice, Quot.sound]AI assistance from OpenAI Codex (GPT-5) was used in developing, checking, and adapting the argument to Lean. The artifacts below are provided for independent inspection.