# Source and statement-fidelity audit

## 1. Primary-source recovery and maintained transcription

The missing primary source has now been recovered through the official
National Diet Library (Japan) digitization. NDL PID `10996926`, DOI
`10.11501/10996926`, is *Mathematica Japonica* 46(3), November 1997. Its item
metadata and an independent NDL Search SRU/DC-NDL record both index

> P. ERDOÖS, “Some of my favourite unsolved problems,” pp.527–537.

The NDL scan is access-restricted (`ooc`), but the NDL API explicitly permits
anonymous snippets. `references/ndl_primary/` pins the unmodified metadata,
permission response, SRU record, and 28 full-text-search responses. Its offline
`audit_primary_ocr.py` identifies the article's start at issue-content index 82,
the target passage at index 85 (UUID
`a2337306-be89-471c-929b-fb5db315ef08`), and merges OCR offsets 583–1525 into
943 consecutive characters with no gap or overlap conflict.

The primary OCR independently contains, in order:

> “Consider the triangular lattice … denote by f(t) the number of distances
> from any points … Let … be any sequence of points … Is it true … the number
> of distances is less than or equal to f(t) with equality perhaps only for the
> triangular lattice? In particular, is it true that … Perhaps the following
> stronger conjecture holds: Let t₁<⋯ be the set of distances occurring in the
> triangular lattice …”

(The quotation normalizes only obvious OCR spacing/case; the exact 943-character
OCR is pinned.) This externally settles the historical fork that blocked prior
reviews: the absolute-threshold comparison and stronger shell conjecture really
occur in Erdős's 1997 article. They are not a later catalog invention and are
not the distinct 1987 Vesztergombi theorem about the multiplicities of the two
smallest distance values.

The OCR is poor on displayed mathematics (`〓`, missing subscripts and errors
such as `aquality` for “equality”), so it does not by itself authenticate every
glyph or missing normalization factor. For those symbols, the pinned maintained
snapshot `references/erdosproblems_662_2026-07-12.html` gives what it calls an
“essentially verbatim” transcription. It defines `f(t)` as the number of
triangular-lattice distances “from any point” at most `t`, prints

- `f(1)=6`,
- `f(√3)=12`,
- `f(3)=18`,

then asks about “the number of distances” in a finite one-separated set and
ends:

> In particular, is it true that the number of distances ≤ √3−ε is less than 1?

The same page explicitly warns:

> this does not make sense as written; there must be at least one typo.

It then transcribes Erdős's stronger conjecture at triangular-lattice shells
with strict `<t_n`, and again calls the literal wording nonsense. This audit
accepts that warning and treats each surviving count normalization separately.

The official publisher TOC
`references/Mathematica_Japonica_46_3_TOC.html` independently confirms the same
article, pages, volume, and date.

## 2. Machine-confirmed corruption

`Research.TriangularShells` defines the unit triangular lattice by integer
coordinates with squared norm

```text
q(a,b) = a² + ab + b²
```

and exhaustively proves:

```lean
(triCoordsWithin 1).card = 6
(triCoordsWithin 3).card = 12
(triCoordsWithin 9).card = 36
```

Consequently the natural cumulative “from a fixed point” definition has
`f△(3)=36`, not 18. The actual first shell radii are
`1, √3, 2, √7, 3, ...`, not the sequence printed in the commentary. Other
literal count scopes are already refuted in F-018–F-020.

The final `1` is also incompatible with the immediately preceding
`f(√3)=12`. Under the source's own local phrase “from any point”, the smallest
single-character repair is **12**: the printed text has lost its final `2`.
This is a reconstruction, not a claim about inaccessible authorial intent.

## 3. The local/shell reconstruction tested here

For a finite one-separated planar configuration and a fixed point `v`, count
other points within the threshold. Compare this local degree with the number of
nonzero unit-triangular-lattice points in the corresponding centered ball.
This reconstruction is supported by:

1. the defining phrase “from any point”;
2. the values 6 and 12, which are centered local ball counts;
3. the page's quoted restriction to triangular-lattice shell radii;
4. the final `√3−ε` clause, for which the adjacent comparison value is 12.

The checker resolves both parts of this reconstruction rather than assuming
the universal conjecture is true.

### The particular clause is true

`SqrtThreeStrictThreshold.lean` proves, with ordinary Euclidean distance:

```lean
∀ ε > 0, ∀ v,
  #{w ≠ v | dist(w,v) ≤ √3-ε} < 12.
```

It also proves the direct global consequence `E_r<6n` for every nonempty
finite configuration and every `r<√3`. No “sufficiently large” hypothesis is
needed.

### The all-shell local extension is false

`ShellCounterexample38.lean` gives 38 exact rational points. Every distinct
pair is at distance at least one, but point 18 has all 37 other points at
ordinary distance strictly below 3. Since the independently certified
triangular comparison is `f△(3)=36`, this violates both `<36` and `≤36` at an
actual shell, and it uses the stronger strict distance threshold `<3`.

