Structural Code Generation: Exact Decoding Sieves, a Read-Only Symbol Memory, and Verifier Certificates

Code models emit syntax errors, invented identifiers and insecure constructs. We ask how much of this can be guaranteed away, and how much can only be measured, under a protocol where every criterion was logged before the measurement it governs. Rice's theorem bounds the promise: only properties decidable on the prefix can be enforced at generation time; semantic properties need an external verifier. We build the three corresponding stages around one open 1.5B code model (Qwen2.5-Coder-1.5B) and test each against a pre-registered prediction. (1) Exact decoding sieves: a witness oracle admits a prefix only if it exhibits a completion accepted by the interpreter, and Gumbel ranking makes masking exact and lazy. On 10,200 generations per arm at temperature 1, no output left the language and none referenced an unresolved identifier, with no blocking. On HumanEval and MBPP (421 tasks, 15 samples each), syntax validity rises from 96.75% to 100% and invented identifiers fall from 2.08% to 0% at no cost in pass@1 (49.31% to 49.56%; paired gain +0.25 points). (2) A read-only symbol memory, the exact limit of a Casimir attention score, is exact and O(1) on 1,049,524 lines, but on repository-level completion up to RepoBench's 128k level it does not beat embedding retrieval (paired difference +0.000): the prediction is falsified. (3) Verifier certificates: syntactic safety patterns removed every flagged instance of the classes they name (25/389 insecure samples without, 0/375 with), while a CodeQL feedback loop reduced the other classes by only 21% (predicted: half); with Dafny, the certified fraction went from 3.2% in one round to 3.5% within five (predicted: double). We report two validation-gate failures that found real bugs, every falsified prediction, and the limits of each guarantee. Files: preprint, code, tests, the complete pre-registration log and the measurement files from which every number is generated. Every number in the paper is generated from the measurement files (python paper/make_assets.py); PLAN_STATUS.md is the complete, dated pre-registration log. RepoBench-derived text is removed from the archive (CC BY-NC-ND licence); see the archive README.