Canonical naturals

CanonicalNat F says that every element of F has a canonical natural number below a fixed bound, and that every natural reduces to an element by ofNat, with ofNat acting as reduction modulo bound. The laws make toNat a bijection onto Fin bound, so bound is the cardinality of F and ofNat is exactly "the element whose canonical natural is n % bound".

For a prime field the canonical natural is the residue in [0, p); for a binary field it is the bit pattern of the declared basis; for an extension of degree d over a base of size q it is the base-q expansion of the coefficients.

Serialization is derived from this class rather than stated with it. The fixed-width byte codec of a scalar field is the little-endian bytes of toNat (ByteCodec.ofCanonicalNat in CompPoly.Data.Bytes.CanonicalNat), and sampling a field element from a longer byte string is ofNat of the string's integer, which is uniform up to a bound proved in Nat terms. Two carriers of the same field agree on toNat, so they agree on every derived encoding.

class CompPoly.CanonicalNat (F : Type u) : Type u

F has a canonical natural below bound for every element, and every natural reduces to an element of F modulo bound. The laws make toNat a bijection F ≃ Fin bound.

• bound : ℕ

  The exclusive upper bound on canonical naturals; equal to the cardinality of F.

• toNat : F → ℕ

  The canonical natural of an element.

• ofNat : ℕ → F

  The element with canonical natural n % bound.

• toNat_lt (x : F) : toNat x < bound F
• ofNat_toNat (x : F) : ofNat (toNat x) = x
• toNat_ofNat_of_lt {n : ℕ} (h : n < bound F) : toNat (ofNat n) = n
• ofNat_mod (n : ℕ) : ofNat (n % bound F) = ofNat n

theorem CompPoly.CanonicalNat.bound_pos {F : Type u} [CanonicalNat F] : 0 < bound F

theorem CompPoly.CanonicalNat.toNat_injective {F : Type u} [CanonicalNat F] : Function.Injective toNat

@[simp]

theorem CompPoly.CanonicalNat.toNat_inj {F : Type u} [CanonicalNat F] {x y : F} : toNat x = toNat y ↔ x = y

@[simp]

theorem CompPoly.CanonicalNat.toNat_ofNat {F : Type u} [CanonicalNat F] (n : ℕ) : toNat (ofNat n) = n % bound F

def CompPoly.CanonicalNat.ofNat? {F : Type u} [CanonicalNat F] (n : ℕ) : Option F

Decode a natural as an element, failing when it is not a canonical natural.

@[simp]

theorem CompPoly.CanonicalNat.ofNat?_toNat {F : Type u} [CanonicalNat F] (x : F) : ofNat? (toNat x) = some x

theorem CompPoly.CanonicalNat.ofNat?_eq_some_iff {F : Type u} [CanonicalNat F] {n : ℕ} {x : F} : ofNat? n = some x ↔ n < bound F ∧ toNat x = n

theorem CompPoly.CanonicalNat.ofNat?_eq_none_iff {F : Type u} [CanonicalNat F] {n : ℕ} : ofNat? n = none ↔ bound F ≤ n

def CompPoly.CanonicalNat.equivFin {F : Type u} [CanonicalNat F] : F ≃ Fin (bound F)

The canonical natural as an equivalence with Fin (bound F).

theorem CompPoly.CanonicalNat.card_eq {F : Type u} [CanonicalNat F] [Fintype F] : Fintype.card F = bound F

The bound is the cardinality of F.

Constructors

Two ways a concrete type acquires the structure. A fast carrier of a prime field supplies its own toNat together with the conversion from ZMod p; a binary field supplies its bit pattern. Both are @[instance_reducible] definitions so an instance can be CanonicalNat.ofToField … or CanonicalNat.ofBitVec … directly.

@[instance_reducible]

def CompPoly.CanonicalNat.ofToField {F : Type u} {p : ℕ} [NeZero p] (toNat : F → ℕ) (ofField : ZMod p → F) (toNat_lt : ∀ (x : F), toNat x < p) (ofField_cast_toNat : ∀ (x : F), ofField ↑(toNat x) = x) (toNat_ofField : ∀ (n : ZMod p), toNat (ofField n) = n.val) : CanonicalNat F

The canonical-natural structure of a carrier of ZMod p: the carrier's own toNat, with ofField as the way back. The hypothesis toNat_ofField is the carrier-agreement law, so every encoding derived from this structure agrees with the one on ZMod p.

@[instance_reducible]

def CompPoly.CanonicalNat.ofBitVec {F : Type u} {k : ℕ} (toBitVec : F → BitVec k) (ofBitVec : BitVec k → F) (ofBitVec_toBitVec : ∀ (x : F), ofBitVec (toBitVec x) = x) (toBitVec_ofBitVec : ∀ (b : BitVec k), toBitVec (ofBitVec b) = b) : CanonicalNat F

The canonical-natural structure of a type presented as k-bit patterns: the bit pattern read as an integer, with bound = 2 ^ k.

@[instance_reducible]

instance CompPoly.instCanonicalNatZMod (p : ℕ) [NeZero p] : CanonicalNat (ZMod p)

ZMod p with the residue in [0, p) as canonical natural.

@[simp]

theorem CompPoly.CanonicalNat.bound_zmod (p : ℕ) [NeZero p] : bound (ZMod p) = p

@[simp]

theorem CompPoly.CanonicalNat.toNat_zmod {p : ℕ} [NeZero p] (x : ZMod p) : toNat x = x.val

@[simp]

theorem CompPoly.CanonicalNat.ofNat_zmod {p : ℕ} [NeZero p] (n : ℕ) : ofNat n = ↑n