theorem Elligator.Elligator1.bitsToNat_le_full_range {n : ℕ} (τ : Fin n → Bool) : bitsToNat τ ≤ ∑ i ∈ Finset.range n, 2 ^ i

theorem Elligator.Elligator1.bitsToNat_lt_two_pow_n {n : ℕ} (τ : Fin n → Bool) : bitsToNat τ < 2 ^ n

Every bit-vector of length n has binary value less than 2^n.

theorem Elligator.Elligator1.bitsToNat_le_q_sub_one_over_two {q : ℕ} (τ : ↥S) : bitsToNat ↑τ ≤ (q - 1) / 2

theorem Elligator.Elligator1.bitsToNat_injective {n : ℕ} : Function.Injective bitsToNat

bitsToNat is injective: distinct bit-vectors give distinct natural numbers.

theorem Elligator.Elligator1.bitsToNat_surj (n m : ℕ) (hm : m < 2 ^ n) : ∃ (τ : Fin n → Bool), bitsToNat τ = m

Every natural number less than 2^n is the binary value of some bit-vector.

theorem Elligator.Elligator1.natCast_injective_of_prime_card {F : Type u_1} [Field F] [Fintype F] (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime : Prime q) (a b : ℕ) (ha : a < q) (hb : b < q) (h : ↑a = ↑b) : a = b

theorem Elligator.Elligator1.lower_half_neg_eq {F : Type u_1} [Field F] [Fintype F] {q : ℕ} (field_cardinality : Fintype.card F = q) (hq : Prime q) {a b : ℕ} (ha : a ≤ (q - 1) / 2) (hb : b ≤ (q - 1) / 2) (heq : ↑a = -↑b) : a = b

theorem Elligator.Elligator1.σ_injective {F : Type u_1} [Field F] [Fintype F] {q : ℕ} (field_cardinality : Fintype.card F = q) (q_prime : Prime q) (q_mod_4_congruent_3 : q % 4 = 3) : Function.Injective σ

theorem Elligator.Elligator1.exists_S_elem_of_le {q : ℕ} (q_mod_4_congruent_3 : q % 4 = 3) (n : ℕ) (hn : n < q) (hle : n ≤ (q - 1) / 2) : ∃ (τ : ↥S), bitsToNat ↑τ = n

theorem Elligator.Elligator1.exists_σ_preimage_or_neg {F : Type u_1} [Field F] [Fintype F] {q : ℕ} (field_cardinality : Fintype.card F = q) (q_prime : Prime q) (q_mod_4_congruent_3 : q % 4 = 3) (t : F) : ∃ (τ : ↥S), σ ↑τ = t ∨ σ ↑τ = -t