Skip to content

Powers of a logarithm's two linears beside it are integrated by t = L1/L2, a power of x beside a power of A + B ln(c x^n) by the closed reduction, and the principal root of a negative real is exactly imaginary - #1379

Merged
Rafael-SOWNet merged 4 commits into
masterfrom
log-quotient-substitution
Sep 17, 2026

Conversation

@Rafael-SOWNet

@Rafael-SOWNet Rafael-SOWNet commented Sep 16, 2026 •

Copy link
Copy Markdown
Member

Rubi's logarithm families (family 3): 180 → 206 of the 225-problem sample, 0 wrong, 0 error, both sides measured with the same harness. The independent suites: 1707/1774 (from 1706), 0 wrong, 0 timeouts. Cut from master; independent of #1377.

What it does

Powers of a logarithm's two linears beside a power of it, by t = L1/L2. Rubi's (f + g x)^m (h + i x)^q (A + B ln(e ((a + b x)/(c + d x))^n))^p with f + g x and h + i x proportional to the logarithm's linears took the rational-beside-a-logarithm rule one step of parts at a time, with the coefficients of its partial fractions growing to b^205, and then the substitution search past its budget — 21 of the 27 problems left in the family. Under t = (a + b x)/(c + d x), with D = b c − a d: a + b x = D t/(b − d t), c + d x = D/(b − d t), dx = D dt/(b − d t)^2, so the integrand is a power of t times a power of b − d t times a power of A + B ln(K t^n), which the same rule answers in one step (SolveByTheQuotientOfTheLogarithmsLinears, before that rule in the chain). The powers of t and of b − d t are summed so that each stands once — with (b − d t)^2 above and (b − d t)^(−4) below as they came, the rule expanded its rational part to a page. Exponents may be symbols ((g L1)^m taken as g^m L1^m, K L1^n/L2^n as K t^n, the generic case) and the answer is checked against the integrand at sampled points. A polynomial beside the logarithm is left to parts in x. The proportionality of a linear to the logarithm's is decided at sampled points and its ratio read exactly, because the chain hands the linear on as a g^0 b^(−1) + x for (a g + b g x) made monic, which is not read as a polynomial; a linear in that spelling is read by its derivative.

x^p (A + B ln(c x^r))^n by the closed reduction of x^p ln(x)^n. The affine logarithm's derivative is s/x for s = B r, each step of parts brings the factor s; a lone power of it is p = 0, and (d x)^m is d^m x^m. Rubi's (e x)^q (a + b ln(c x^n))^3, (a + b ln(c (d x^m)^n))^4, and t^(−2 − m) (A + B ln(e t^n))^2 in the variable of the substitution above.

#1378, found on the way. That reduction wrote u ln(u^2) for an integrand's ln(−1 + a x) under u = sqrt(−1 + a x), and the corpus harness read the answer as wrong at 3 of 6 points where its derivative is the integrand: at −1 + a x < 0 the root came back from the polar form with a real part of 6e-102 (cos(pi/2) at a hundred digits), and its square lay a hair below the negative axis, where ln reads −i pi for the +i pi the number has. Fixed in Number.Pow: a negative real to a real power that is a whole number of halves is the modulus to that power times i^k, exactly; and for a base off the positive axis a real power that is a whole number (how 2 arrives with the downcasting off) is the integer it is, so the square is the exact multiplication. A positive real keeps its exp(p ln b) — the first version applied the integer path there too, and a sum with 3.66^120 in every term stopped cancelling, because every power of the base shares the logarithm's digits and not a repeated product's.

Measured

