Unit-distance final grid

The quantity is the number of selected edges $Nj$ in the final algebraic-grid proof step. Fewer edges are better. The claim assumes the upstream generic-grid and private-valuation lemmas. The line cases are separate, and no better headline unit-distance exponent is claimed.

OpenAI baseline: $20\cdot5=100$ , released Oct 6, 2:58 PM PT.

These results are Claimed: their authors published them, and we have not checked them.

Bound	Evidence level	Author	Date	Proof scope
$8\cdot4=32$	Claimed	Rohan Arun	Oct 9, 10:36 PM PT	Proof scope No Lean proof is supplied.

Relevant repos

rohanarun/unit-distance-grid-refinement: The line cases are separate from the final grid.