chordSlope
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not apply when the two x-coordinates are equal.
- Does not treat the point at infinity.
- Does not enforce the short Weierstrass equation or nonsingularity.
- Does not special-case fields of characteristic two or three.
formal statement (Lean)
51def chordSlope {p : ℕ} (x₁ y₁ x₂ y₂ : ZMod p) : ZMod p :=
proof body
Definition body.
52 (y₂ - y₁) * (x₂ - x₁)⁻¹
53
54/-- Tangent slope for point doubling. -/