RFC: a more robust solution to `auxDecl`

During elaboration, recursive calls are not represented as constants (as the function is not part of the environment yet) but local variables with the auxDecl LocalDeclKind. As that is not how users think about recursive calls, there is significant work keeping up the illusion that these variables are more or less constants. Some quick examples:

• https://github.com/leanprover/lean4/commit/fce7697151475aef7d46ebba052952e2148e77a4
• https://github.com/leanprover/lean4/commit/3e45060dd52c13ee4904da1ccf6279df154f1a8a#diff-17db126c0cb31426bd9426c44e4ff7a2e864b302735fa8830ab66d3934ad8674R1111-R1192
• Many tactics have to special-case them, which is easy to forget to do
• The language server also gets confused about a constant and a variable existing at the same position
• ...I feel like there were even more examples/issues

Unfortunately, we cannot e.g. add these as constants as opaques to a temporary environment that is later discarded as elaboration may mutate the environment even during nested term elaboration and removing specific constants from an environment is not something we should support. Thus I propose to make recursive bindings merely logically part of the environment during elaboration, which could be done in a variety of ways:

• Keep recursive bindings in the elaboration context, abstract direct environment access during elaboration away into monadic functions that mix in the recursive bindings
• Keep recursive bindings in a new structure extending Environment used only during elaboration: similar to above, but works for non-monadic functions as well
• Keep recursive bindings in a new field of Environment itself that is never accessed by the kernel, clear field at end of elaboration: not elegant, but least churn

Start by reading the issue's discussion of recursive bindings, auxDecl, elaboration, and Environment. Compare the three proposed approaches: elaboration-context integration, a temporary Environment extension, or an Environment field. Done means selecting and implementing a robust approach that avoids special cases while preserving kernel behavior, but no specific files or tests are named.