Family 3, 25 problems a file, 5 s budget, master 2b4a5256 against this branch, same harness on both (the 185 recorded for master in #1363 was an older verification — a right answer with b^205 coefficients cannot be verified at a hundred digits by either, and two problems master "solved" then are timeouts for both now):

Source Run master branch
3.1.2 (d x)^m (a+b log(c x^n))^p 25 24 25
3.1.4 (f x)^m (d+e x^r)^q (a+b log(c x^n))^p 25 23 24
3.1.5 u (a+b log(c x^n))^p 25 22 24
3.2.1 (f+g x)^m (A+B log(e ((a+b x) over (c+d x))^n))^p 25 15 22
3.2.2 (f+g x)^m (h+i x)^q (A+B log(e ((a+b x) over (c+d x))^n))^p 25 9 24
3.2.3 u log(e (f (a+b x)^p (c+d x)^q)^r)^s 25 23 23
3.3 u (a+b log(c (d+e x)^n))^p 25 21 22
3.4 u (a+b log(c (d+e x^m)^n))^p 25 23 23
3.5 Logarithm functions 25 20 19
total 225 180 206

The one loss, ln(d (a + b x + c x^2)^n)/(d + e x)^5, is 19 s alone on both builds and was answered in master's run from a warm memo at 24 s of wall time — budget-edge, not a change. Every answer is verified by differentiating back with the parameters pinned, in the harness and in the library.

Left in the family: polynomial × log with the coefficients growing ((f + g x)^3 (A + B ln(...)), 8 s on both), (a + b ln(c (d (e + f x)^p)^q))/(g + h x)^2 (a different linear below; the step of parts declines its symbolic partial fractions), and the 3.5 miscellany.

Four suites green. The gate moved, downwards: SolveEasy allocates 783,622 → 453,364 B (−42%), 390 → 222 µs — the solve of x^2 + x + 1 evaluates sqrt(−3) four times, each of which was a hundred-digit Arctan2, cos and sin of pi/2 through the polar form and is now the decimal square root times i. The first push took the modulus through the exact-base path, whose search over every root of unity of 3 cost the same row +17.4% and failed the gate on this PR, which is what the gate is for; the 2077th entry in version_performance_control.md records both, and the baseline is the run of commit 6e5986a7.

Part of #718.

🤖 Generated with Claude Code

https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura

…1/L2, a power of x beside a power of A + B ln(c x^n) by the closed reduction, and the principal root of a negative real is exactly imaginary

Rubi's (f + g x)^m (h + i x)^q (A + B ln(e ((a + b x)/(c + d x))^n))^p
with f + g x and h + i x proportional to the logarithm's linears took
the rule for a rational function beside a power of a logarithm one step
of parts at a time, with the coefficients of its partial fractions
growing to b^205, and then the substitution search past its budget:
twenty-one of the twenty-seven problems left in the family-3 sample.
Under t = (a + b x)/(c + d x), with D = b c - a d, a + b x is
D t/(b - d t), c + d x is D/(b - d t) and dx is D dt/(b - d t)^2, so the
integrand is a power of t times a power of b - d t times a power of
A + B ln(K t^n), which the same rule answers in one step; the powers of
t and of b - d t are summed so that each stands once, since with
(b - d t)^2 above and (b - d t)^(-4) below as they came the rule
expanded its rational part to a page. The exponents may be symbols,
(g L1)^m taken as g^m L1^m and K L1^n/L2^n as K t^n, the generic case,
and the answer is checked against the integrand at sampled points. A
polynomial beside the logarithm is left to parts in x, where it is one
closed step and in t a power below the bar. The proportionality of a
linear to the logarithm's is decided at sampled points and its ratio
read exactly, since the chain hands the linear on in whatever spelling
it gave it -- a g^0 b^(-1) + x for (a g + b g x) made monic -- and a
linear in that spelling is read by its derivative.

The reduction of x^p ln(x)^n takes A + B ln(c x^r) in the logarithm's
place, whose derivative is s/x for s = B r, each step of parts bringing
the factor s; a lone power of it is the case p = 0, and (d x)^m is
d^m x^m. Rubi's (e x)^q (a + b ln(c x^n))^3 and (a + b ln(c (d x^m)^n))^4,
and t^(-2 - m) (A + B ln(e t^n))^2 in the variable of the substitution
above.

That reduction wrote u ln(u^2) for an integrand's ln(-1 + a x) under
u = sqrt(-1 + a x), and the corpus harness read the answer as wrong at
three of six points where its derivative is the integrand: at
-1 + a x < 0 the root came back from the polar form with a real part
of 6e-102, from cos(pi/2) at a hundred digits, and its square lay a
hair below the negative axis, where ln reads -i pi for the +i pi the
number has. A negative real to a real power that is a whole number of
halves is the modulus to that power times a power of i, exactly; and
for a base off the positive axis a real power that is a whole number --
how 2 arrives with the downcasting off -- is the integer it is, so the
square is the exact multiplication. A positive real keeps its
exponential of the logarithm, whose digits every power of it shares,
so that a sum with 3.66^120 in each term still cancels to what it
cancels to (#1378).

Family 3 sample (25 a file): 180 -> 206 of 225, 0 wrong, 0 error, both
sides measured with the same harness -- the 185 recorded for master was
an older verification, and a right answer with coefficients like b^205
cannot be verified at a hundred digits by either. The independent
suites: 1707/1774 (from 1706), 0 wrong, 0 timeouts.

Four suites green.

Part of #718.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura
@Rafael-SOWNet

Copy link
Copy Markdown
Member Author

Composition with #1377 (which carries #1374): merge-tree reports one conflict, Sources/Tests/UnitTests/Core/Numeric.cs — both append a test class at the end of the file, same anchor, keep both. The library files merge clean. Whichever lands second gets that one mechanical round from me.

Rafael-SOWNet and others added 3 commits September 16, 2026 12:52
…ecimal square root, not a search over the roots of unity

The first version took the modulus through the exact-base path, which
enumerates every root of unity of the base at a hundred digits to find
an exact one, and sqrt(-3) four times in a solve of x^2 + x + 1 cost
that row 17.4% of its allocation on the gate. An exact base whose
numerator and denominator are squares has an exact root; any other
takes the integer square root of the decimal and a whole power of it.
SolveEasy: 783,622 -> 453,364 bytes, 390 -> 222 us, since the polar
form's Arctan2, cos and sin at a hundred digits are gone with it. The
2077th entry in the performance log.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura
@Rafael-SOWNet
Rafael-SOWNet merged commit 05c5652 into master Sep 17, 2026
31 checks passed
@Rafael-SOWNet
Rafael-SOWNet deleted the log-quotient-substitution branch September 17, 2026 12:22
Rafael-SOWNet added a commit that referenced this pull request Sep 17, 2026
…is simplified (#1407)

atanh(tanh(a + b x))^4 was answered in 300 ms and, since #1379, ran past three minutes: the
reader for a power of A + B ln(c x^r) simplified the logarithmic derivative of any single
logarithm's argument to see whether it was r/x, and the argument here is a quotient of
exponentials whose derivative the simplifier turns over for minutes on the way to no. The
argument is read first -- products, quotients and powers of x and of constants, however
nested, c (d x^m)^n -- and anything else is not this shape without a derivative being taken.
The reader of a linear in the quotient-of-linears rule gets the same guard: a leaf with a
function of x in it is not a linear however it simplifies.

Family 7's atanh(tanh) and acoth(coth) rows are answers again, in 300 ms and 41 ms; the
1774-problem suite is unchanged at 1706 with 0 wrong.

Part of #718.


Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura

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.

1 participant