feat: define well-founded recursion without large elimination of Acc

[nomeata]

This PR redefines WellFounded.fix, WellFounded.fixF and WellFounded.recursion so that they no longer eliminate an accessibility proof into data, and adds Acc.rec', Acc.recOn', Acc.ndrec' and Acc.ndrecOn' for code that needs to do so itself. Fixpoint equations and compiled code are unchanged, and Acc.rec is untouched. The one visible change is that well-founded definitions now depend on Classical.choice, which #print axioms reports.

The new definitions are characterised by a FixGraph relation — a recursive Prop inductive relating an argument to the value obtained by unfolding F along the accessibility tree — and are obtained from Classical.choice. FixGraph is single-valued, which is what WellFounded.fixF_eq and WellFounded.fix_eq are now proved from. Classical.choice is taken from the prelude to avoid the import cycle that import Init.Classical would create.

Acc.rec' and friends have the same signatures as Acc.rec, Acc.recOn, Acc.ndrec and Acc.ndrecOn, but are @[irreducible] and go through the same construction, so they carry no iota rule. Acc.rec'_intro and Acc.rec'_eq replace the definitional unfolding; Acc.rec'_eq is the one to reach for where rfl used to close an unfolding equation, and since rw matches on the head symbol, wrappers like Acc.recOn' have to be unfolded first, as in rw [myDef, Acc.recOn', Acc.rec'_eq].

@[csimp] lemmas continue to rewrite WellFounded.fixF, WellFounded.fix and the whole Acc.rec / Acc.rec' family to directly recursive implementations, so nothing becomes noncomputable in practice. The universe parameters of the primed declarations are pinned motive-first to match the unprimed ones, because @[csimp] requires both sides of a replacement theorem to have identical universe parameter lists.

This is a prerequisite for #13851, which restricts Acc.rec to Prop motives; it is useful on its own as a migration path, since downstream code can move to Acc.rec' before that lands.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-14892 build failed against this PR. (2026-08-22 09:36:56) View Log
• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-08-21 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-22 09:47:25)
• 💥 Mathlib branch lean-pr-testing-14892 build failed against this PR. (2026-08-25 12:30:14) View Log

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-08-21 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-08-22 09:47:27)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-08-22 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-08-25 11:39:22)