"Less Than 256" Is Not the Weak-Key Set: A Counterexample and a One-Sentence Correction for the ECDSA Small-Scalar Rule Proposed for the CA/Browser Forum TLS Baseline Requirements, with a Lean Proof

CA/Browser Forum servercert pull request #683 (draft ballot, 2026-10-22) adds to the TLS Baseline Requirements, Section 6.1.6, the requirement that a CA "ensure that the public key does not correspond to a Private Key whose private scalar is less than 256", following the eMudhra incident (Mozilla Bugzilla 2083449). This note shows that the sentence does not describe the set of keys the search it alludes to recovers: for k in 1..255, the scalars n - k (public key -kG, same x-coordinate as kG) and k^-1 mod n (public key Q with kQ = G) are not "less than 256", yet each is recovered at the same cost, at most 255 group operations. Both are verified against the eight real eMudhra public keys. A one-sentence correction is proposed, and in Lean 4 (core library; axioms propext and Quot.sound only; no sorry) the scalar clause is proved to hold exactly for the keys an x-only search of that size recovers; the draft clause is a strict special case. The negation family is already handled by zlint's e_ecdsa_small_private_key lint; what is new is that the ballot text, which is what a CA is audited against, does not say so, and the inverse family, which no current linter or text covers. Code (Apache-2.0) and the Lean proof reproduce every number in the note; the text is CC BY 4.0. The analysis, code and proof were produced with substantial assistance from an AI system (Claude, Anthropic), directed and checked by the author, who chose the target, decided the claims, ran the code and is responsible for the content.