feat: verifiable whileM via ordered fixpoints for stronger specs

[sgraf812]

This PR generalizes Spec.whileM and Spec.forIn_loop so that termination measures and invariants can range over monadic state, and shrinks the unfolding step's typeclass footprint to just Lean.Order.MonadTail (replacing MonadAttach + LawfulMonadAttach + WPAdequate).

Internally, whileM.Pred is reformulated around the order-theoretic least fixed point: whileM_eq takes ∃ g, whileM.body f g = g as a hypothesis, discharged by whileM_eq_of_monadTail from the new typeclass. The previous Internal.Ensures / MayReturn / IsAttach / WPAdequate infrastructure is removed.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 79659457fb0377da019c274eb58e5de2ff95d9d0 --onto 5d5642107d0433519265f155ddbfbfb98007a80b. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-08 11:36:04)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 79659457fb0377da019c274eb58e5de2ff95d9d0 --onto 5d5642107d0433519265f155ddbfbfb98007a80b. You can force reference manual CI using the force-manual-ci label. (2026-05-08 11:36:06)