onCurve
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.