A reciprocal inside a logarithm is not moved out unconditionally (#1062)

[Rafael-SOWNet]

ln(1/b) = -ln(b) is false on the negative reals: the principal argument does not negate with its logarithm.

at b = -0.63
ln(1 / b)	0.462 + 3.1416i
-ln(b)	0.462 - 3.1416i

Three arms of PowerRules applied it for every b.

The guard already existed, ten lines below

// ln(a) + ln(b) = ln(a*b), and the difference likewise, are false off the positive
// reals: at x = -3 the sum of ln(x) and ln(x+1) exceeds ln(x*(1+x)) by 2*pi*i, the
// turn of the argument the principal branch discards. Both were applied
// unconditionally, and that was the last disagreement `boundcheck` reported.

Same defect, same file, fixed for one pair and not for the three arms above it. That is the third time in this file's history a branch-cut fix has stopped at the rule it was reported against — after #752 and #801, whose own test file says the same thing about its predecessor.

The guard here is the same one, asked through the same helper, because it is the same question: ln(1/b) is ln(1) − ln(b), so a reciprocal is the difference case with a numerator of one. Both ways of earning the rewrite carry over — the argument is decidably a positive real, or the limit machinery is reading towards a destination and has established the sign on the way. Nothing is withdrawn outright, which the comment there warns costs terminating limits.

	before	now
RewriteRules.Power.ApplyOnce("ln(1 / x)")	-ln(x)	ln(1 / x)
RewriteRules.Power.ApplyOnce("log(2, 1 / x)")	-log(2, x)	log(2, 1 / x)
RewriteRules.Power.ApplyOnce("log(1 / x, 1 / y)")	log(x, y)	log(1 / x, 1 / y)
RewriteRules.Power.ApplyOnce("ln(1 / 2.5)")	-ln(5/2)	-ln(5/2) — still fires where it is sound

Why nothing had caught it

Simplify is unchanged. "ln(1 / x)".Simplify() is ln(1 / x) before and after, because the candidate search never picked that branch. So boundcheck, which measures Simplify across branch cuts, could not see it, and no public answer moves.

What moves is RewriteRules.Power applied on its own — which is precisely what #746 tier 2 makes a caller able to do, and why a rule being unsound in isolation is now worth fixing rather than tolerating.

It was found by widening work/rulecheck's corpus: its level-3 shapes were a stride-13 sample of level 2, so it never built log(_, 1/_).

The test asserts against the rule set, not against Simplify

Asserted against Simplify it would pass whatever the rule did. Four of its seven cases fail on master.

Full suite: Failed: 0, Passed: 8600, Skipped: 14, Total: 8614.

🤖 Generated with Claude Code

https://claude.ai/code/session_01Bjumi5K7fg8yx6UK1mZTQd