Documentation

LeanPool.GKPCarry.PowerResidues

Powers of two modulo powers of three #

This file proves that 2 generates the unit group modulo every positive power of three. At level n, its order modulo 3 ^ (n + 1) is exactly 2 * 3 ^ n. Thus one complete period of exponents is equivalent to the full unit group.

source
def GKPCarry.twoUnit (level : ℕ) :
(ZMod (3 ^ (level + 1)))ˣ

The unit represented by 2 modulo 3 ^ (level + 1).

Equations
Instances For
    source
    theorem GKPCarry.orderOf_twoUnit_sq (level : ℕ) :
    orderOf (twoUnit level ^ 2) = 3 ^ level
    source
    theorem GKPCarry.two_dvd_orderOf_twoUnit (level : ℕ) :
    2 ∣ orderOf (twoUnit level)
    source
    theorem GKPCarry.orderOf_twoUnit (level : ℕ) :
    orderOf (twoUnit level) = 2 * 3 ^ level

    The multiplicative order of 2 modulo 3 ^ (level + 1) is the full Euler period 2 * 3 ^ level.

    source
    theorem GKPCarry.card_units_three_pow_succ (level : ℕ) :
    Fintype.card (ZMod (3 ^ (level + 1)))ˣ = 2 * 3 ^ level

    The unit group modulo 3 ^ (level + 1) has 2 * 3 ^ level elements.

    source
    def GKPCarry.twoPowerUnitMap (level : ℕ) :
    Fin (2 * 3 ^ level) → (ZMod (3 ^ (level + 1)))ˣ

    Send an exponent in one complete period to the corresponding power of 2 in the unit group.

    Equations
    Instances For
      source
      theorem GKPCarry.twoPowerUnitMap_injective (level : ℕ) :
      Function.Injective (twoPowerUnitMap level)
      source
      noncomputable def GKPCarry.twoPowerUnitEquiv (level : ℕ) :
      Fin (2 * 3 ^ level) ≃ (ZMod (3 ^ (level + 1)))ˣ

      A complete period of exponents is equivalent to all units modulo the corresponding power of three.

      Equations
      Instances For
        source
        @[simp]
        theorem GKPCarry.twoPowerUnitEquiv_apply (level : ℕ) (exponent : Fin (2 * 3 ^ level)) :
        (twoPowerUnitEquiv level) exponent = twoUnit level ^ ↑exponent
        source
        theorem GKPCarry.val_twoPowerUnitEquiv_apply (level : ℕ) (exponent : Fin (2 * 3 ^ level)) :
        (↑((twoPowerUnitEquiv level) exponent)).val = 2 ^ ↑exponent % 3 ^ (level + 1)

        The natural representative of the unit associated to an exponent is the ordinary modular power.

        source
        theorem GKPCarry.two_pow_mod_three_pow_succ_eq_reduced_exponent (level exponent : ℕ) :
        2 ^ exponent % 3 ^ (level + 1) = 2 ^ (exponent % (2 * 3 ^ level)) % 3 ^ (level + 1)

        Reduction of an arbitrary exponent to the exact period does not change the residue modulo 3 ^ (level + 1).