PublicECDLPData
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not encode the secret scalar k satisfying Q = kP.
- Does not assert the hardness of recovering k.
- Does not restrict the prime p or the curve parameters beyond the listed fields.
- Does not include any Recognition Science cost or J-function data.
formal statement (Lean)
112structure PublicECDLPData (p : ℕ) where
113 curve : ShortWeierstrassCurve p
114 base : ECPoint p
115 target : ECPoint p
116 order : ℕ
117 cofactor : ℕ
118 family : CurveFamily
119
120def ECDLPInstance.publicData {p : ℕ} (inst : ECDLPInstance p) : PublicECDLPData p where
121 curve := inst.curve
proof body
Definition body.
122 base := inst.base
123 target := inst.target
124 order := inst.order
125 cofactor := inst.cofactor
126 family := inst.family
127
128/-- A watch invariant is admissible only if it is computed from public data. -/