fix(certora): cheapen CreatedMarkets max LIF invariant

[prd-carapulse]

Summary

• Replaces the nonlinear to_mathint(liquidationCursor) * (WAD - lltv) CreatedMarkets predicate with an inline lowest-LLTV cursor guard plus the enabled-cursor bound invariant.
• Adds a local CreatedMarkets invariant proving enabled liquidation cursors are bounded by WAD, so the max-LIF invariant can use that bound cheaply.
• Keeps the parent PR's protocol behavior unchanged; this is Certora-spec-only.

Request Context

• Initiator: Mathis / Slack: <@U02NB58F6R3> / GitHub: @MathisGD
• Initial Slack thread: C0B520ZTPJM / thread_ts 1782064536.363429
• Additional context: Parent PR modular lif #992 failing verify (CreatedMarkets) on createdMarketsHaveMaxLifAtMostTwoWad timeout in take and liquidate.
• Rationale: Fix parent PR CI without weakening the protocol-side max-LIF check.

Test Plan

• certoraCVLFormatter -w certora/specs/CreatedMarkets.spec
• certoraRun certora/confs/CreatedMarkets.conf --compilation_steps_only
• forge build --force
• git diff --check

Stacked on: #992

Requested by: <@U02NB58F6R3>