Documentation

Elligator.Elligator1.Example

Computational sanity checks #

This plays the same role for the Lean development that the Sage scripts at https://elligator.cr.yp.to/thm1.sage and https://elligator.cr.yp.to/thm4.sage play for the original paper: brute-force numeric evidence, complementary to the actual proofs.

TODO order this a bit and find meaningful examples to check, rather than just dumping a bunch of random computations.

The field and parameter #

source
@[reducible, inline]
abbrev Elligator.Elligator1.Example.F7 :
Type

The field with 7 elements

Equations
Instances For
    source
    instance Elligator.Elligator1.Example.instFactPrimeOfNatNat_elligator :
    Fact (Nat.Prime 7)
    source
    theorem Elligator.Elligator1.Example.q7_prime :
    Nat.Prime 7
    source
    theorem Elligator.Elligator1.Example.F7_isPrimePow :
    IsPrimePow 7
    source
    theorem Elligator.Elligator1.Example.card_F7 :
    Fintype.card F7 = 7
    source
    theorem Elligator.Elligator1.Example.F7_mod_four :
    7 % 4 = 3
    source
    def Elligator.Elligator1.Example.s7 :
    F7

    A non-zero element of F7

    Equations
    Instances For
      source
      theorem Elligator.Elligator1.Example.s7_ne_zero :
      s7 ≠ 0
      source
      theorem Elligator.Elligator1.Example.s7_sq_ne_pm_two :
      (s7 ^ 2 - 2) * (s7 ^ 2 + 2) ≠ 0

      Decoding: ϕ : F7 → E(F7), Definition 2 #

      source
      theorem Elligator.Elligator1.Example.decode_three_on_curve :
      have P := ↑(ϕ 3 s7_ne_zero s7_sq_ne_pm_two card_F7 F7_mod_four); P.1 ^ 2 + P.2 ^ 2 = 1 + d s7 * P.1 ^ 2 * P.2 ^ 2
      source
      def Elligator.Elligator1.Example.mkBits (n : ℕ) :
      Fin (b 7) → Bool

      mkBits n reads off the bits of n, giving an element of Fin (b 7) → Bool for any n without needing to know b 7's concrete value up front.

      Equations
      Instances For
        source
        theorem Elligator.Elligator1.Example.b7_eq :
        b 7 = 2
        source
        theorem Elligator.Elligator1.Example.mkBits_mem_S (n : ℕ) (h : n < 4) :
        mkBits n ∈ S

        All four 2-bit strings land in S for q = 7, since (7-1)/2 = 3 is the largest possible 2-bit value.

        source
        theorem Elligator.Elligator1.Example.S7_card :
        S.card = 4
        source
        theorem Elligator.Elligator1.Example.encode_injective_showcase :
        Function.Injective fun (τ : ↥S) => ι τ s7_ne_zero s7_sq_ne_pm_two card_F7 F7_mod_four