This counterexample is robust to the printed `f(3)=18` error: 37 exceeds both
18 and the corrected value 36.  `arbitrarily_large_shell_three_local_counterexamples`
places far-separated copies of the exact block above every prescribed
cardinality, so the main text's “sufficiently large” qualifier cannot rescue a
local interpretation.

### The shell-restricted global-average reconstruction is also false

The dimensionally meaningful global repair counts unordered short pairs
`E_t(X)` and asks for

```text
2 E_t(X) ≤ f△(t) |X|,
```

or equivalently bounds the directed average degree by `f△(t)`.  Restricting
this repair to actual triangular shell radii does not save it.  At ordinary
radius 6, Lean proves the complete triangular count is `f△(6)=126`.  The
rational oblique lattice with basis

```text
(1,0), (136/305,273/305)
```

is one-separated and has 128 closed-ball offsets.  Boundary accounting on a
`365×365` patch proves at least 16,786,618 directed pairs, while the proposed
allowance is only `126·133225=16,786,350`.  Endpoint swapping gives at least
8,393,309 direct unordered pairs versus `63·133225=8,393,175`.

`not_eventualShellSixDirectedAverageBound` and
`not_eventualShellSixUnorderedBound` use translated copies to negate the full
sufficiently-large quantifiers.  Their definitions use ordinary Euclidean
distance at most 6 and quantify over every finite index type/configuration;
the squared-distance machinery is connected by proved finset equalities.

This addresses the main clause's closed `≤t` shell/global reading.

### The quoted strict-shell wording under printed and corrected comparisons

Because the strict quote is also corrupt, `StrictShellReadings.lean` treats
both comparison conventions rather than choosing one silently.

For the **corrected cumulative** convention, squared norm 300 is a genuine
triangular shell (`t=√300=10√3`).  Lean proves the complete closed comparison
`f△(√300)=1074` (and strict triangular count 1068).  The rational oblique
lattice generated by `(1,0),(276/565,493/565)` is one-separated and has 1078
offsets strictly below this shell.  Boundary correction on a `4535×4535`
patch gives 22,088,128,946 directed strict pairs, 3296 more than `1074n`, and
1648 more direct unordered pairs than `537n`.  Translated copies formally
negate both full eventual strict-shell claims.

For the **printed** comparison `f(3)=18`, the exact 38-point packing has 710
directed (355 unordered) pairs strictly below ordinary distance 3, versus
`18·38=684` (respectively `9·38=342`).  Replicas negate both global eventual
normalizations.  Their center has 37 strict neighbours, so the local strict
reading fails against both printed 18 and corrected 36.

Thus `strict_shell_readings_false` gives an explicit formal treatment of the
strict wording under the printed and corrected cumulative conventions.  It
does not claim that the malformed symbols define a unique authorial intent.

## 4. Exactness and independence of the witnesses

`references/Packomania_cci38_original.txt` records the numerical configuration
that prompted the local search. Lean does **not** trust those decimals or any
floating-point calculation. The proof lists independently rounded integer
coordinates, scales them by the exact rational `349/100000000`, and uses kernel
`decide` to check all 703 distinct-pair integer inequalities and all 37 strict
center inequalities. Symbolic cast lemmas then transfer them to real Euclidean
squared distances.

The shell-six global witness is independently exact.  Lean proves
`136²+273²=305²`, the integer quadratic identity

```text
305m²+305n²+272mn = 136(m+n)²+169m²+169n²,
```

and completeness of both explicit `[-6,6]²` offset windows.  Kernel `decide`
checks only 169 candidate offsets and their weighted boundary sum.  A dependent
incidence type plus an injective endpoint map proves the 16,786,618 lower bound
without enumerating all patch pairs.  `numerics/exact_shell_six.py` separately
recomputes every integer statistic and the verifier runs it before Lean; it is
cross-validation, not part of the proof's trust base.

The corrected strict witness is verified identically: the Pythagorean identity
`276²+493²=565²`, a positive sum-of-squares decomposition, complete explicit
windows, and a dependent incidence injection.  Kernel `decide` sees only 2401
candidate offsets, not the 22 billion certified pairs.  The printed strict
count 710 is a separate kernel census on the exact 38-point coordinates.
`numerics/exact_strict_shells.py` independently checks the 1078/1074/1068
counts, boundary sums, and finite excess.

## 5. Related literature and forum claims

The Rényi archive copy
`Erdos_Lovasz_Vesztergombi_1989_graph_large_distances.pdf` is the complete
Erdős–Lovász–Vesztergombi paper *On the Graph of Large Distances*. It studies
the largest distinct distance levels and does not define the triangular
comparison function in #662. It therefore cannot authorize a silent repair of
the 1997 wording.

