nonsingular
plain-language theorem explainer
The nonsingular predicate on a ShortWeierstrassCurve over ZMod p requires the discriminant 4a³ + 27b² to be nonzero in that field. Analysts checking elliptic-curve discrete-log instances cite the predicate to confirm the curve equation defines a valid elliptic curve. The body is a direct algebraic inequality on the curve parameters a and b.
Claim. Let $E$ be a short Weierstrass curve over the field $ZMod p$ given by the equation $y^2 = x^3 + a x + b$. The curve $E$ is nonsingular precisely when $4a^3 + 27b^2 ≠ 0$ holds in $ZMod p$.
background
The module defines a minimal explicit surface for auditing elliptic-curve discrete logarithm claims. It fixes a finite carrier $ZMod p$, a short Weierstrass curve, points including infinity, the chord-tangent group operation, scalar multiplication, and an ECDLP solution predicate, all before any Recognition Science invariant is tested. ShortWeierstrassCurve is the structure holding coefficients $a$ and $b$ such that the equation is $y^2 = x^3 + a x + b$ over $ZMod p$. The nonsingular condition is the classical algebraic requirement that this curve be nonsingular.
proof idea
The definition is a one-line algebraic expression that computes the discriminant $4a^3 + 27b^2$ and asserts its nonvanishing in $ZMod p$.
why it matters
This definition supplies the validity condition for curves inside ECDLPInstance structures. It appears in the cryptography module that prepares the discrete-log problem for subsequent Recognition Science checks. The parent structure ECDLPInstance collects curve, base point, target, order, and cofactor to pose the recovery of $k$ from $Q = kP$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.