Read an exponent out of a logarithm where a limit says the base holds its sign (#902)

[Rafael-SOWNet]

2.1.0 withdrew log_b(a^c) = c * log_b(a) from an undecided argument (#902, #903), because the
identity needs Im(c * ln a) inside ln's principal strip and the rule asked for nothing —
ln(e^x) came back as x, which at x = 3*pi*i is 9.4247i where the expression is pi*i. Two
limits were recorded as the price, with a test asserting the loss:

	2.1.0	this PR
lim x->+oo (x^2)^x / e^(2*x*ln(x))	unevaluated	1
lim x->+oo x^x / e^(x*ln(x) - ln(x))	unevaluated	+oo

Both are answered again, by the route #922 built for the logarithm gathering: a stated approach.
A base that holds a positive sign on the way to the destination makes ln a real, and an exponent
that is real along the approach leaves the product real, so there is nothing for the principal
branch to discard.

Outside a limit the rule still declines. ln(e^x) and log(2, 2^x) are still left as written,
and that half has a test of its own now — widening the guard until an ordinary Simplify applies
the identity restores #902's wrong answer while every limit that motivated the change keeps passing.

Realness is decided structurally rather than read off a limit: a positive limit does not make a
base real on the way to it, since x + i*sin(x) tends to +oo off the real line. Closed real
subexpressions (which is how pi and e get in), the approach variable, and sums, products,
quotients and absolute values of those qualify. A power needs a whole exponent or a decidably
positive base, since (-2)^(1/2) is imaginary. A second variable carries no approach and is
refused, as is anything unlisted — the list costs coverage and never correctness.

The prediction this retires is worth more than the two answers

Both limits were recorded as needing an assumption travelling with the expression — #746's
tier 1, and the second half of #721 — on the strength of three insertion points that were each
implemented, instrumented and measured to fail.

The measurement was sound and the conclusion drawn from it was not. All three were pre-passes: a
pre-pass rewrites the expression and hands it on, so it cannot reach the candidate search that
rebuilds the logarithm behind it, which is exactly what the instrumentation showed (the rule is
asked 117 times inside one l'Hopital descent). An ambient scope is not a pass. The rule itself
asks whether an approach is being read, so it is answered wherever the rule is asked, candidate
search included. No assumption mechanism arrived and none was needed.

Written up as §12 of SimplificationContract.md, with the distinction to carry to the next unsound
rule of this shape: a rewrite the machinery performs on a shape it matches directly (#802) reaches
what the machinery constructs; a condition the rule asks an ambient scope about (#922, and this)
reaches that and what Simplify constructs for itself.

Measured

The failure mode for these rules is a hang rather than a wrong answer — the limit machinery's
own expansion creates the shapes they put back — so the suite duration is a reading, not a footnote.

• suite 6950 passed / 0 failed, 4m38s (normal); F# wrapper 130/130
• boundcheck 0 disagreements; crashcheck 1652 cases, 0 crashed, 0 did not finish
• propcheck 1340 checks / 0 failures; rootcheck 596/596 clean; simpsweep
  10463/10463 agree
• casbench 116/119, 0 wrong / 0 error / 0 timeout — equal to a stock-master build of the
  same harness, measured rather than assumed (the committed coverage.md in the analysis workspace
  predates Gather logarithms only where that is exact, and tell the limit machinery where it is going #922 and still says 117)

Closes the limit half of #902. Relates to #721.

🤖 Generated with Claude Code