fix: prove the valuations submodule closure fields in Hadwiger

[Vilin97]

Problem

hadwiger is currently unsolvable by construction: no submission — including a completely valid, sorry-free formalization of Hadwiger's theorem — can be accepted by the comparator.

The fixed (non-hole) definition valuations in LeanEval/ConvexGeometry/Hadwiger.lean shipped its three Submodule membership-closure fields as sorry:

noncomputable def valuations (n : ℕ) : Submodule ℝ (ConvexBody (E n) → ℝ) where
  carrier := {f | IsValuation f}
  add_mem' := by sorry
  zero_mem' := by sorry
  smul_mem' := by sorry

The target theorem's type is Module.finrank ℝ (valuations n) = n + 1, so every accepted declaration with the required type has valuations — and therefore sorryAx — in its transitive dependency closure, regardless of what the submitted proof term looks like. The comparator's recursive axiom check walks type-and-value dependencies and rejects any axiom outside permitted_axioms (propext, Quot.sound, Classical.choice), so every submission fails. There is no submission-side workaround: the type is fixed by Solution.lean, and LeanEval.ConvexGeometry.valuations cannot be redeclared. (This is the same defect class that was repaired for the Conway knot problems in #372.)

Fix

Prove the three closure fields in the trusted source (they are routine: continuity is preserved by +/•, each invariance clause is preserved pointwise, and the inclusion–exclusion identity is linear in f), drop the now-stale "left as sorry" wording from the module docstring and manifest notes, and regenerate the generated/hadwiger workspace.

The statement surface is untouched: E, IsValuation, the valuations carrier, and the hadwiger target statement are all byte-identical. Only the three proof fields (Prop-valued, proof-irrelevant) gained real proofs. Deliberately not adding valuations to the holes: making it solver-replaceable would let a submission swap in a different submodule of the same type whose rank is trivially n + 1, destroying the mathematical content of the target.

Verification

• lake build LeanEval.ConvexGeometry.Hadwiger — clean; the only remaining sorry warning is the @[eval_problem] target theorem itself.
• #print axioms LeanEval.ConvexGeometry.valuations (both in the source tree and inside the regenerated workspace against ChallengeDeps):
  [propext, Classical.choice, Quot.sound] — exactly the permitted set, no sorryAx.
• lake build in generated/hadwiger succeeds; ChallengeDeps builds with no sorry warnings (previously the tainted valuations warned there). The only sorry warnings are the intentional holes (Challenge.lean statement, solver placeholder in Submission.lean).
• lake exe lean-eval validate-manifest and lake exe lean-eval check-problem-build pass.

Possible follow-up (not in this PR)

check-problem-build tolerates all "declaration uses sorry" warnings because target holes legitimately contain sorry. A generation-time audit that walks the trusted (non-hole) declarations of each generated workspace and rejects sorryAx there would have caught this class of bug (Hadwiger here, Conway knots in #372) before publication.

🤖 Generated with Claude Code