onCurve
Defines the predicate checking whether a point satisfies the Weierstrass equation on a short Weierstrass curve over Z/pZ, treating the point at infinity as always valid. Researchers constructing explicit ECDLP test cases within the Recognition Science auditing surface would reference this predicate. The definition is given directly by cases on the point constructors.
claimLet $E$ be given by coefficients $a,b$ so that the curve equation is $y^2 = x^3 + a x + b$ over the field $Z/pZ$. For a point $P$, the predicate holds when $P$ is the identity element at infinity or, for an affine point $(x,y)$, the equality $y^2 = x^3 + a x + b$ is satisfied.
background
The module supplies a minimal explicit surface for elliptic-curve discrete-logarithm problems so that Recognition Science invariants can be tested against ordinary mathematical statements. It introduces the short Weierstrass curve as the structure carrying coefficients $a$ and $b$, together with the inductive type of points consisting of the distinguished infinity element and affine pairs drawn from $ZMod p$. The upstream edge-count definition from the D-cube is imported at the module level but plays no role in the predicate.
proof idea
The declaration is a direct definition by pattern matching on the inductive point type. The infinity constructor is mapped to the constant true proposition. The affine constructor is mapped to the concrete cubic equation that uses the curve coefficients $a$ and $b$.
why it matters in Recognition Science
The predicate is a prerequisite for the ECDLPInstance structure that packages a curve, base point, target point, order and cofactor. It therefore supports the module's stated purpose of rendering the ordinary ECDLP precise before any Recognition Science candidate invariant is applied. No connection is made to the forcing chain, the Recognition Composition Law, or the phi-ladder constants.
scope and limits
- Does not define or prove the chord-tangent group law.
- Does not address hardness of the discrete logarithm.
- Does not enforce the discriminant-nonzero condition.
- Does not invoke any Recognition Science constants or forcing steps.
formal statement (Lean)
38def onCurve {p : ℕ} (E : ShortWeierstrassCurve p) : ECPoint p → Prop
39 | ECPoint.infinity => True
40 | ECPoint.affine x y => y ^ 2 = x ^ 3 + E.a * x + E.b
41
42/-- Negation in the elliptic-curve group law. -/