Skip to content

Stop pulling an exponent out of a logarithm over an undecided argument (#902) - #903

Merged
Rafael-SOWNet merged 1 commit into
masterfrom
fix/log-power-pull
Aug 12, 2026
Merged

Stop pulling an exponent out of a logarithm over an undecided argument (#902)#903
Rafael-SOWNet merged 1 commit into
masterfrom
fix/log-power-pull

Conversation

@Rafael-SOWNet

Copy link
Copy Markdown
Collaborator

Closes #902.

log_b(a^c) = c * log_b(a) holds where c * ln(a) stays inside the strip Im in (-pi, pi] that ln
maps onto. Patterns.Power.cs:158 asked for nothing at all, and since the rewritten form is shorter it
won the complexity contest — so this is what an ordinary caller got:

was is
ln(e^x) x left as written
log(2, 2^x) x left as written
ln(x^2) 2 * ln(x) left as written
ln(e^3), log(2, 2^5) 3, 5 unchanged
ln(e^x) under Codomain.Set(Domain.Real) x x, unchanged

At x = 3*pi*i the expression ln(e^x) is pi*ie^(3*pi*i) is -1 — while x is 9.4247...i.
The two differ by exactly the full turn the principal branch discards. MathS.Settings.Codomain
defaults to Domain.Complex, so this was unsound on the library's own default reading, and a negative
real base breaks it independently: log(2, 64) is 6 where 2 * log(2, -8) is 6 + 9.0647...i.

The guard asks for a base that is decidably a positive real and an exponent that may be taken as real —
the reading says so, the node's declared codomain says so, or its value is a real. A symbolic exponent
under the complex reading is none of those, so the expression is left as written. Same treatment as the
four inverse-trigonometric rules of #884: decide, or decline.

Two limits are lost, deliberately

was is
lim x->+oo (x^2)^x / e^(2*x*ln(x)) 1 unevaluated
lim x->+oo x^x / e^(x*ln(x) - ln(x)) +oo unevaluated

Right answers becoming no answer. They are unevaluated rather than NaN, so the caller is told
nothing was settled rather than told the limit does not exist, and they have a test of their own
asserting exactly that — with the reasoning in its remarks, so a future fix flips them back
deliberately rather than by accident.

This is the judgement call in the PR, so here is the reasoning rather than just the outcome.
ln(e^x) is ordinary input and its answer was silently wrong; these two limits are specialised and
their answer is now honestly absent. AGENTS.md's ordering is right answer > no answer >
wrong answer
, and BREAKING-CHANGES.md already records two integrals lost the same way, described
there as a deliberate loss. If you would rather keep the two limits and live with the wrong ln(e^x)
until assumptions travel, say so and I will close this — the measurement is the useful part either way.

Why the limit side cannot supply it, measured rather than assumed

Both lost limits want the identity that just went away: d/dx (x^2)^x carries ln(x^2), and
l'Hopital's rule reached it through Simplify. On the way to +oo the base genuinely is positive, so
the identity is true there — the limit machinery has no way to say so to the simplifier.

I implemented the limit-side reader and tried it at three insertion points: a Replace pass over the
whole expression in SimplifyAndComputeLimitToInfinity, the exponent SolveAsIndeterminatePower
constructs, and the differentiated quotient inside ApplylHopitalRuleImpl. Instrumented, the pull
fires and rewrites ln(x^2) to 2 * ln(x) correctly — and the limits stay unevaluated, because
Simplify's own candidate search writes (x^2)^x back into a logarithm and needs the identity again.
A stack trace from the guard confirms where it is asked from: Patterns.PowerRules under
Simplificator.Alternate, under ApplylHopitalRuleImpl.

So the rule is load-bearing inside the search, and no pre-pass substitutes for it. What would
restore these two is an assumption travelling with the expression — #746's tier 1, and the subject of
#721 — which is why none of that code is in this PR. Only the finding is, in the test's remarks and the
changelog.

Measured

Suite 6342 passed / 0 failed with 8 new cases; F# wrapper 130 passed. casbench 117/119 with 0 wrong,
rootcheck 596/596, simpsweep 10463/10463, propcheck 1340 checks with 0 failures, crashcheck 1652 cases
with 0 crashes.

boundcheck: 4 disagreements down to 2. Both logarithm entries go away. The two left are
log(x, x) -> 1 provided x > 0 and ln(x) + ln(x+1) -> ln(x * (1 + x)), each already recorded as
wanting a decision rather than a guard — the first is the declared-domain-versus-evaluation question of
#721 under #890, and deliberately not touched here.

Cut from master at 5397c6f9, so it does not overlap #901 in code; both edit BREAKING-CHANGES.md,
which is one conflict round for whichever merges second.

#902)

log_b(a^c) = c * log_b(a) holds where c * ln(a) stays inside the strip Im in (-pi, pi] that
ln maps onto, 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 -- e^(3*pi*i) being -1, so the two differ by exactly
the turn the principal branch discards. The rewritten form is shorter, so it won the
complexity contest and this is what an ordinary caller got. Codomain defaults to Complex, so
it was unsound on the library's own default reading; a negative real base breaks it too,
log(2, 64) being 6 where 2 * log(2, -8) is 6 + 9.0647i.

The rule now wants a base that is decidably a positive real and an exponent that may be
taken as real -- the reading says so, the node's declared codomain says so, or its value is
one. A symbolic exponent under the complex reading is none of those and the expression is
left as written, which is the treatment the four inverse-trigonometric rules of #884 got.
ln(e^3) still folds, and so does ln(e^x) under Codomain.Set(Domain.Real).

Two limits are lost with it, both from right answer to no answer, and both recorded in
BREAKING-CHANGES.md and in a test of their own that asserts the unevaluated node:

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

They want the identity that just went away: d/dx (x^2)^x carries ln(x^2) and l'Hopital's
rule reached it through Simplify. On the way to +oo the base really is positive, so it is
true there and the limit machinery has no way to say so. Supplying it from the limit side was
implemented and measured, at three insertion points: the pull fires and gives 2 * ln(x)
correctly, and the limits stay unevaluated, because Simplify's own candidate search writes
(x^2)^x back into a logarithm and needs the identity again. It is load-bearing inside the
search, so restoring these wants an assumption travelling with the expression -- #746 tier 1
and #721 -- rather than another pass. That code is not in this commit; only the finding is.

A wrong answer reachable from ln(e^x) is worse than two unevaluated limits by the ordering in
AGENTS.md, and this file already records two integrals lost the same way.

boundcheck 4 disagreements -> 2, the remaining two being log(x, x) and ln(x) + ln(x+1), each
recorded elsewhere as wanting a decision rather than a guard. Suite 6342 passed, F# wrapper
130 passed, casbench 117/119 with 0 wrong, rootcheck 596/596, simpsweep 10463/10463,
propcheck 1340 checks 0 failures, crashcheck 1652 cases 0 crashes.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@Rafael-SOWNet

Copy link
Copy Markdown
Collaborator Author

Measured against #901, since both were cut from master before the other and both edit BREAKING-CHANGES.md: they merge cleanly, no conflict round. git resolves the two changelog sections on its own, and the code changes are in different files.

Merged together on a throwaway branch: 6351 tests passed / 0 failed, boundcheck 42 shapes rewritten with 2 disagreements — the two logarithm entries gone from this PR and the two abs/sgn ones gone with #899 earlier, leaving log(x, x) and ln(x) + ln(x+1). Spot-checked: abs(-sqrt(6)) is sqrt(6), ln(e^x) is left alone, ln(e^3) is 3, abs(sgn(x)) is left alone.

So either order works.

@Rafael-SOWNet
Rafael-SOWNet merged commit cfabeab into master Aug 12, 2026
25 checks passed
Rafael-SOWNet added a commit that referenced this pull request Aug 12, 2026
One conflict, in BREAKING-CHANGES.md, where #901 and #903 landed their glance rows and their
sections around the place this branch adds its own. All three are additions rather than
disagreements: master's rows and sections keep their positions and this branch's follow.

Verified after resolving rather than assumed: abs(-sqrt(6)) is sqrt(6), ln(e^x) is left as
written, and a solve answer carrying a conditional set still prints its own binder. Suite 6359
passed, F# wrapper 130 passed, both 0 failed.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Simplify turns ln(e^x) into x, which is wrong off the strip Im x in (-pi, pi]

1 participant