Fast KoalaBear Field Operations

This module provides a native-word implementation of KoalaBear arithmetic as a sidecar to the canonical KoalaBear.Field := ZMod KoalaBear.fieldSize model.

Fast field values are stored as Montgomery UInt32 residues below KoalaBear.fieldSize, representing x * 2^32 modulo the KoalaBear prime. Addition, subtraction, and negation operate directly on Montgomery words; multiplication uses Montgomery reduction on a native UInt64 product.

def KoalaBear.Fast.modulus : UInt32

KoalaBear modulus as a native word.

def KoalaBear.Fast.modulus64 : UInt64

KoalaBear modulus as a 64-bit word for modular reduction.

def KoalaBear.Fast.rModModulus : UInt32

2^32 mod KoalaBear.fieldSize. This is the Montgomery representation of one.

def KoalaBear.Fast.r2ModModulus : UInt32

(2^32)^2 mod KoalaBear.fieldSize, used to enter Montgomery representation.

def KoalaBear.Fast.montgomeryNegInv : UInt32

-KoalaBear.fieldSize⁻¹ mod 2^32, used by Montgomery reduction.

@[reducible, inline]

abbrev KoalaBear.Fast.Field : Type

The fast native-word KoalaBear field carrier, stored as a Montgomery residue.

@[implicit_reducible]

instance KoalaBear.Fast.instDecidableEqField : DecidableEq Field

@[inline]

def KoalaBear.Fast.raw (x : Field) : UInt32

The raw Montgomery word backing a fast KoalaBear element.

@[simp]

theorem KoalaBear.Fast.modulus_toNat : modulus.toNat = fieldSize

The native UInt32 modulus agrees with the mathematical KoalaBear modulus.

@[simp]

theorem KoalaBear.Fast.modulus64_toNat : modulus64.toNat = fieldSize

The native UInt64 modulus agrees with the mathematical KoalaBear modulus.

@[inline]

def KoalaBear.Fast.montgomeryReduce (x : UInt64) : Field

Montgomery reduction of a 64-bit word. Hot bounded callers use montgomeryReduceBounded.

@[inline]

def KoalaBear.Fast.ofCanonicalNat (n : ℕ) (_h : n < fieldSize) : Field

Build a fast element from a canonical natural representative.

@[inline]

def KoalaBear.Fast.reduceUInt64 (x : UInt64) : Field

Reduce a UInt64 modulo the KoalaBear prime and return a Montgomery fast element.

def KoalaBear.Fast.zero : Field

The zero fast KoalaBear element.

def KoalaBear.Fast.one : Field

The one fast KoalaBear element.

@[inline]

def KoalaBear.Fast.ofNat (n : ℕ) : Field

Convert a natural number into fast Montgomery representation.

@[inline]

def KoalaBear.Fast.ofUInt32 (x : UInt32) : Field

Convert a 32-bit word into fast Montgomery representation.

@[inline]

def KoalaBear.Fast.ofField (x : KoalaBear.Field) : Field

Convert from the canonical ZMod KoalaBear field into fast Montgomery form.

@[inline]

def KoalaBear.Fast.ofInt (n : ℤ) : Field

Convert an integer into fast Montgomery representation.

@[inline]

def KoalaBear.Fast.toCanonicalUInt32 (x : Field) : UInt32

Convert a fast element to its canonical native-word representative.

@[inline]

def KoalaBear.Fast.toNat (x : Field) : ℕ

Convert a fast KoalaBear element to its canonical natural representative.

@[inline]

def KoalaBear.Fast.toField (x : Field) : KoalaBear.Field

Convert a fast KoalaBear element to the canonical ZMod KoalaBear field.

@[simp]

theorem KoalaBear.Fast.toNat_ofCanonicalNat (n : ℕ) (h : n < fieldSize) : toNat (ofCanonicalNat n h) = n

Converting a canonical natural representative to fast form preserves its value.

@[simp]

theorem KoalaBear.Fast.toField_ofCanonicalNat (n : ℕ) (h : n < fieldSize) : toField (ofCanonicalNat n h) = ↑n

ofCanonicalNat embeds a canonical representative into the canonical field.

@[simp]

