S Properties

This file identifies the binary values represented by S, the lower-half string set used in Theorem 4, and computes its cardinality.

Main results

• bitsToNat_image_S: binary evaluation maps S onto the integer interval [0, (q - 1) / 2].
• S_card_eq_q_add_one_div_two: when q ≡ 3 (mod 4), the set S has (q + 1) / 2 elements.

References

See [bernstein2013a], Section 3.4, Theorem 4.

theorem Elligator.Elligator1.bitsToNat_image_S {q : ℕ} : Finset.image bitsToNat S = Finset.Icc 0 ((q - 1) / 2)

Binary evaluation maps the admissible strings S onto exactly the natural-number interval from 0 through (q - 1) / 2, as required by the definition of S in Theorem 4.

theorem Elligator.Elligator1.S_card_eq_Icc_card {q : ℕ} : S.card = (Finset.Icc 0 ((q - 1) / 2)).card

theorem Elligator.Elligator1.S_card_eq_q_add_one_div_two {q : ℕ} (hq_mod : q % 4 = 3) : S.card = (q + 1) / 2

The lower-half string set S has (q + 1) / 2 elements when q ≡ 3 (mod 4). This is the cardinality computation used in Theorem 4 of the paper.