QuietMethod
Independent verification & quantitative refinement

Erdős Problem #671

A complete construction with pointwise-unbounded Lebesgue functions everywhere, yet a convergence point for every continuous function.

Stage samples
k2 + 1
Lean source
2,830 lines
Checked
No sorry / admit

Both questions are answered affirmatively.

There exists a triangular array of distinct interpolation nodes in [-1, 1] whose Lebesgue functions λn satisfy

lim supn → ∞ λn(x) = ∞for every x ∈ [-1, 1],

while for every continuous function f there is a point xf ∈ [-1, 1] such that

Lnf(xf) → f(xf).

The second statement holds at the same point where the Lebesgue functions are unbounded along a subsequence.

Large locally, controlled everywhere else.

1

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.

2

Nested protection

On the same small interval, every non-selected row has Lebesgue function at most 2. Exterior rows force growth outside the protected intervals.

3

A branch for each f

With Nk = k2 + 1 sample values, two differ by at most 2‖f‖∞/k2. Choosing their branch makes the interpolation error tend to zero.

Selected-branch error3‖f‖/k + ωf(1/k) → 0

Cubic sampling is unnecessary.

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

Existing constructionk3 + 1
This refinementk2 + 1

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.

Machine-checked in Lean.

The 2,830-line formalisation was checked with Lean 4.33.0-rc1 and mathlib. It contains no sorry, admit, or custom axioms.

#print 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.

Read, download, and verify.