---
id: H25
title: ECDSA malleability and Schnorr correctness follow from the abstract group axioms alone (formalised)
axis: D
kind: formal
statement: 'In an axiomatised cyclic group with x(−P) = x(P): if (r, s) verifies then (r, −s) verifies; and s = k + e·d implies
  [s]G = R + [e]P.'
motivation: 'Research question B1/B4: which properties depend only on the group structure (and hence are shared by every curve)?'
assumptions: Abstract group structure fields; modular inverses as hypotheses.
expected_contribution: Machine-checked statements of two textbook facts.
related_work:
- schnorr1991efficient
- nist2023fips186
- wuille2020bip340
possible_counterexamples: None (theorems).
verification_strategy: formal/ Lean project.
computational_budget: minutes
status: evaluated
classification: known_reproduced
evidence:
- formal/README.md
- formal/build.log
- tests/test_formal_lean.py
verdict: 'Machine-checked in an axiomatised CyclicGroup structure (fields listed in formal/README.md): schnorr_correct (s
  = k + e·d mod n ⟹ s•G = R + e•P), ecdsa_correct, ecdsa_malleable ((r,s) valid ⟹ (r, n−s) valid, modular inverse as witness).
  Only propext/Quot.sound used.'
---

# H25 — ECDSA malleability and Schnorr correctness follow from the abstract group axioms alone (formalised)

In an axiomatised cyclic group with x(−P) = x(P): if (r, s) verifies then (r, −s) verifies; and s = k + e·d implies [s]G = R + [e]P.