perf: compute the COFE solver's up/down pair by a single recursion

[sgraf812]

Description

perf: compute the up/down pair by a single recursion. Fix.Impl.up and Fix.Impl.down were mutually recursive, so the compiled code for either hom at level k recomputes both branches at every level, which is 2^k recursive calls. updown computes the section/retraction pair at every level by a single recursion and up/down are its projections, making that O(k). All solver proofs survive unchanged up to structure eta. Measured on a round-trip of a value through level k of a tower over ProdOF (HomOF (LaterOF IdOF) (LaterOF IdOF)) (constOF (LeibnizO Nat)) in the interpreter: the mutual recursion costs 84ms at k = 14 and quadruples every two levels (6.4s at k = 20); the paired recursion stays around a millisecond even at k = 2000. Instrumenting the functor's map counts 2k(k+1) hom constructions with the pair against roughly 4 * 2^k without.

The regression test Iris.Tests.COFESolverEval guards exactly this cost: it round-trips a value through level 21 of that tower at runtime (upN then downN) and reads back a Nat threaded through the constOF component, so the homs must actually be constructed by the compiled code. Compiled evaluation is not subject to maxHeartbeats, so the check is a wall-clock budget calibrated against a pure baseline fold timed in the same interpreter, which makes machine speed cancel out: the paired recursion costs 1 baseline units, the mutual recursion 300 or more, and the limit is 20. A regression therefore fails deterministically in well under a minute instead of hanging the build. The file is not a module and is built by the IrisTest glob rather than listed in Iris.Tests.

Checklist

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

[Kaptch]

Thanks! I'll take a look at all three ~early next week :)

[sgraf812]

Thanks for giving it a look, but no rush! This was all produced by Claude and I need to review it myself. #497 and #498 are ready for review, but no need for you to read this one unless I have removed draft status.

[sgraf812]

Not very convinced about the "perf relative to baseline" approach due to flakiness in CI, but I suppose we can always deactivate the test when it becomes a problem.

[Kaptch]

All three look good (this one is especially appreciated)! May I ask you only to remove the tests in all three? I think the clarifying comments in the code are enough to understand the rationale. After that, I can merge them asap.

[sgraf812]

Great! Removed the tests.