ScalarBinaryEmbedding.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Constructing the binary point map from nested finite forks. The resulting map has exactly the bit-update bounds used in the sumset step.