Repository navigation
A root of a quotient is a quotient of roots where that is exact, and a root gathers with a whole power of its own base - #1300
Merged
Conversation
…a root gathers with a whole power of its own base
Charlwood's `arcsin(x/sqrt(1 - x^2))` had no antiderivative. By parts against one leaves
`x (1 - x^2)^(-3/2)/sqrt((1 - 2x^2)/(1 - x^2))`, a root of a quotient, which no rule
reads. On the principal branch `sqrt(P/Q) = sqrt(P)/sqrt(Q)` unless `Q < 0 < P`: with both
negative the two `i`s cancel, with `P` negative alone the two sides agree, and only
with `Q` negative under a positive `P` do they differ by sign. So the rule asks
whether there is a real `x` with `Q(x) < 0 < P(x)`, on one point of each interval
between the real roots, and splits only where there is not -- `1 - x^2 < 0` only
past 1, where `1 - 2x^2` is negative too. Quadratics at most on either side, since
those are what the rules behind this read, and a root of a sextic set free is a
search that ends nowhere: `sin(x)/sqrt(1 - sin(x)^6)` under the tangent went from a
twenty-millisecond decline to a twenty-second one in the first draft.
What the split leaves is `sqrt(1 - x^2)` above the bar beside `(1 - x^2)^(-3/2)`, and
the combining rule read them as unrelated. A whole power of the same base gathers
with the root exactly, since a whole power combines with any principal power of its
base: `P * P^(-1/2) = P^(1/2)`. Gathered, the remainder is `x/((1 - x^2) sqrt(1 - 2x^2))`,
one root of one quadratic, and Euler answers it. Where what is gathered still holds
two roots that must not be combined -- both negative somewhere the integrand is
real -- the gathered form is handed on as it is rather than declined with the
gathering undone.
## Measured
Every answer differentiated back on both sides of zero, inside the interval where
the arcsine is real.
Rubi corpus, 463-problem sample, on the same evening:
master at #1294 353/463, 0 wrong, 0 timeouts, 85 s (measured)
master at #1296 357/463 (#1295's +3, #1296's +1)
with this 358/463, 0 wrong, 0 timeouts, 87 s
One more, nothing lost: Charlwood's `arcsin(x/sqrt(1 - x^2))`.
The five test suites are 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
added a commit
that referenced
this pull request
Sep 12, 2026
…, with the sign placed where the split is exact (#1302) Charlwood's `x^3 arcsin(x)/sqrt(1 - x^4)` had no antiderivative. By parts against the arcsine leaves `sqrt(1 - x^4)/sqrt(1 - x^2)`, which is `sqrt(1 + x^2)` -- and the two roots as written share nothing, so the combining rule saw a quartic radical over a quadratic one and did what it could, which was nothing. Each base with an odd exponent is now factored over the rationals and the root split over the factors where that is exact -- at most one factor negative anywhere on the reals -- and the whole polynomial factors beside them are factored the same way; gathered again by factor, `(1 - x)(1 + x)` cancels between the two and `sqrt(1 + x^2)` is what is left. The sign of the factorization is the part that needed care. `1 - x^4` is `-(x + 1)(x - 1)(x^2 + 1)`, and with the constant folded into `x + 1` two of the factors are negative inside the unit interval -- exactly where the integrand is real -- so that split is not exact there; folded into `x - 1`, as `1 - x`, at most one factor is negative anywhere, and it is. So every placement is tried and the first exact one taken, and a base with none stays whole: `sqrt(x^4 - 1)/sqrt(x^2 - 1)` has two negative factors below `-1` whichever carries the sign, and is declined rather than answered there with the wrong sign. The refinement is kept only where it leaves fewer roots than it found, since otherwise it only respells the integrand. ## Measured Every answer differentiated back on both sides of zero. Rubi corpus, 463-problem sample, on the same evening: master at #1298 364/463, 0 wrong, 0 timeouts, 77 s (measured) master at #1300 365/463 (#1300's +1) with this 366/463, 0 wrong, 0 timeouts, 78 s One more, nothing lost: Charlwood's `x^3 arcsin(x)/sqrt(1 - x^4)`. The five test suites are green. Part of #718. Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
Rafael-SOWNet
added a commit
that referenced
this pull request
Sep 12, 2026
…rest, and equal sums cancel when the full simplification says so (#1303) Charlwood's `x arctan(x) ln(x + sqrt(1 + x^2))/sqrt(1 + x^2)` had no antiderivative, and its by-parts test pinned it as declined: with two factors to differentiate there is no reason to pick one, and what is left still holds the other. Taken together there is: the product of the two transcendental factors against `x/sqrt(1 + x^2)`, whose integral is `sqrt(1 + x^2)`, leaves `sqrt(1 + x^2) (f g)'`, and the product rule puts one factor in each term -- `arctan(x)` and `ln(x + sqrt(1 + x^2))/sqrt(1 + x^2)`, each answered. Only against an algebraic rest, which is where its integral is closed and the remainder is smaller than what it came from; `ln(x) arctan(x)/x` stays declined, `1/x` integrating to a third transcendental factor. The remainder is distributed over the product rule's sum and no further: `arctan(x) (1 + x/sqrt(x^2 + 1))` written out in full comes apart into two terms neither of which is elementary. Three things the remainders needed. The radicals differentiation leaves beside each other are combined and cancelled before the term is asked, and the sums that cancel are decided by the full simplification where the cheap one leaves them: `x + sqrt(1 + x^2)` against `sqrt(x^2 + 1) + x` is not zero as written, and a term carrying that quotient uncancelled was ten seconds of substitution candidates. A single root the combining rule leaves alone is written as the one power `P^(n/2)` it is rather than `P^q sqrt(P)`, since `sqrt(P)/P` beside a logarithm of `x + sqrt(P)` is not the `1/sqrt(P)` the substitution for that logarithm reads. And the substitution rule no longer offers the sums of a hundred-node remainder as candidates, nor any sum past thirty nodes: each is one simplification of the quotient, and one remainder of Charlwood's `x ln(1 + x^2) ln(x + sqrt(1 + x^2))/sqrt(1 + x^2)` spent twelve seconds on them. The table answers `x/sqrt(1 + x^2)` as a piecewise on a coefficient's sign whose conditions are decided, and by parts read the piecewise as the integral of `v`; it takes the inner-simplified form now, as the public entry does. ## Measured Every answer differentiated back. Rubi corpus, 463-problem sample, on the same evening: master at #1298 364/463, 0 wrong, 0 timeouts, 77 s (measured) master at #1300 370/463 (#1299's and #1300's) with this 372/463, 0 wrong, 0 timeouts, 81 s Two more, nothing lost: Charlwood's `x arctan(x) ln(x + sqrt(1 + x^2))/sqrt(1 + x^2)` and `x ln(1 + x^2) ln(x + sqrt(1 + x^2))/sqrt(1 + x^2)`. The first draft measured 100 s of wall; the cancellation by the full simplification is what took it back to 81. The five test suites are green. Part of #718. Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Charlwood's
arcsin(x/sqrt(1 - x^2))had no antiderivative. By parts against one leavesx (1 - x^2)^(-3/2)/sqrt((1 - 2x^2)/(1 - x^2)), a root of a quotient, which no rulereads. On the principal branch
sqrt(P/Q) = sqrt(P)/sqrt(Q)unlessQ < 0 < P: with bothnegative the two
is cancel, withPnegative alone the two sides agree, and onlywith
Qnegative under a positivePdo they differ by sign. So the rule askswhether there is a real
xwithQ(x) < 0 < P(x), on one point of each intervalbetween the real roots, and splits only where there is not --
1 - x^2 < 0onlypast 1, where
1 - 2x^2is negative too. Quadratics at most on either side, sincethose are what the rules behind this read, and a root of a sextic set free is a
search that ends nowhere:
sin(x)/sqrt(1 - sin(x)^6)under the tangent went from atwenty-millisecond decline to a twenty-second one in the first draft.
What the split leaves is
sqrt(1 - x^2)above the bar beside(1 - x^2)^(-3/2), andthe combining rule read them as unrelated. A whole power of the same base gathers
with the root exactly, since a whole power combines with any principal power of its
base:
P * P^(-1/2) = P^(1/2). Gathered, the remainder isx/((1 - x^2) sqrt(1 - 2x^2)),one root of one quadratic, and Euler answers it. Where what is gathered still holds
two roots that must not be combined -- both negative somewhere the integrand is
real -- the gathered form is handed on as it is rather than declined with the
gathering undone.
Measured
Every answer differentiated back on both sides of zero, inside the interval where
the arcsine is real.
Rubi corpus, 463-problem sample, on the same evening:
One more, nothing lost: Charlwood's
arcsin(x/sqrt(1 - x^2)).The five test suites are green.
Part of #718.
🤖 Generated with Claude Code
https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura