pith. sign in
module module moderate

IndisputableMonolith.Cryptography.ECDLPWatch

show as:
view Lean formalization →

The ECDLPWatch module defines short Weierstrass elliptic curves over ZMod p together with point addition, scalar multiplication, and ECDLP instances. Cryptographers formalizing discrete-log hardness would reference these structures when embedding elliptic-curve groups into cost analyses. The module consists entirely of inductive type definitions and basic operations with no theorems proved.

claimThe short Weierstrass curve is the set of points satisfying $y^2 = x^3 + a x + b$ over the field $ZMod p$, equipped with the chord-and-tangent group law, scalar multiplication, and an ECDLPInstance type that packages a base point and target for the discrete-logarithm search.

background

The module imports Mathlib for algebraic structures and IndisputableMonolith.Cost for cost accounting. Its central definition is the short Weierstrass curve equation $y^2 = x^3 + a x + b$ over a prime field, together with the types ECPoint, onCurve, pointAdd, scalarMul, CurveFamily, and ECDLPInstance that appear among its sibling declarations. These objects supply the concrete algebraic setting in which elliptic-curve discrete-logarithm problems are posed inside the Recognition Science framework.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the elliptic-curve primitives that any later cryptographic cost or hardness argument would invoke. It sits directly above the Cost module and provides the ECDLPInstance and scalarMul objects needed for downstream protocol or complexity statements, although no used_by edges are recorded yet.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (17)