Documentation

CsdLean4.Mathlib.QuantumInfo.Reversible.ModInv

Reversible modular inverse — the semantic layer (ECDLP Tranche 4) #

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate).

The modular-inverse layer of the reversible-arithmetic substrate (specs/ecdlp-resource-plan.md). The semantic target is the oracle action y ↦ y⁻¹ on ZMod N (modular inversion — the field division underlying elliptic-curve slope computation). Per the investigation map this layer is reuse: the arithmetic content is Mathlib's ZMod inverse (ZMod.mul_inv_of_unit, inv_mul_of_unit, isUnit_iff_coprime, unitOfCoprime), so this module is the thin oracle + algebra on top, and — the load-bearing increment — the reversibility connection to the multiplication oracle (Tranche 3): multiplying by a is undone by multiplying by a⁻¹, so mulConst a is a reversible permutation whose inverse is mulConst a⁻¹.

What is proved here #

Honest scope — no inversion circuit (and why that is the right call here) #

This is the semantic / algebraic layer only. A reversible circuit for modular inversion (extended Euclid) is large and is not built. This is deliberate and standard for ECDLP resource accounting: elliptic-curve point arithmetic in projective / Jacobian coordinates avoids a per-operation field inversion (one inversion at the very end, or via Fermat a⁻¹ = a^{N-2} = modular exponentiation built from the Tranche-3 multiplier). So the dominant cost is multiplications (Tranche 3, with derived gate counts), and the inversion-as-a-circuit is deferred to the EC layer's coordinate choice. What is established here is the inversion oracle and the reversibility algebra that the EC group law consumes.

source
def Reversible.modInv (N : ℕ) (a : ZMod N) :
ZMod N

The modular-inverse oracle action: y ↦ y⁻¹ on ZMod N (Mathlib's ZMod inverse).

Equations
Instances For
    source
    theorem Reversible.mul_modInv_of_unit {N : ℕ} {a : ZMod N} (h : IsUnit a) :
    a * modInv N a = 1

    For a unit a, a · a⁻¹ = 1 (reuse ZMod.mul_inv_of_unit).

    source
    theorem Reversible.modInv_mul_of_unit {N : ℕ} {a : ZMod N} (h : IsUnit a) :
    modInv N a * a = 1

    For a unit a, a⁻¹ · a = 1 (reuse ZMod.inv_mul_of_unit).

    source
    theorem Reversible.isUnit_modInv {N : ℕ} {a : ZMod N} (h : IsUnit a) :
    IsUnit (modInv N a)

    The modular inverse of a unit is a unit.

    source
    theorem Reversible.modInv_modInv {N : ℕ} {a : ZMod N} (h : IsUnit a) :
    modInv N (modInv N a) = a

    modInv is an involution on units: (a⁻¹)⁻¹ = a. So as a permutation of the units, the modular-inverse oracle is its own inverse.

    source
    theorem Reversible.modInv_isUnit_iff_coprime {N : ℕ} (m : ℕ) :
    IsUnit ↑m ↔ m.Coprime N

    The unit ⇔ coprimality bridge: (m : ZMod N) is invertible iff m is coprime to N (reuse ZMod.isUnit_iff_coprime). The admissibility condition for a modular inverse to exist.

    Reversibility: the multiplication oracle is inverted by mulConst at the modular inverse #

    source
    theorem Reversible.mulConst_modInv_leftInverse {N : ℕ} {a : ZMod N} (h : IsUnit a) (y : ZMod N) :
    mulConst N (modInv N a) (mulConst N a y) = y

    mulConst a⁻¹ left-inverts mulConst a (for a unit a): multiplying by a then by a⁻¹ recovers y. So the reversible circuit realising mulConst a (Tranche 3) is undone by the one for mulConst a⁻¹.

    source
    theorem Reversible.mulConst_modInv_rightInverse {N : ℕ} {a : ZMod N} (h : IsUnit a) (y : ZMod N) :
    mulConst N a (mulConst N (modInv N a) y) = y

    mulConst a⁻¹ right-inverts mulConst a (for a unit a).

    source
    theorem Reversible.mulConst_modInv_bijective {N : ℕ} {a : ZMod N} (h : IsUnit a) :
    Function.Bijective (mulConst N a)

    The multiplication oracle mulConst a is a bijection for a unit a, with explicit inverse mulConst a⁻¹ — the reversibility witness underlying its reversible-circuit realisation. Strengthens ModMul.mulConst_bijective (which proves bijectivity without exposing modInv as the inverse) by threading mulConst (modInv a) as the two-sided inverse the EC layer consumes.