isSolution
The predicate declares that a natural number k solves an elliptic curve discrete logarithm instance precisely when k is strictly smaller than the instance order and repeated addition of the base point k times recovers the target point. Cryptographers or Recognition Science auditors testing invariants against standard discrete-log hardness would cite this definition to keep the problem statement explicit and free of hidden structure. It is realized as a direct conjunction of the order bound and the scalar-multiplication equality.
claimLet $p$ be a natural number and let $I$ be an elliptic-curve discrete-logarithm instance consisting of a short Weierstrass curve $E$, base point $P$, target point $Q$, and order $n$. Then $k$ is a solution for $I$ if and only if $k < n$ and the scalar multiple $kP$ equals $Q$, where scalar multiplication is the iterated chord-tangent group operation on $E$.
background
The module supplies a minimal, auditable surface for the elliptic-curve discrete-logarithm problem so that Recognition Science invariants can be applied without concealed hypotheses. Its central data structure packages a short Weierstrass curve over the field with $p$ elements, a base point, a target point, the order, a cofactor, and a curve-family tag, together with the proofs that the curve is nonsingular and both points lie on the curve. Scalar multiplication is the reference recursive definition obtained by repeated point addition, returning the point at infinity for the zero multiplier.
proof idea
The definition is a direct conjunction of two atomic conditions: the strict inequality $k <$ instance order and the equality obtained by applying the scalar-multiplication function to the base point. No lemmas are invoked; the body simply assembles the order bound with the result of the upstream scalarMul definition.
why it matters in Recognition Science
This predicate supplies the concrete solution concept required before any Recognition Science invariant (J-cost, defect distance, or phi-ladder bound) can be imposed on an ECDLP instance. It is the direct analogue of the solution predicate in the balanced J-subset-sum module, which likewise demands a weight target, a residue condition, and a J-cost bound. The surrounding module exists precisely to keep later invariants honest by restricting them to the public fields of the instance structure, consistent with the program of making every mathematical surface explicit before deriving physical consequences from the single functional equation.
scope and limits
- Does not implement or analyze any algorithm for recovering the discrete logarithm.
- Does not assert computational hardness or easiness for any concrete curve or field size.
- Does not invoke the J-function, the Recognition Composition Law, or the phi-ladder.
- Does not supply security reductions, attack bounds, or complexity statements.
formal statement (Lean)
107def isSolution {p : ℕ} (inst : ECDLPInstance p) (k : ℕ) : Prop :=
proof body
Definition body.
108 k < inst.order ∧ scalarMul inst.curve k inst.base = inst.target
109
110/-- Public data available to an adversary. This structure exists to keep later
111RS invariants honest: they may depend only on these fields. -/