perf: do not reference the input string from recursive-call annotations

This PR fixes a quadratic slowdown when elaborating files with many recursive definitions. The `share common exprs` step of definition elaboration hashed the whole input file once per recursive call, so a file with thousands of structurally or well-founded recursive definitions could spend most of its elaboration time there.

Recursive calls are annotated with their `Syntax` via `mkRecAppWithSyntax`, so that `WF` and `Structural` can report errors at the call site. Every token of that syntax carries a `SourceInfo.original` whose `leading` and `trailing` substrings share the whole input string, and identifiers additionally carry `rawVal`, another substring of it. The annotated expression is later hash-consed by `ShareCommon.shareCommon'` in `shareCommonPreDefs`, a traversal that follows every pointer and has no identity cache for strings. It therefore reached the input string once per substring and hashed it every time. The cost per definition was proportional to the file size, and the cost per file was quadratic in the number of recursive definitions.

`mkRecAppWithSyntax` now stores a copy of the syntax that does not reference the input string. `SourceInfo.original` becomes `SourceInfo.synthetic` with the same range and `canonical := true`, and identifiers get a fresh copy of their raw value. All consumers of the annotation use it through `withRef`, which only needs the source range, so error positions are unchanged. The syntax tree is kept rather than reduced to a position because the `partial_fixpoint` error message prints the recursive call, and syntax produced by quotations may have no position to recover the text from. The only observable difference is that a comment written inside a recursive call no longer appears in that message.

The cost of the bug was (number of recursive calls) × (size of the input string). The two experiments below vary each factor separately.

The new benchmark `tests/elab_bench/share_common_rec_app.lean` generates the input as a string and elaborates it with `Lean.Elab.process`, so the source infos point at that generated string. It measures the wall-clock time of elaborating the whole input. Both rows contain the same 2000 recursive definitions; the second row appends a 4 MB comment, which is inert but makes the input string large.

| Input | Before | After | Speedup |
|---|---|---|---|
| 2000 recursive defs, 112 KB | 5.2 s | 4.9 s | 1.06x |
| 2000 recursive defs + 4 MB comment, 4.1 MB | 12.2 s | 5.2 s | 2.3x |

The first row barely changes because a 112 KB file is small, so the hashing was a small part of the 5 s of ordinary elaboration. The second row shows the bug: the comment alone cost 7 s before the fix. After the fix the two rows are equal, that is, the input size no longer matters. If this annotation ever references the input string again, the second row will jump.

The second experiment isolates the affected step. The numbers are the profiler's `share common exprs` time summed over all declarations of a generated file, not the whole elaboration time.

| Input | Before | After | Speedup |
|---|---|---|---|
| 1000 recursive defs, 56 KB | 0.19 s | 0.015 s | 13x |
| 8000 recursive defs, 450 KB | 6.05 s | 0.25 s | 24x |
| 1000 recursive defs + 2 MB comment, 2.1 MB | 2.76 s | 0.016 s | 172x |
| 8000 non-recursive `match` defs, 450 KB | 0.15 s | 0.17 s | none |

After the fix the step costs about 0.02 ms per definition regardless of the input size: 1000 definitions take 0.015 s with or without the 2 MB comment, and 8000 take 0.25 s. Before the fix the same step grew with the input size: the 2 MB comment turned 0.19 s into 2.76 s for identical definitions, and going from 1000 to 8000 definitions multiplied the cost by 32 rather than 8, because the file grew with the definitions. The last row has no recursive calls, hence no annotation, and shows that this step was never slow on its own.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>