feat: add Royco Dawn valuation recovery case

[fricoben]

Summary

Adds the Royco Dawn valuation-recovery benchmark pinned to Royco's public Dawn source commit 5fd7c9922b7bd1d9c860ce4ce39c339d28798cb2.

The case models _previewSyncTrancheAccounting, including cross-tranche signed attribution, JT-first then ST recovery, loss booking, forced-perpetual JT liability erasure, fee and yield arithmetic, and successful-execution fixed-width bounds.

Proven specifications

• recovery gains clear higher-priority liabilities before lower-priority allocation
• JT and ST valuation losses are booked to the source-matching liability ledger
• ST-attribution residual is absorbed by the JT effective delta
• forced-perpetual liability erasure is explicit in the trace
• signed attribution overflow at the documented boundary is rejected
• successful preview sync conserves total effective NAV against current total raw NAV

All six reference theorems compile without sorry or axioms. Generated task files remain agent-facing exact ?_ placeholders.

The active-case list changes the checked-in v0.2 environment identity. This PR refreshes
the v0.2 environment ID and canonical manifest hash using the existing post-case-addition
procedure. The frozen v0.2 task set remains unchanged at 240 tasks.

Scope

The theorem surface covers successful executions of the modeled preview transition. It does not prove deposits, redemptions, token transfers, YDM internals, or arbitrary transaction sequences. External YDM values are explicit inputs. Checked-width arithmetic is represented by successful-path predicates and exact arithmetic helpers.

Verification

lake build Benchmark.Cases.Royco.DawnValuationRecovery.Contract
lake build Benchmark.Cases.Royco.DawnValuationRecovery.Specs
lake build Benchmark.Cases.Royco.DawnValuationRecovery.Proofs
lake build
python3 scripts/validate_manifests.py
python3 scripts/check_reference_solutions.py
./scripts/check.sh

Observed locally:

• Contract, Specs, and Proofs targets pass
• full 2509-job build passes
• manifest validation passes for 39 families, 40 implementations, 40 cases, and 247 tasks
• all six Royco task-runner executions pass with ready reference and editable proofs
• repository check passes 386 tests and all 240 frozen-v0.2 reference checks
• git diff --cached --check passes
• pinned Solidity SHA-256: 0ad7d96f4d3b00d0348492f24bb470bbd6558fbb3d339d8ff928033003f5b148