PublicECDLPData
plain-language theorem explainer
Public data for an elliptic curve discrete logarithm problem consists of the curve equation, base and target points, group order, cofactor, and a family tag. Researchers testing Recognition Science invariants against ECDLP would reference this structure to enforce that invariants use only information available to an adversary. It is realized as a record whose constructor simply copies the corresponding fields from a full ECDLP instance.
Claim. Let $p$ be a natural number. A public ECDLP datum over the prime field $Z/pZ$ comprises a short Weierstrass curve $E: y^2 = x^3 + a x + b$, base point $P$, target point $Q$, the order $n$ of the base point, a cofactor $h$, and a curve-family classifier.
background
The module establishes an explicit surface for auditing elliptic-curve discrete-logarithm claims prior to any Recognition Science invariant test. A short Weierstrass curve is given by the equation $y^2 = x^3 + a x + b$ with coefficients in $Z/pZ$. Points on the curve are either the point at infinity or affine pairs $(x, y)$ satisfying the equation. The curve family tag distinguishes toy, anomalous, supersingular, and other classes relevant to known attacks.
proof idea
The structure is introduced by a direct record declaration. The accompanying projection function ECDLPInstance.publicData is a one-line wrapper that extracts the six public fields from a complete ECDLPInstance.
why it matters
This definition supplies the admissible input type for the PublicInvariant structure, which requires any watch score to be computed solely from public data. It thereby enforces honesty in later Recognition Science checks on ECDLP instances. The construction sits inside the ECDLP Watch Surface module whose purpose is to make the ordinary mathematical problem precise before testing candidate invariants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.