chordSlope
plain-language theorem explainer
Defines the slope of the chord joining two distinct affine points on an elliptic curve over the prime field Z/pZ. Cryptographers formalizing ECDLP instances cite it when encoding the group law for discrete-log audits. The definition is a direct one-line expression that multiplies the y-difference by the modular inverse of the x-difference.
Claim. For distinct affine points with coordinates $(x_1,y_1)$ and $(x_2,y_2)$ in the field $Z/pZ$, the chord slope is $(y_2-y_1)(x_2-x_1)^{-1}$.
background
The ECDLP Watch module supplies a minimal, explicit surface for stating elliptic-curve discrete-log problems over a prime field. It fixes a finite carrier ZMod p, a short Weierstrass curve, affine points together with the point at infinity, and the chord-tangent addition rule that turns the curve into an abelian group. The present definition supplies the slope term that appears in the addition formula whenever the two input points have distinct x-coordinates. Upstream, the point construction from interval arithmetic supplies a basic singleton interval, while the forcing structure records the meta-realization axioms that the surrounding Recognition Science framework requires for self-referential consistency.
proof idea
One-line definition that applies the subtraction and multiplicative inverse operations already present in the field ZMod p.
why it matters
The definition is the algebraic kernel of the point-addition operation that appears in the ECDLP instance predicate. It therefore sits inside the chord-tangent group law used to make the discrete-log problem mathematically precise before any Recognition Science invariant (J-cost, phi-ladder, or eight-tick octave) is tested against it. The parent pointAdd definition consumes this slope directly when both points are affine and their x-coordinates differ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.