fix: make the Banach fixpoint opaque

[sgraf812]

Description

Fixes a class of deterministic timeouts in isDefEq checks that involve fixpoint.

The regression test Iris.Tests.Fixpoint shows the minimal shape: a contraction Phi on the hom space SiProp -n> SiProp whose body applies the recursive call to two different argument transformations, and a unification between (fixpoint Phi.f) P1 and (fixpoint Phi.f) P2 for syntactically different P1, P2 (a failed exact that a subsequent tactic recovers from). When isDefEq can unfold fixpoint into COFE.compl of the approximation chain, the comparison only resolves after reducing both applications to their True-leaf trees; the two recursive-call arguments give every path through the unfolding a distinct argument, so the defeq cache cannot collapse the descent, and at step index 24 the single failed unification exceeds even the default maxHeartbeats budget. The same mechanism measured in a downstream development (a guarded recursive-domain interpreter): Fixpoint.chain iterations x77-295 and tens of thousands of projection unfolds per goal, ending in deterministic timeouts.

The fix follows #497's treatment of Tower.iso: fixpointP f : { x : α // x ≡ f x } packs the fixpoint together with its unfolding equation as a single opaque value, with the chain construction kept in fixpointAux. fixpoint and fixpoint_unfold are its two projections, so both the elaborator and the kernel treat fixpoint as a stuck constant: the failed unification above is detected at the arguments, within a maxHeartbeats 4000 cap that turns any reintroduction of chain descent into a deterministic timeout. fixpoint_ne is reproved from fixpoint_unfold; every other fixpoint lemma (fixpoint_unique, fixpoint_ind, the fixpointAB family) already lived on the API and is untouched. All statements are unchanged.

As in the #497 test, the test file is deliberately not a module (non-module importers ignore module-system annotations such as @[expose], so opaque is what seals fixpoint for them, and the file checks the seal from such an importer; the IrisTest glob builds it), and Phi's proof fields are sorry (silenced): unification only ever touches the data.

Verified in both directions: replacing fixpoint by the chain-based fixpointAux in the regression example reproduces the deterministic timeout at the 4000 cap (and still at 200000); with the opaque packing it passes under a 400 cap.

Checklist

• My code follows the mathlib naming and code style conventions
• I have added my name to the authors section of any appropriate files