feat: add wildcat borrow case

[fricoben]

Summary

• add the Wildcat family and Wildcat V2 implementation manifests
• add a Wildcat V2 borrow-liquidity benchmark case and generated task
• model the successful borrow path and prove positive borrows preserve required liquidity

Verification

• lake build Benchmark.Cases.Wildcat.BorrowLiquiditySafety.Compile

Notes

• the current reference proof isolates the arithmetic argument mechanically but uses one explicit axiom for the successful borrow post-state writes due a Verity macro limitation around requireSomeUint on multiplication-heavy paths