pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Cryptography.ECDLPWatch

show as:
view Lean formalization →

The ECDLPWatch module defines short Weierstrass elliptic curves over ZMod p together with their group law and scalar multiplication to support ECDLPInstance objects. It supplies the algebraic primitives for discrete-log problems inside the Recognition Science cryptography layer while importing the Cost module for resource tracking. The module contains only definitions and type declarations with no theorems or proofs.

claimThe central object is the short Weierstrass curve $y^2 = x^3 + a x + b$ over the field $ZMod p$, equipped with the elliptic-curve point group law, negation, chord and tangent slopes, point addition, and scalar multiplication.

background

This module sits in the cryptography domain and imports IndisputableMonolith.Cost to attach J-cost accounting to curve operations. ShortWeierstrassCurve encodes the equation $y^2 = x^3 + a x + b$ over $ZMod p$, nonsingular enforces the discriminant condition that yields an abelian group, and ECPoint is the type of affine points on the curve. The sibling definitions supply negation, chordSlope, tangentSlope, slopeAddPoint, pointAdd, scalarMul, CurveFamily, and ECDLPInstance, all built on the imported Cost framework.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the elliptic-curve primitives that feed into ECDLPInstance constructions and higher cryptography results in the Recognition Science framework. It links finite-field curve arithmetic to the J-cost structures imported from the Cost module, providing the base layer for discrete-log hardness arguments without depending on the T0-T8 forcing chain or phi-ladder directly.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (17)