The Sixty-Fifth Distance

w₁ = 1/2 + i√3/2; w₃ = 5/6 + i√11/6; z = a + b·w₁ + c·w₃ + d·w₁w₃.

|z|² = r + s√33; unit exactly when r = 1 and s = 0.

Subtract two coordinate vectors and expand the squared modulus. Independence of the rational part and the square-root part makes the equality test exact.

Dragging rounds two basis coefficients to fractions with denominator 120. The arithmetic checks those snapped coordinates exactly; the screen is approximate. Arrow keys move the selected point by one such step.

Select a pair after the coordinates load.

The basis and the complete integer unit-direction list are in Engel et al., the Moser lattice section. Read the arithmetic.

For an ordinary unit-distance graph, a pair not listed as an edge may still be a unit distance. That is allowed. Here the target already reaches the averaging upper bound, so its graph must list every unit pair. Its ancestors are induced subgraphs: they inherit both edges and the absence of edges. If an ancestor forces a missing pair to have unit length, the final drawing would have an extra pair beyond the bound.

That is the hereditary TU argument. It would be unsound to discard an arbitrary graph just because it has an unlisted unit pair. Unknown verdicts were kept throughout the filter-only run.

Written lemmas and trust chain · AMP's linear-relation method.

For unit displacements x, y, z with ax + by + cz = 0, put A = |a|², B = |b|², C = |c|², q = A + B − C and Δ = 4AB − q². A split checks d² = Δ and covers both rows (q ± id)ax + 2Aby = 0.

All three edges must be present, all three coefficients must be nonzero, and the starting relation must follow from the current row space. Each child must equal precisely the parent constraints plus its specified orientation row.

At a leaf, two graph edges obey x = ωy. Their unit lengths would require |ω|² = 1. The checker proves this relation and computes a different exact squared modulus, so the branch is impossible.

The certificate works in a real field of degree 4. Exact polynomial reduction and rational root isolation certify one selected root; decimals below are display approximations.

The root is reconstructed from every graph rhombus. For distinct points, a 4-cycle of unit edges (a rhombus) has coincident diagonal midpoints. A triangle supplies the equilateral alternatives used by the first splits. Later splits use weighted edge relations; no guessed coordinates enter the refutation.

The browser checker supports only the split and nonunit-multiplier rules used here, and rejects other move kinds. Proof checker · Exact field arithmetic · AMP's Heron rule.

The cell extract cannot prove that the graph generator omitted nothing. Exhaustiveness rests on the canonical augmentation argument, the enumeration and pruning implementations, and their archived checks. The reproduction sample shares nauty with the production enumerator. Its sampled parent indices were not retained.

The large intermediate files and pruning certificates were replayed before deletion; they are not bundled into this page. They can be regenerated from the research procedure. The largest slices needed a streaming checker. A partitioned diagnostic did not finish every dense piece with the unchanged in-memory checker; those slices are covered by the streaming whole-slice check, not by a claim that the diagnostic completed.

Both exact certificate programs use the same written geometric implications. An error in a lemma could pass both. The compiler, interpreters, machine arithmetic and source-to-output history remain part of the computation's trust chain. The full re-run reduces reliance on the original worker artifacts; it does not formally verify the software.

The free display choices are a deterministic graph layout, an optional logarithmic bar scale, and the rounded dragging grid. Graph-layout lengths and all decimals are illustrative. The lattice landing exercise fixes the other points and searches only integer unit directions; the upper-bound argument applies to arbitrary distinct points in the plane.

The research account of these limits · Sources and terms.