nonsingular
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.
claimLet $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 in Recognition Science
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$.
scope and limits
- Does not verify that the chord and tangent operations satisfy the group axioms.
- Does not address the security or hardness of the discrete logarithm on the curve.
- Does not embed any phi-ladder or J-cost constructions from the Recognition framework.
- Does not handle projective coordinates or point at infinity explicitly.
formal statement (Lean)
28def nonsingular {p : ℕ} (E : ShortWeierstrassCurve p) : Prop :=
proof body
Definition body.
29 (4 : ZMod p) * E.a ^ 3 + (27 : ZMod p) * E.b ^ 2 ≠ 0
30
31/-- Projective point surface specialized to a short Weierstrass equation. -/