W1-7: Review Wave 1 for Lean idiomaticity

[arademaker]

Description

Persona: Leonardo de Moura (Lean Critic)

Final review of all Wave 1 code for Lean 4 idiomaticity. This is a gate — Wave 1 is not complete until this review passes.

Review checklist

• Naming conventions: Follow Mathlib style (camelCase for defs, snake_case for theorems)
• Type design: Are we using dependent types effectively? Any unnecessary Nat where Fin or BitVec would be better?
• Tactic style: Are proofs clean? No unnecessary unfold chains? Using simp, omega, ring_nf where appropriate?
• API design: Are public definitions well-typed and composable?
• Module structure: Are imports minimal? Use #min_imports to verify
• CLAUDE.md: Update toolchain version to v4.28.0-rc1, update phase status

Documents to update

• doc/HOL-Light-to-Lean-Execution.md — reflect any design changes
• doc/architecture-reflections.md — update with new automation insights
• doc/bignum-plan.md — update current state metrics

Acceptance Criteria

• All Wave 1 code reviewed
• No Lean anti-patterns remaining
• Documentation updated
• CLAUDE.md updated

Dependencies

• W1-5 (all other Wave 1 work must be complete)