theorem KoalaBear.Fast.toNat_reduceUInt64 (x : UInt64) : toNat (reduceUInt64 x) = x.toNat % fieldSize

Reducing a UInt64 gives the canonical natural residue modulo KoalaBear.

@[simp]

theorem KoalaBear.Fast.toField_reduceUInt64 (x : UInt64) : toField (reduceUInt64 x) = ↑x.toNat

Reducing a UInt64 agrees with casting that word into the canonical field.

@[inline]

def KoalaBear.Fast.add (x y : Field) : Field

Fast modular addition in Montgomery form.

@[inline]

def KoalaBear.Fast.neg (x : Field) : Field

Fast modular negation in Montgomery form.

@[inline]

def KoalaBear.Fast.sub (x y : Field) : Field

Fast modular subtraction in Montgomery form.

@[inline]

def KoalaBear.Fast.mul (x y : Field) : Field

Fast modular multiplication in Montgomery form.

@[inline]

def KoalaBear.Fast.square (x : Field) : Field

Fast squaring.

@[inline]

def KoalaBear.Fast.pow (x : Field) (n : ℕ) : Field

Exponentiation over the fast representation using repeated squaring.

def KoalaBear.Fast.invExponent : ℕ

Fermat exponent used for inversion in the KoalaBear prime field.

@[inline]

def KoalaBear.Fast.inv (x : Field) : Field

Inversion in Montgomery form by a fixed 4-bit Fermat chain.

@[inline]

def KoalaBear.Fast.div (x y : Field) : Field

Division through inversion and fast multiplication.

@[implicit_reducible]

instance KoalaBear.Fast.instZeroField : Zero Field

@[implicit_reducible]

instance KoalaBear.Fast.instOneField : One Field

@[implicit_reducible]

instance KoalaBear.Fast.instAddField : Add Field

@[implicit_reducible]

instance KoalaBear.Fast.instNegField : Neg Field

@[implicit_reducible]

instance KoalaBear.Fast.instSubField : Sub Field

@[implicit_reducible]

instance KoalaBear.Fast.instMulField : Mul Field

@[implicit_reducible]

instance KoalaBear.Fast.instInvField : Inv Field

@[implicit_reducible]

instance KoalaBear.Fast.instDivField : Div Field

@[implicit_reducible]

instance KoalaBear.Fast.instNatCastField : NatCast Field

@[implicit_reducible]

instance KoalaBear.Fast.instIntCastField : IntCast Field

@[implicit_reducible]

instance KoalaBear.Fast.instNatSMulField : SMul ℕ Field

@[implicit_reducible]

instance KoalaBear.Fast.instIntSMulField : SMul ℤ Field

@[implicit_reducible]

instance KoalaBear.Fast.instPowFieldNat : Pow Field ℕ

@[implicit_reducible]

instance KoalaBear.Fast.instPowFieldInt : Pow Field ℤ

@[implicit_reducible]

instance KoalaBear.Fast.instNNRatCastField : NNRatCast Field

@[implicit_reducible]

instance KoalaBear.Fast.instRatCastField : RatCast Field

@[implicit_reducible]

instance KoalaBear.Fast.instNNRatSMulField : SMul ℚ≥0 Field

@[implicit_reducible]

instance KoalaBear.Fast.instRatSMulField : SMul ℚ Field

@[simp]

theorem KoalaBear.Fast.toField_ofField (x : KoalaBear.Field) : toField (ofField x) = x

Converting from the canonical field to fast form and back is the identity.

@[simp]

theorem KoalaBear.Fast.ofField_toField (x : Field) : ofField (toField x) = x

Converting from fast form to the canonical field and back is the identity.

theorem KoalaBear.Fast.toField_injective : Function.Injective toField

The canonical-field interpretation distinguishes fast KoalaBear values.

@[simp]

theorem KoalaBear.Fast.toField_zero : toField 0 = 0

toField maps fast zero to canonical zero.

@[simp]

theorem KoalaBear.Fast.toField_one : toField 1 = 1

toField maps fast one to canonical one.

@[simp]

theorem KoalaBear.Fast.toField_add (x y : Field) : toField (x + y) = toField x + toField y

Fast addition agrees with addition in the canonical KoalaBear field.

@[simp]

theorem KoalaBear.Fast.toField_sub (x y : Field) : toField (x - y) = toField x - toField y

