fix(verdict): bound recursive function eta expansion

[oxura]

Fixes #1164.

Recursive function domains need not have a finite eta-long form. Track the type path only on synthetic eta binders; stop when that path revisits a type and let the kernel check the remaining argument. Original source variables start their own paths, so an unrelated finite function is not skipped merely because its type appeared elsewhere. Both argument elaboration and case-tree leaf elaboration use this boundary.

On current main, the finite translation then exposed a second recursion: Term.fits unfolded identical recursive types and recursively fitted their domains forever. It now checks structural reflexivity before unfolding, as conversion already does. The fits_sound proof handles that branch through reflexive conversion; the complete Lean source, including all kernel claims, compiles. No new axioms, fuel increase, source-checker edit or kernel eta-conversion rule.

The regression contains the report's erased recursive domain, the alternating G/G -> U32 domain, a recursive-function leaf, and an ordinary finite higher-order function. Its runtime pin exercises the finite control; the recursive types are exercised by export and the real kernel verdict, not claimed as emitted-runtime coverage. The elaborator's header documents the finite expansion boundary.

Verification on Linux x86_64:

• Untouched main: a separate Knot -> U32 recursive-domain input passes source checking, then .bendtt export fails with machine-stack overflow. After: export finishes and the real kernel accepts it.
• Full changed kernel built from source using the pinned Lean 4.34.0 toolchain; the original issue's finite translated F example prints ALL PROOFS CHECK.
• Real --verdict: the new regression plus ten existing eta, dependent-function-equality, quantity and recursive-group fixtures all print ALL PROOFS CHECK.
• Direct kernel negative controls still reject a label of the empty enum, a wrong function result label, and Type-to-Data subsumption.
• New regression's default IO execution and actual native binary both print 23.
• bun gates/repo.ts: PASS 54 / 54; gate files and token caps unchanged.

No cluster or physical GPU run is claimed. README, guides and intro-film presentation are unchanged.

[Lorenzobattistela]

Thanks @oxura. The bug in #1164 is real, and this does make those examples export. We're closing it anyway, because it fixes one of several places that unfold a recursive type definition forever (the same family as #1206), and it changes the kernel to get there. We'd rather fix this one abstraction level above, so recursive types are handled in one place for every pass, instead of patching each pass on its own. #1164 stays open to track that.

[oxura]

Understood. I will not reopen the per-pass/kernel patch or propose another workaround in this PR. The reproductions and export before/after evidence remain available here, but #1164 should be solved through the shared recursive-type abstraction covering every pass, alongside #1206. I am leaving that architectural/kernel work to your intended implementation.