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.