Module field_algebra 

Kernel algebra for the prime field 𝔽_q of ML-KEM / ML-DSA — the certified arithmetic substrate (F2 seed).

Every identity here is discharged by the kernel’s OWN decision procedures — the ring canonicalizer for polynomial identities (which hold for ALL values, not a ≤16-bit sample), and Fourier-Motzkin lia for the modular-reduction range bounds — with no Z3. This is the layer the NTT’s correctness and its symmetry-derived speed rewrites build on: a rewrite that cuts multiplies (or collapses a symmetric butterfly) is only safe once the kernel certifies it computes the same polynomial.

Constants

KYBER_Q

Kyber / ML-KEM’s modulus — prime, so ℤ/qℤ is the field 𝔽_q.

MLDSA_MONT_R

Montgomery radix R = 2³² and qinv = q⁻¹ mod R = 58728449 (the SUBTRACT convention: the reduction is redc(a) = (a − ((a·qinv) mod R)·q) / R, matching mldsa::montgomery_reduce). The exact integer cofactor (qinv·q − 1) / R makes the numerator a clean multiple of R.

MLDSA_Q

Dilithium’s modulus — prime, so ℤ/qℤ is the field 𝔽_q.

MLDSA_QINV

MONT_R

Montgomery radix R = 2¹⁶ and qinv' = −q⁻¹ mod R = 3327, with the exact integer cofactor (qinv'·q + 1) / R = 169. These are the constants of the division-free reduction redc(x) = (x + ((x·qinv') mod R)·q) / R used by the (SIMD) ML-KEM NTT.

NEG_QINV_MOD_R

Functions

conditional_subtract_in_range

Certify that conditional-subtract reduction keeps a modular-ADD result in range. After an addition in 𝔽_q the value a lies in [0, 2q); the reduction is csub(a) = if a ≥ q { a − q } else { a }, and the result must lie in [0, q). The two non-trivial bounds (the a ≥ q branch) are discharged by Fourier-Motzkin: a goal is valid iff its negation’s constraints are UNSAT.

gauss_three_multiply_identity

Gauss’s three-multiplication identity — the symmetry that turns a 4-multiply bilinear form ad + bc into 3 multiplies (a+b)(c+d) − ac − bd. It is the archetypal “spend an add to save a multiply” rewrite behind fast complex / polynomial / NTT-butterfly multiplication. Certified as a polynomial identity over any commutative ring by the kernel’s ring canonicalizer, so a codegen pass may apply it knowing it is sound.

mldsa_montgomery_congruence

Certify the ML-DSA Montgomery CONGRUENCE: (a − lo·q) − a = −q·lo, so the reduction numerator redc·R = a − lo·q differs from a by a multiple of q ⇒ redc·R ≡ a (mod q) ⇒ redc ≡ a·R⁻¹ (mod q). A ring identity in the free variables a, lo, certified for all values.

mldsa_montgomery_divisibility

Certify the ML-DSA Montgomery DIVISIBILITY: a·qinv·q − a = cofactor·R·a, i.e. the reduction’s numerator a − (a·qinv)·q = −cofactor·R·a is an EXACT multiple of R (so /R is a shift, never a rounding divide). This holds because qinv·q ≡ 1 (mod R); the ring canonicalizer reduces both sides to a·(qinv·q − 1), certifying it for ALL a.

mldsa_montgomery_reduction_certified

The full ML-DSA Montgomery reduction is kernel-certified: the numerator is an exact multiple of R (divisibility) and the result is a·R⁻¹ mod q (congruence). Together these prove mldsa::montgomery_reduce — hence the AVX2 montmul32 that shares its formula — computes the right field element, with no Z3, for ALL inputs (not a sampled bit-width).

montgomery_reduction_certified

The full Montgomery reduction is kernel-certified: the constant divides exactly (so /R is a shift), the result is x·R⁻¹ mod q (congruence), and the final conditional subtract keeps it in [0, q) (range). A single gate over the three procedures.

montgomery_reduction_congruence

Certify the Montgomery CONGRUENCE: (x + lo·q) − x = q·lo, so the reduction numerator differs from x by a multiple of q ⇒ redc·R ≡ x (mod q) ⇒ redc ≡ x·R⁻¹ (mod q) (R is a unit in 𝔽_q). A ring identity in the free variables x, lo, certified for all values.

montgomery_reduction_divisibility

Certify the Montgomery DIVISIBILITY: x + (x·qinv')·q = x·169·R, i.e. the reduction’s numerator (with the un-reduced lo = x·qinv') is an EXACT multiple of R — so redc’s / R is an exact shift, never a rounding division. This is what makes qinv' = 3327 the RIGHT constant (qinv'·q ≡ −1 mod R): the kernel ring canonicalizer reduces both sides to x·11075584, certifying it for ALL x, not a sampled width.