Machine-checked specification defects in a post-quantum construction: a case study in literal-first formalisation

A case study in literal-first formalisation: the algebraic core of a post-quantum construction (VWZ, Kyber-style over F_3329) was transcribed into Isabelle/HOL with one rule - transcribe the specification as written, and allow restatement only after the machine rejects the original sentence. The result is not a security proof. It is a register of four specification defects: an arithmetic domain mismatch (T2_B3), a dimension-convention mismatch (T2_D4), a missing rank premise (T2_B7), and a statement whose free variables force two different messages to produce identical target bits (T2_D5). Three are closed. T2_B7 was refuted by an explicit counterexample, restated with the missing non-zero-minor premise, and then proved: rank is at most 2 because every row lies in a two-vector span, and at least 2 because a non-zero 2x2 minor forces it. T2_D5 is false as written; because the relevant function is an uninterpreted constant, the refutation is a logical derivation rather than a computed witness, and the obligation has no consumer anywhere in the development. The development contains 20 Isabelle theories, 582 lemmas, and 56 ledger obligations with 6 registered sorry steps (0 outside the ledger). These are tracked-file counts (git ls-files); an untracked theory backup left in a working tree inflates them. Reproduction requires Isabelle2025-2; build time is 33-41 s on the author's machine. Scope and limits: no claim is made about the security of the construction, about any implementation, or about transcription fidelity. The ledger records which obligations are discharged, not that the construction is correct. The accompanying dependency-chain check with quick_and_dirty disabled rules out hidden sorry steps in the compiled chain; it is not a full independent proof-term audit. Artifact: the Isabelle sources and the two write-ups (a short README and a long report) are in the GitHub repository at the v1.0.1 tag, licensed Apache-2.0. Every number quoted here was measured at commit d984b77 (2026-10-24). Version 1.0.1 corrects the LICENSE file in the archive, which carried the GPLv3 text in v1.0.0 even though README and every Isabelle source header declared Apache-2.0. No theory or code changed.