Fast subtraction agrees with subtraction in the canonical KoalaBear field.

@[simp]

theorem KoalaBear.Fast.toField_neg (x : Field) : toField (-x) = -toField x

Fast negation agrees with negation in the canonical KoalaBear field.

@[simp]

theorem KoalaBear.Fast.toField_mul (x y : Field) : toField (x * y) = toField x * toField y

Fast multiplication agrees with multiplication in the canonical KoalaBear field.

def KoalaBear.Fast.ringEquiv : Field ≃+* KoalaBear.Field

Ring equivalence between the fast Montgomery representation and canonical KoalaBear.Field.

@[simp]

theorem KoalaBear.Fast.ringEquiv_apply (x : Field) : ringEquiv x = toField x

Applying ringEquiv is the same as interpreting a fast value canonically.

@[simp]

theorem KoalaBear.Fast.ringEquiv_symm_apply (x : KoalaBear.Field) : ringEquiv.symm x = ofField x

Applying the inverse ringEquiv is conversion into fast Montgomery form.

@[simp]

theorem KoalaBear.Fast.toField_square (x : Field) : toField (square x) = toField x * toField x

Fast squaring agrees with multiplication by itself in the canonical field.

@[simp]

theorem KoalaBear.Fast.toField_pow (x : Field) (n : ℕ) : toField (pow x n) = toField x ^ n

Fast natural-power computation agrees with powers in the canonical field.

@[simp]

theorem KoalaBear.Fast.toField_inv (x : Field) : toField x⁻¹ = (toField x)⁻¹

Fast inversion agrees with inversion in the canonical KoalaBear field.

@[simp]

theorem KoalaBear.Fast.toField_div (x y : Field) : toField (x / y) = toField x / toField y

Fast division agrees with division in the canonical KoalaBear field.

@[simp]

theorem KoalaBear.Fast.toField_natCast (n : ℕ) : toField ↑n = ↑n

Natural casts into fast form agree with natural casts into the canonical field.

@[simp]

theorem KoalaBear.Fast.toField_intCast (n : ℤ) : toField ↑n = ↑n

Integer casts into fast form agree with integer casts into the canonical field.

@[simp]

theorem KoalaBear.Fast.toField_nsmul (n : ℕ) (x : Field) : toField (n • x) = n • toField x

Natural scalar multiplication is preserved by toField.

@[simp]

theorem KoalaBear.Fast.toField_zsmul (n : ℤ) (x : Field) : toField (n • x) = n • toField x

Integer scalar multiplication is preserved by toField.

@[simp]

theorem KoalaBear.Fast.toField_npow (x : Field) (n : ℕ) : toField (x ^ n) = toField x ^ n

Natural powers through the Pow instance are preserved by toField.

@[simp]

theorem KoalaBear.Fast.toField_zpow (x : Field) (n : ℤ) : toField (x ^ n) = toField x ^ n

Integer powers through the Pow instance are preserved by toField.

@[simp]

theorem KoalaBear.Fast.toField_nnratCast (q : ℚ≥0) : toField ↑q = ↑q

Nonnegative rational casts into fast form agree with canonical-field casts.

@[simp]

theorem KoalaBear.Fast.toField_ratCast (q : ℚ) : toField ↑q = ↑q

Rational casts into fast form agree with canonical-field casts.

@[simp]

theorem KoalaBear.Fast.toField_nnqsmul (q : ℚ≥0) (x : Field) : toField (q • x) = q • toField x

Nonnegative rational scalar multiplication is preserved by toField.

@[simp]

theorem KoalaBear.Fast.toField_qsmul (q : ℚ) (x : Field) : toField (q • x) = q • toField x

Rational scalar multiplication is preserved by toField.

@[implicit_reducible, instance 100]

instance KoalaBear.Fast.instField : _root_.Field Field

Field instance transferred from canonical KoalaBear through toField.

@[implicit_reducible, instance 100]

instance KoalaBear.Fast.instCommRing : CommRing Field

Commutative-ring instance inherited from the transferred field structure.

@[implicit_reducible, instance 100]

instance KoalaBear.Fast.instNonBinaryField : NonBinaryField Field

Fast KoalaBear is a non-binary field.