---
id: F-025
title: Global shell-six average-degree counterexample
tier: lean
polarity: negative
depends_on: [F-002]
supersedes: []
verifier: cd verified_math/F-025_global-shell-six-average-counterexample/lean && lake build && ! grep -R -n -E '\b(sorry|admit|native_decide)\b' Research.lean Research
date: 2026-07-12
---

## Statement

The plausible shell-restricted global normalized version of Erdős #662 is
false already at the genuine triangular-lattice shell radius `t=6`.  The unit
triangular lattice has exactly 126 nonzero points at distance at most six, but
the one-separated rational oblique lattice generated by

```text
u = (1,0),  v = (136/305,273/305)
```

has 128 nonzero offsets in that ball.  A boundary-corrected `365×365` finite
patch has 133,225 points and at least 16,786,618 directed radius-six pairs,
strictly above `126·133225=16,786,350`; equivalently it has at least 8,393,309
direct unordered pairs, strictly above `63·133225=8,393,175`.

Moreover, for every requested cardinality `N`, `N+1` copies translated far
apart give a one-separated finite configuration of cardinality at least `N`
with the same strict normalized excess.  Thus neither the eventual directed
average-degree claim nor the equivalent unordered claim `E₆≤63n` can hold.
All source-facing final statements use ordinary Euclidean distance, not merely
squared-distance notation.

Formally, the main theorems are:

- `triCoordsWithinThirtySix_card` and
  `mem_triCoordsWithinThirtySix_iff` (the complete triangular count is 126);
- `obliquePoint_oneSeparated`;
- `shellSixIncidence_card` (exactly 16,786,618 certified directed incidences);
- `arbitrarily_large_global_shell_six_counterexamples_ordinary`;
- `not_eventualShellSixDirectedAverageBound`;
- `not_eventualShellSixUnorderedBound`; and
- `triangular_shell_six_global_average_reading_false`.

## Proof / verification

For an integer offset `(m,n)`, squared distance in the oblique lattice is

```text
Q(m,n) = (305m² + 305n² + 272mn)/305.
```

Lean proves the exact decomposition

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

which is at least 305 for every nonzero integer pair, establishing global
one-separation.  Kernel `decide` over the explicit `[-6,6]²` window proves
there are 128 allowed offsets and verifies the boundary sum

```text
Σ (365-|m|)(365-|n|) = 16,786,618.
```

Separate inequalities prove this window is complete.  A dependent incidence
type contains the legal starts for each signed offset.  Lean computes its
cardinality symbolically via `Fintype.card_sigma` and the tiny offset sum, then
constructs an injective map from incidences to actual directed patch pairs;
no enumeration of the roughly 17 billion possible patch pairs occurs.
Endpoint swapping proves the factor two between directed and unordered counts.
Finally, blocks translated 2000 units apart preserve one-separation, and a
product incidence embedding scales the strict excess to arbitrarily large
cardinalities.  Ordinary-distance finsets are proved exactly equal to their
squared-distance versions using `Real.sqrt_le_iff`.

Artifacts:

- `lean/Research/GlobalShellSix.lean` — complete construction, exact censuses,
  structural incidence count, replications, ordinary-distance equivalence, and
  negations of both eventual normalized claims;
- `lean/Research/{Basic,TriangularShells}.lean` — squared Euclidean distance and
  earlier triangular-coordinate infrastructure;
- `lean/Research.lean` and pinned Lake project files;
- `numerics/exact_shell_six.py` and its output — an independent exact-integer
  audit of the offset count, boundary statistics, finite excess, and first
  winning square side length.  This script is cross-validation only; Lean is
  the verifier.
