PowerRules has three arms that move a reciprocal through a logarithm:
Logf(Divf(Integer(1), var any1), Divf(Integer(1), var any2)) => MathS.Log(any1, any2),
Logf(var any1, Divf(Integer(1), var any2)) => -MathS.Log(any1, any2),
Logf(Divf(Integer(1), var any1), var any2) => -MathS.Log(any1, any2),
All three are unconditional, and ln(1/b) = -ln(b) is false on the negative reals. The principal argument does not negate with its logarithm:
at x = -0.63 |
|
ln(1 / x) |
0.462 + 3.1416i |
-ln(x) |
0.462 - 3.1416i |
Measured, not derived: RewriteRules.Power.ApplyOnce("ln(1 / x)") is -ln(x), and the arm was attributed by asking every rule in RewriteRules.Power.Rules which one reproduces it — PowerRules:198.
The guard already exists, 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.
Sumf(Logf(var any3, var any1), Logf(var any3a, var any2)) when any3 == any3a
&& MayGatherLogarithms(any1, any2, isDifference: false) => ...Same defect, same file, fixed for one pair and not for its three neighbours. ln(1/b) is ln(1) - ln(b), so a reciprocal is the difference case with a numerator of 1 and the existing helper answers it directly — including its second way in, where the limit machinery has established the sign on the way to a destination.
What it does and does not break
Simplify does not produce it — "ln(1 / x)".Simplify() is ln(1 / x), so no caller sees a wrong answer today; the candidate search does not pick that branch.
A caller applying RewriteRules.Power on its own does, and that is what #746 tier 2 makes possible: rule sets as first-class data that a caller may reach for one at a time.
Why it was not found before
work/rulecheck samples nothing that builds log(_, 1/_): its level-3 corpus was a stride-13 sample of level 2. Widened to every level-2 shape, it reports all three arms. boundcheck did not find it either, because it measures Simplify — which, as above, declines the rewrite.
PowerRuleshas three arms that move a reciprocal through a logarithm:All three are unconditional, and
ln(1/b) = -ln(b)is false on the negative reals. The principal argument does not negate with its logarithm:x = -0.63ln(1 / x)0.462 + 3.1416i-ln(x)0.462 - 3.1416iMeasured, not derived:
RewriteRules.Power.ApplyOnce("ln(1 / x)")is-ln(x), and the arm was attributed by asking every rule inRewriteRules.Power.Ruleswhich one reproduces it —PowerRules:198.The guard already exists, ten lines below
Same defect, same file, fixed for one pair and not for its three neighbours.
ln(1/b)isln(1) - ln(b), so a reciprocal is the difference case with a numerator of1and the existing helper answers it directly — including its second way in, where the limit machinery has established the sign on the way to a destination.What it does and does not break
Simplifydoes not produce it —"ln(1 / x)".Simplify()isln(1 / x), so no caller sees a wrong answer today; the candidate search does not pick that branch.A caller applying
RewriteRules.Poweron its own does, and that is what #746 tier 2 makes possible: rule sets as first-class data that a caller may reach for one at a time.Why it was not found before
work/rulechecksamples nothing that buildslog(_, 1/_): its level-3 corpus was a stride-13 sample of level 2. Widened to every level-2 shape, it reports all three arms.boundcheckdid not find it either, because it measuresSimplify— which, as above, declines the rewrite.