The forum-linked April 2026 reconstruction note is pinned as
`erdos662_reconstruction_2026-04.pdf`.  Its first repair analyzes normalized
threshold counts only through the interval surrounding `√3`; its second repair
is Vesztergombi's published two-smallest-distance theorem.  It does not analyze
the shell-restricted global claim at radius 6 and therefore neither contains
nor preempts F-025.  The underlying primary scan
`Vesztergombi_1987_small_distances_pp95-101.pdf` explicitly proves
`m₁+m₂≤6n`; this is the already-known theorem formalized separately in F-017,
not the absolute-threshold statement refuted here. The recovered NDL OCR now
settles this distinction from the primary 1997 article itself: Erdős explicitly
introduces `f(t)`, arbitrary separated sequences, the triangular-lattice
equality question, and the stronger shell conjecture in that passage.

The forum's Fejes Tóth (1942) remark concerns asymptotic packing density.  That
the triangular lattice maximizes points per unit area does not imply that it
maximizes the number of neighbours in every fixed closed ball.  F-025 makes the
distinction concrete: its oblique lattice has lower density but 128 radius-six
offsets versus 126.  A targeted literature-index search found general lattice
packing, smooth-energy, and shell-perturbation papers, but no result specifically
asserting this finite-radius count; the package therefore makes no novelty
claim beyond supplying the exact verified counterexample.

## 6. Scope boundary

F-023/F-024 refute the **local-degree shell** conjecture, F-025 refutes the
closed **global average-degree shell** reconstruction at radius 6, and F-026
refutes the **strict shell** readings under printed and corrected comparators,
all including full eventual quantifiers where meaningful.  The continuous-
threshold literal, normalized, per-point, and distinct-value scopes are
separately treated by F-018–F-020. F-017 is the published theorem about
multiplicities of the first two *distinct distance values*, a different claim.

The primary 1997 passage is now authenticated by official NDL metadata and
continuous overlapping OCR. It fixes the intended **subject**—absolute
thresholds and triangular shells—and eliminates the opposite-answer
Vesztergombi-multiplicity fork. The displayed glyphs remain textually corrupt,
so this package still does not pretend that one missing factor or typo has a
uniquely authenticated repair. Instead, F-018–F-020 treat the continuous
literal/normalized/local/distinct scopes, while F-023–F-026 treat closed and
strict shell scopes under both printed and corrected comparisons. Thus the
remaining OCR ambiguity is covered mathematically rather than used to select a
convenient theorem.

## 7. Pinned hashes

The verifier checks:

```text
9648ac30c99606682084af3c96e43ec496007c36be2b18187d68e92fd1ef4cd8  erdosproblems_662_2026-07-12.html
dee92433847a446118c3c3a2d2b8de9301a901c376883b59ad8f0a9bee57facf  erdosproblems_662_forum_2026-07-12.html
328367c685878e6c02f05c029b9ea8125859a450e1ae08d02433dc2bb99d0746  Mathematica_Japonica_46_3_TOC.html
79c50c3e7e40fbe23dc4677c4d9c27ef0a406cec96cda77655682be7c536cb99  Erdos_Lovasz_Vesztergombi_1989_graph_large_distances.pdf
a9c9c2d7ff458986c340190c2666e8bf1da0c6d288f050389f7a6ca9a1307e8e  Packomania_cci38_original.txt
cf97a53b80e0d9bab3d4d0d741cc02e7de0a5ba26f8bbab8ead2e0b53b277572  Packomania_25_36_table.pdf
63bbc227ca70c9e45ac61f001ab62268e2a53d4efff75f5796c7801e48e5b44f  erdos662_reconstruction_2026-04.pdf
4f6857ed7abdc5371d27b0c76a69248ae4b864c1fdce02ffd1309366c8e30136  Vesztergombi_1987_small_distances_pp95-101.pdf
fcc19491810c101fd7567ec0247063e4300a0fcb023429a2f1d8217d00a51ac8  ndl_primary/audit_primary_ocr.py
7ccc12bba061106495eeb72e8cd9eb96578c6f395fcb7cfa172ffbbf90e7c0f5  ndl_primary/item_api.json
80fcd75d70f727af636a1466df8d293350dd6709db52135404f70ad940189fdf  ndl_primary/ndl_search_sru.xml
91dd6f7c70bb4343a25aa5e2863cca113977d539480aafe63eedd375663b891d  ndl_primary/reconstructed_ocr.txt
f8456b67e3ee1264251c2e74df6072cd907afc610322aabb73699737a66237c7  ndl_primary/snippet_api_capture.json
8c5aaab6e1efdec7f7f9f65cc0de77461c36a46e6b7c9ee7a35299dd6e8449ee  ndl_primary/snippet_permission_api.json
```
