Erdős Problem 482

Read formalization.yaml

authors

Trevor Morris

method

autonomous

review

self-assessed (Trevor Morris)

axioms

Classical.choice, Quot.sound, propext

sorry

1 unproved goals declared

results

7 main results named, checked with Comparator, with an alignment table

sources

On the restricted ordinal theorem; Accessible independence results for Peano arithmetic; Erdős Problem #403 (only finitely many powers of two are sums of distinct factorials); On consecutive sums in sequences

divergences

Erdős #482 is resolved in GREATER generality than the source: `erdos482_resolution` proves that for every real w > 0 and base g >= 2 an explicit Graham-Pollak-type recurrence reads the base-g digits of w, not merely the binary digits of √2. Erdős #880 is likewise extended beyond the headline question (exact order, and the HHP07 Theorem 3/4/8/9 companions are included). Erdős #1050: the general engine (`borwein_thm1_abs`) proves Borwein's Theorem 1 in full -- ∑ 1/(qⁿ+c) is irrational for any integer base of magnitude >= 2 and any nonzero rational c -- which is stronger than the q=2, c=-3 instance the problem asks for. In the comparator challenges, both k >= 3 headlines of #880 are stated EXISTENTIALLY ("there is a basis of order h whose restricted-sum set has unbounded gaps"), which is what HHP07 Thm 1(ii) claims. The proof supplies the explicit Hegyvári-Hennecart-Plagne witness, but naming that construction in the challenge would drag its recurrence into the trusted surface for no gain.

checked by

nobody independent of its authors yet