scalarMul
plain-language theorem explainer
Scalar multiplication on points of a short Weierstrass curve over ZMod p is defined recursively by repeated chord-tangent addition, returning the point at infinity for scalar zero. Recognition Science auditors and cryptographers cite this reference implementation when embedding standard ECDLP instances into RS-invariant checks. The definition proceeds by pattern matching on the natural-number scalar and delegates each step to the total pointAdd operation.
Claim. Let $E$ be a short Weierstrass curve $y^2 = x^3 + a x + b$ over the prime field $ZMod p$. The map $k, Pmapsto kP$ on $E(ZMod p)$ satisfies $0P = O$ (the point at infinity) and $(n+1)P = P + (nP)$, where $+$ is the chord-tangent group law on the curve.
background
The module supplies an explicit surface for auditing elliptic-curve discrete-log claims inside the Recognition framework. It fixes a finite carrier $ZMod p$, a short Weierstrass curve structure carrying coefficients $a,b$, the inductive type of points (infinity or affine pairs), the total chord-tangent addition, and the scalar-multiplication operation that feeds the solution predicate. ShortWeierstrassCurve is the structure whose fields are the curve coefficients; ECPoint is the inductive carrier that admits infinity as the identity. pointAdd supplies the group law with explicit cases for infinity and the usual slope formulas for affine points. The upstream E definition from SpectralEmergence records the edge count of the D-cube and is imported only for cardinality bookkeeping.
proof idea
The declaration is a recursive definition by pattern matching on the natural-number argument. The base case maps scalar 0 to ECPoint.infinity. The successor case applies pointAdd to the current point and the result of the recursive call on the predecessor scalar.
why it matters
scalarMul supplies the reference group action required by the downstream isSolution predicate that decides whether a candidate integer solves a given ECDLPInstance. It therefore lets Recognition Science invariants be tested against ordinary elliptic-curve discrete-log data without introducing an efficient implementation that might hide side-channel structure. The same operation appears in the LinearAlgebraOp enumeration, linking the cryptography surface to the linear-algebra primitives extracted from the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.