Consolidate to single proof file

Simplified project structure: all definitions and proofs now in a single U4Lean.lean file (440 lines). No changes to the proof itself.