---
id: F-026
title: Strict shell-threshold readings are false
tier: lean
polarity: negative
depends_on: [F-023, F-024, F-025]
supersedes: []
verifier: cd verified_math/F-026_strict-shell-readings-counterexamples/lean && lake build && ! grep -R -n -E '\b(sorry|admit|native_decide)\b' Research.lean Research
date: 2026-07-12
---

## Statement

All principal normalized/local interpretations of Erdős's separately quoted
strict shell wording fail, under both the printed and corrected comparison
values.

### Corrected cumulative comparison

Squared norm 300 is a genuine triangular-lattice shell (`t=√300=10√3`).
The complete corrected closed triangular count is 1074 (and its strict count
is 1068).  The one-separated rational oblique lattice with basis

```text
(1,0), (276/565,493/565)
```

has 1078 nonzero offsets at ordinary distance **strictly below** `√300`.
A boundary-corrected `4535×4535` patch has 20,566,225 points and at least
22,088,128,946 directed strict pairs, exceeding
`1074·20,566,225=22,088,125,650` by 3296.  It has at least 11,044,064,473
direct unordered strict pairs, exceeding `537n` by 1648.  Far-separated copies
formally negate both full eventual corrected strict-shell claims.

### Printed value `f(3)=18`

The exact rational 38-point configuration from F-023 has exactly 710 directed
pairs (355 unordered) at ordinary distance **strictly below 3**.  Thus its
average directed degree exceeds the printed comparison 18 (`710>18·38=684`),
and its unordered count exceeds `9·38=342`.  Far-separated copies formally
negate both eventual global normalized versions.  Their distinguished centers
have 37 strict neighbours, so the eventual local reading fails for both the
printed value 18 and corrected value 36.

The consolidated theorem `strict_shell_readings_false` includes:

- corrected complete counts 1074/1068;
- `¬ EventualCorrectedStrictShellDirectedBound`;
- `¬ EventualCorrectedStrictShellUnorderedBound`;
- `¬ EventualPrintedStrictThreeGlobalBound`;
- `¬ EventualPrintedStrictThreeUnorderedBound`; and
- `¬ EventualStrictThreeLocalBound 18` and
  `¬ EventualStrictThreeLocalBound 36`.

All final threshold statements use ordinary Euclidean distance with strict
`<`, and every negation retains the sufficiently-large quantifier.

## Proof / verification

For the corrected strict witness, Lean proves

```text
565m²+565n²+552mn = 276(m+n)²+289m²+289n² ≥ 565
```

for every nonzero integer offset, establishing one-separation.  Kernel
`decide` on an explicit executable `[-24,24]²` window verifies the 1078
strict offsets, both triangular counts, and the exact weighted boundary sum.
Separate inequalities prove all windows complete.  As in F-025, a dependent
incidence type and injective endpoint map reduce a 22-billion-pair lower bound
to the small offset census; translated copies scale the excess.

For the printed value, a kernel census of the exact integer-coordinate
38-point witness proves exactly 710 oriented strict pairs.  A product incidence
embedding places these pairs in every translated block.  Endpoint-swap proofs
identify both directed counts with twice the direct unordered counts.  Exact
square-root lemmas connect squared inequalities to ordinary strict thresholds.
No floating point or approximate geometry enters the proof.

Artifacts:

- `lean/Research/StrictShellReadings.lean` — all strict censuses,
  constructions, replications, factor-two proofs, and eventual negations;
- `lean/Research/{GlobalShellSix,ShellCounterexample38,TriangularShells,Basic}.lean`
  — depended-on verified constructions and geometry;
- pinned Lean project files;
- `numerics/exact_strict_shells.py` and output — independent integer audit of
  the corrected strict-shell construction (cross-validation only).
