ShortWeierstrassCurve
ShortWeierstrassCurve packages the two coefficients a and b that define an elliptic curve in short Weierstrass form over the prime field ZMod p. Cryptographers setting up ECDLP instances inside the Recognition Science watch module cite this structure to fix the curve equation before any group-law or discrete-log predicates are stated. The declaration is a bare structure with two fields and carries no proof obligations or computational content.
claimA short Weierstrass curve over the finite field $ZMod p$ is given by the pair of coefficients $(a,b)$ with $a,b : ZMod p$, so that the affine equation reads $y^2 = x^3 + a x + b$.
background
The ECDLP Watch Surface module supplies a minimal, explicit carrier for auditing elliptic-curve discrete-logarithm claims. It fixes a prime-field carrier ZMod p, admits the point at infinity, equips the curve with the chord-tangent addition law, and defines scalar multiplication together with an ECDLP solution predicate. All later structures and functions in the module are built on top of this curve data type.
proof idea
Direct structure declaration that introduces the two fields a and b of type ZMod p. No lemmas or tactics are invoked; the declaration itself is the complete definition.
why it matters in Recognition Science
ShortWeierstrassCurve is the root data type for the entire ECDLPWatch module. It is referenced by ECDLPInstance, PublicECDLPData, nonsingular, onCurve, pointAdd, scalarMul and tangentSlope, thereby supplying the concrete curve parameters required before any RS candidate invariant can be tested against an ordinary ECDLP instance. The module sits downstream of UniversalForcingSelfReference.for, whose meta-realization certificate records the structural properties needed to embed the curve inside the forcing-chain framework.
scope and limits
- Does not impose the discriminant nonvanishing condition.
- Does not define the group law or point addition formulas.
- Does not attach any Recognition Science cost or invariant.
- Does not restrict the prime p beyond being a natural number.
formal statement (Lean)
23structure ShortWeierstrassCurve (p : ℕ) where
24 a : ZMod p
25 b : ZMod p
26
27/-- Discriminant nonvanishing condition for `y^2 = x^3 + ax + b`. -/