[v0.4] Text and coverage left from the v0.4 train's member reviews (follow-up to #167) #182

Follow-up to #167. These items were raised on the member PRs and are not on f1e1157. None changes compiler records.

• SPEC §17.17, certificate B: "2.4 KB of each certificate B" (SPEC.md:5003), program and crate terms "noncomputable" (:5024; they are not compiled), the B checking times measured on text certificates, and the two reasons given for the missing module header.
• COSTS_B: record how it was derived (SPEC.md:4923 says half of the greatest; the review found the text-era costs divided by four). State in SP-02 that a mixed shape fitting at full scale 256 gets no edge check (cases/preservation.rs:425).
• fix(backend): lower explicit shared byte literals without widening limits #68:
  • The binder-hygiene rule (SPEC.md:2777) still says byte literals are written without qualification; they use _root_. names and bind __byteN.
  • The VERIFICATION measurements describe a scratch file at Lean's default limits, not generated modules (semantic.rs sets maxRecDepth 100000).
  • "MD-02 applies the same reader" is false (models.rs:541-594; 2 of 6 *.bytes definitions checked).
• feat(models): decode IEEE-754 bit patterns as exact dyadic rationals (MD-13, #118) #150:
  • dyadicRoundShift (examples/models/src/Recognizer.lex.tex:356) ignores the done flag of iterate_until and returns a wrong value when exponent plus shift exceeds 512. Return Option, or delete it with the unused dyadicMul.
  • decodeBinary64's unsigned branch is untested.
  • CHANGELOG says "43 theorems (39 + 4)"; there are 47.
  • The skewed-oracle plant's output is "..." in VERIFICATION.md.
• Capacity: CHANGELOG says that, with certificate A as data, a pair of match arms costs about 5.7 times its text cost (1018 against 180 sixteenths), so the widest match that fits the default max_file_bytes falls from about 420 to 240 constructors (SP-02, SPEC §17.17), and that a project with a wider match raises max_file_bytes.
• feat(semantic-ir): byte and fixed-width widening conversions in language 1.2 (SM-32, #114) #151:
  • Add a production root over UInt64/Int64 with an input that reaches to_int's overflow at or above 2^63.
  • SPEC §17.12 rule 2 should say that overflow happens.

Definition of done: each bullet is fixed or answered on this issue; just vv green.

Generated by Claude Code