1---2id: H253title: ECDSA malleability and Schnorr correctness follow from the abstract group axioms alone (formalised)4axis: D5kind: formal6statement: 'In an axiomatised cyclic group with x(−P) = x(P): if (r, s) verifies then (r, −s) verifies; and s = k + e·d implies7 [s]G = R + [e]P.'8motivation: 'Research question B1/B4: which properties depend only on the group structure (and hence are shared by every curve)?'9assumptions: Abstract group structure fields; modular inverses as hypotheses.10expected_contribution: Machine-checked statements of two textbook facts.11related_work:12- schnorr1991efficient13- nist2023fips18614- wuille2020bip34015possible_counterexamples: None (theorems).16verification_strategy: formal/ Lean project.17computational_budget: minutes18status: evaluated19classification: known_reproduced20evidence:21- formal/README.md22- formal/build.log23- tests/test_formal_lean.py24verdict: 'Machine-checked in an axiomatised CyclicGroup structure (fields listed in formal/README.md): schnorr_correct (s25 = 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).26 Only propext/Quot.sound used.'27---2829# H25 — ECDSA malleability and Schnorr correctness follow from the abstract group axioms alone (formalised)3031In 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.32