# Erdős #662 — source-facing Lean verifier

Run from the snapshot root:

```bash
check_answer/verify.sh
```

A successful run ends with `PASS`. The script:

1. verifies hashes of the maintained problem pages, official journal TOC,
   the recovered NDL primary-source metadata/OCR, related primary papers, and
   original packing provenance;
2. semantically audits 28 overlapping official NDL OCR snippets, identifying
   the 1997 article and reconstructing 943 consecutive source characters with
   no gap or conflict;
3. runs independent exact-integer audits of both closed and strict shell
   censuses and boundary arithmetic;
4. clean-builds the pinned Lean 4 + Mathlib project and prints the axioms of
   every source-facing theorem;
5. rejects every Lean source containing `sorry`, `admit`, or `native_decide`.

## What is verified

The primary 1997 passage has now been recovered from the National Diet
Library's official digitization (PID `10996926`). Its OCR independently
confirms the threshold comparison, triangular equality question, particular
clause, and stronger shell formulation; hence this is not a later catalog
invention or the distinct 1987 two-smallest-multiplicity theorem. Mathematical
glyphs in that OCR remain poor, and the printed problem is acknowledged by its
maintainer to be corrupt. This checker therefore does **not** silently choose a
missing factor or typo. It resolves the major local and global shell readings
explicitly:

- `Research.sqrt_three_sub_epsilon_has_fewer_than_twelve_neighbors`:
  for every `ε>0`, every point of every finite one-separated planar set has
  fewer than 12 neighbours at distance at most `√3-ε`.
- `Research.thresholdUnorderedPairs_card_lt_six_mul_of_lt_sqrt_three`:
  the corresponding direct unordered pair count is `<6n` for every nonempty
  finite set and every threshold below `√3`.
- `Research.triangular_shell_three_local_bound_false` and
  `Research.arbitrarily_large_shell_three_local_counterexamples`:
  an exact rational configuration has 37 local neighbours below ordinary
  distance 3, versus the corrected triangular value 36, and far-separated
  copies remove the sufficiently-large escape.
- `Research.triangular_shell_six_global_average_reading_false`:
  the triangular comparison at ordinary radius 6 is exactly 126, but a
  one-separated rational oblique-lattice patch has 16,786,618 directed short
  pairs on 133,225 points, exceeding `126n` by 268.  Equivalently it has
  8,393,309 direct unordered pairs, exceeding `63n` by 134.
- `Research.not_eventualShellSixDirectedAverageBound` and
  `Research.not_eventualShellSixUnorderedBound`:
  translated copies give arbitrarily large counterexamples, formally negating
  the full eventual quantifiers under both equivalent normalizations.
- `Research.not_eventualCorrectedStrictShellDirectedBound` and
  `Research.not_eventualCorrectedStrictShellUnorderedBound`:
  at the genuine shell `t=√300`, the corrected closed triangular comparison is
  1074, while a one-separated rational oblique patch has 22,088,128,946
  directed pairs strictly below the shell on 20,566,225 points—an excess of
  3296 over `1074n`; replicas remove every cutoff.
- `Research.not_eventualPrintedStrictThreeGlobalBound`,
  `Research.not_eventualPrintedStrictThreeUnorderedBound`, and
  `Research.printed_and_corrected_strict_three_local_bounds_false`:
  the exact 38-point blocks have 710 directed/355 unordered pairs strictly
  below 3, refuting normalized use of the printed value 18, while their center
  degree 37 refutes both printed local 18 and corrected local 36.

Thus the natural repaired particular clause (“fewer than **12**” below
`√3-ε`) is true, while the closed and strict all-shell local/global readings
are false under both printed and corrected comparison conventions.

See [`SOURCE_AUDIT.md`](SOURCE_AUDIT.md) for the line-by-line fidelity analysis.
