Roots above and below the bar that do not combine as a product combine as the quotient they are, and an even power of x under a root comes out of it

[Rafael-SOWNet]

Charlwood's x^3 arcsec(x)/sqrt(x^4 - 1) by parts leaves
sqrt(x^4 - 1)/(2 x^2 sqrt(1 - 1/x^2)), with the derivative of the
arcsecant as it is written, and nothing read it. Three rewritings, each
exact, get it to sqrt(x^2 + 1)/(2|x|), which the rule for a rational
function over the root of a quadratic answers.

The root of 1 - 1/x^2 is a root of (x^2 - 1)/x^2, and the rule that
writes a fractional power of a quotient apart read a written quotient
only; a sum with a quotient in it is read as the one quotient it is now.
That rule is asked one level below the top as well as at it, since the
remainder by parts leaves is asked there -- and no deeper: unscoped, it fed
the search on arcsin(sqrt(1 + x) - sqrt(x)), thirty levels of the same
root written apart and combined again, five seconds where declining takes
one.

sqrt(x^4 - 1)/sqrt(x^2 - 1) has two negative bases inside the unit
interval, where sqrt(P) sqrt(Q) is -sqrt(PQ), so the combining rule
left it -- and it is sqrt(x^2 + 1) there all the same, since the two is
cancel in a quotient. With a of the bases above the bar negative and b
of those below, the left side is i^(a - b) times the root of the moduli
and the right is i^((a + b) mod 2) times it, so the identity holds
exactly where the two agree modulo four: one negative on each side, or
none, or two above beside one below -- and not one below alone, where
1/sqrt(Q) is -i/sqrt|Q| and sqrt(1/Q) is +i/sqrt|Q|. Asked on every
interval between the real roots, from the one sign table the product
question already builds, since the roots are a solve per base and asking
twice on every sub-integrand of a search that declines was seconds. Taken
only where the quotient under the one root cancels to a polynomial, so
that what is handed on has strictly fewer roots than what came in.

And the root of x^4 + x^2 is |x| sqrt(x^2 + 1), exactly, since x^2 is
not negative: a polynomial every monomial of which an even power of x
divides has that power taken out of the root as a power of x for
x > 0, and the answer is extended by parity as for a quotient. What is
set free under a root either way is a polynomial of degree four at most:
the shapes the rules behind read stop there, and the half-angle form of
cos(x)^2/sqrt(1 + cos(x)^2 + cos(x)^4), a root of a sum of quotients by
(u^2 + 1)^6, set free was fourteen seconds of search where declining
takes a fifth of one.

Rubi sample (463 problems, 5 s budget), against the #1317 master this branch is cut from:

master at #1317     408/463, 0 wrong, 0 timeouts, ~98 s
with this           409/463, 0 wrong, 0 timeouts, 96 s

One more, nothing lost: Charlwood 71, in 0.2 s. Timofeev 803 goes through the quotient combination for one of its pieces, in 0.9 s where it was 2.0 s. Charlwood 128, declined, takes 1.3 s where it took 0.8; nothing else moved by more than noise. Two things were measured on the way and are not in this branch: the quotient-power rule unscoped altogether turned arcsin(sqrt(1 + x) - sqrt(x)) from a decline into a timeout, and without the degree bound the half-angle form of Charlwood 20 was fourteen seconds.

The five test suites are green.

Part of #718.

🤖 Generated with Claude Code

https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura