refactor: golf proofs (stacked on #1332)

[Vilin97]

Golfs proofs across Physlib, QuantumInfo, and PhyslibAlpha: streamlining arguments, using stronger mathlib lemmas and tactics, removing redundant steps, and increasing code reuse. No statements or definitions are changed — only proofs.

Stacked on leanprover-community#1332 (codex/golf-proofs-next): until leanprover-community#1332 merges, this PR's diff includes its commits. Review only the commits after 4e3d67f0.

Stats

• Proofs golfed: 510 across 24 files
• Net line change (proof bodies only): −2,760 (4,335 deletions, 1,575 insertions)
• Verification: every touched file recompiled with -Dwarn.sorry=false -Dweak.says.verify=true; full lake build green; declaration-signature audit (type hash of every lemma/theorem, type+value hash of every def) mechanically confirms zero statement/definition changes.

Process disclosure (per AI-POLICY.md)

• Models: golfing subagents ran on Claude Fable 5 (claude-fable-5) and Claude Opus 4.8 (claude-opus-4-8, after a mid-run model switch); orchestration on the same. One max-reasoning subagent per file, each self-verifying via per-file lake env lean compile.
• Wall-clock time: 22h33m wall-clock (spanning session-limit resets)
• Token usage (approximate, output tokens across all agents): ~7.6M subagent output tokens so far

Prompt used

Golf AS MUCH AS POSSIBLE in Physlib. Stack your PR on top of leanprover-community#1332.
Do not change statements, and do not cram tactics on one line. Genuinely make proofs
shorter and simpler by streamlining arguments, increasing mathlib usage, reduce code duplication, increase code reuse, use more powerful tactics, etc. Do not change any statements and definitions - only work on proofs!
Keep RAM usage under 40GB. Be thorough, go project by project carefully. If spawning agents, use max reasoning, and tell them to be very
thorough. DO NOT ASK ME ANYTHING AND DO NOT GIVE UP, KEEP FINDING NEW WAYS TO COMPRESS.
Open a draft PR once you golfed 50 proofs, and then every 10, update the PR. Put
this prompt in the PR description and also model name and how long and how many tokens this golfing process took.

🤖 Generated with Claude Code

https://claude.ai/code/session_01YRA4h6VJRALwaZK1xeUsg3

[github-actions]

Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally.

If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks.

If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip.

Important: If a reviewer adds an awaiting-author label to your PR, once you have addressed the review comments, please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.

[Vilin97]

Superseded by the upstream PR: leanprover-community#1364