writing-lean-proofs: eval fixtures are never compiled, and two of them do not build

Follow-up to #226. The writing-lean-proofs eval fixtures are deliberately not compiled (evals/README.md: "Fixtures are not compiled — no Lean toolchain is needed"), which is a reasonable default: the planted flaws are stylistic and reviewable from source. But two fixtures carry claims that only a compiler can check, and both are currently wrong.

1. 04-structural: carry_le_one states a goal its tactic cannot close

evals/cases/04-structural/input/U32Pairs.lean:33-38

theorem carry_le_one (a b : Nat) (h : U32Pair a b) : carry a b ≤ 1 := by
  obtain ⟨ha, hb⟩ := h
  simp only [carry, Nat.div_le_iff_le_mul_add_pred, ...]

ha hb : _ < 2^32 are in context but the simp only list uses neither, and (a + b) / 2 ^ 32 ≤ 1 is false without them — take a = b = 2^40. So the tactic cannot close the goal.

This is not just dead weight, it distorts the rubric. rubric.md:38-43 scores the reviewer on flagging a squeezed terminal simp. A strong reviewer says the more important thing first — "this proof never uses the bounds, so it doesn't establish the goal" — and may not separately frame it as a style problem, failing the criterion for being more correct. And the fix the criterion asks for ("propose a plain terminal simp") also cannot close the goal, since bare simp does not consult hypotheses.

2. 04-structural: mod_add_carry_mul's premise is unverified

evals/cases/04-structural/input/U32Pairs.lean:40-43

  simp [carry]
  omega

Nat.mod_add_div is a simp lemma and the goal shape is close, so if simp closes the goal outright the file does not compile at all (omega: "no goals"). The bare-nonterminal-simp criterion (rubric.md:45-50) asks the reviewer to flag a non-terminal simp — but whether a tactic genuinely follows the simp is exactly what is unchecked.

3. 05-clean-restraint has criticizable code the rubric doesn't shield

evals/cases/05-clean-restraint/input/Carry.lean:16-20

carry_zero_left / carry_zero_right are @[simp] with side conditions (hb : b < 2 ^ 32) that simp must discharge at every use site. That is a defensible thing to raise, and the skill's own discharge-depth guidance would prompt it. The case is the "deliberately good file" — its rubric protects terminal simp, show lines and the rfl def lemma, but not this. A skill-arm review that raises it substantively risks reading to the judge as "manufacturing a list of style violations" and failing overall-verdict.

Suggested fix

Per evals/README.md's own rule — fix the fixture, not the rubric:

• Compile all five case fixtures once by hand against the pinned Mathlib and correct what does not build. A one-shot lake env lean pass, not a toolchain dependency for the suite.
• Make carry_le_one actually provable from ha/hb while keeping the squeezed-terminal-simp flaw intact.
• Confirm mod_add_carry_mul's simp [carry] genuinely leaves a goal for omega.
• Either add a must-not-flag for the conditional @[simp] lemmas in case 05, or make them unconditional.
• Consider a lightweight CI job that compiles fixtures against pinned Mathlib, so this cannot regress silently.

Raised by the deep review on #226 (P3/P4). Not merge-blocking: it can skew individual criterion scores, but does not affect the harness's correctness or the skill content.