ScalarDenseGraph.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Dense graphs of scalar sums give large original subsets with small quantized difference sets. The floor map is used only as an injective coding of the separated input points.

theorem OAI.Falconer.scalar_dense_graph_refinement line 12