Stirling reaches only the power form, so lim x->+oo ln(x!)/x and x!/x^x are still unevaluated #765

Follow-up to #754, measured on the #764 branch. That PR applies Stirling's expansion of ln(f!) inside SolveAsIndeterminatePower, which is where f^g is turned into e^(g * ln f) — so it reaches a factorial only when one sits under a vanishing exponent. Everything else is untouched:

lim x->+oo ln(x!) / x            unevaluated    it is +oo   (~ ln(x) - 1)
lim x->+oo ln(x!) / (x * ln(x))  unevaluated    it is 1
lim x->+oo x! / x^x              unevaluated    it is 0
lim x->+oo x^x / x!              unevaluated    it is +oo
lim x->+oo x! / e^x              unevaluated    it is +oo

Checked numerically with mpmath at 40 digits — ln(x!)/x is 12.8155 at x = 1e6 against ln(x) - 1 = 12.8155, and ln(x!)/(x ln x) is 0.9638 at x = 1e12, approaching 1 slowly from below.

The first two are the ones worth having: ln(n!) ~ n ln n is the standard statement of the result, and a library that answers (x!/x^x)^(1/x) but not ln(x!)/x is answering the harder question and not the easier one.

Why it is not simply a Replace

Rewriting ln(f!) as f*ln(f) - f + ln(2*pi*f)/2 wherever it appears is not sound. What is dropped is 1/(12f) + O(1/f^3), which vanishes — but it is multiplied by whatever the node sits under, and an expression can be built around exactly that term:

x * (ln(x!) - (x*ln(x) - x + ln(2*pi*x)/2))    ->  1/12,  and the rewrite would answer 0

#764 handles this by requiring power / f -> 0, which it can state because it knows the expression is e^(power * ln(base)) and the coefficient of the logarithm is exactly power. Away from that shape the coefficient has to be found rather than known.

What it would take

The coefficient is obtainable: substitute a fresh variable L for the ln(f!) node, differentiate the expression with respect to L, and require that derivative times 1/(12f) tend to zero. For ln(x!)/x that is (1/x) * 1/(12x) = 1/(12x^2) -> 0, so the rewrite is licensed; for the difference above it is x/(12x) = 1/12, and it is refused. That is the same guard #764 uses, computed rather than read off the shape.

Placement wants care for the reason recorded in work/TRIAGE.md: limit rules are order-dependent, and this one asks for a sub-limit of its own (f -> +oo), so it belongs behind the descent rather than inside it — the "only where nothing else answered" position that SolveByRewriting already occupies.

x!/x^x and its relatives are a further step again: there the factorial is not under a logarithm at all, and reaching it means writing f! as e^(ln(f!)) first, whose relative error e^(1/(12f)) is harmless for a plain limit and is not harmless under an outer exponent. Worth doing after the logarithm case and on its own measurement.