tangentSlope
plain-language theorem explainer
The tangentSlope definition supplies the algebraic expression for the slope of the tangent line at an affine point on a short Weierstrass elliptic curve over a prime field. It is cited by any implementation of the chord-and-tangent group law when performing point doubling. The definition is a direct transcription of the standard derivative formula obtained from implicit differentiation of the curve equation.
Claim. Let $E$ be the short Weierstrass curve $y^2 = x^3 + a x + b$ over the field $Z/pZ$. For an affine point $(x, y)$ on $E$, the tangent slope is $(3x^2 + a) / (2y)$.
background
This definition sits inside the ECDLP Watch module, whose purpose is to construct an explicit finite-field elliptic curve group so that discrete-logarithm claims can be stated precisely before any Recognition Science invariant is tested. The ShortWeierstrassCurve structure encodes the equation $y^2 = x^3 + a x + b$ over $Z/pZ$. The module imports foundational material on primitive distinctions and spectral emergence, but the immediate dependency for this definition is the curve structure itself.
proof idea
The definition is a direct one-line transcription of the standard tangent-slope formula. Implicit differentiation of $y^2 = x^3 + a x + b$ gives $2y y' = 3x^2 + a$, hence $y' = (3x^2 + a) (2y)^{-1}$. The expression is written in the prime field using the modular inverse of $2y$.
why it matters
tangentSlope is invoked by the pointAdd definition that realizes the full chord-tangent group law. It therefore supports the ECDLPInstance predicate, allowing the ordinary elliptic-curve discrete-log problem to be formulated exactly before any Recognition Science candidate invariant (J-cost, phi-ladder, etc.) is applied. The module's stated goal is to make the mathematical problem precise prior to testing such invariants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.