Repository navigation
The tangent substitution reads a polynomial in sine and cosine that is homogeneous up to parity - #1294
Merged
Conversation
…s homogeneous up to parity `cos(x)/(sin(x)(2 + sin(2x)))` had no antiderivative. Its arguments unified, it is `cos/(2 sin + 2 sin^2 cos)`, and the third of Bioche's rules declined it: the denominator has terms of degree one and three, and the rule read "homogeneous" as "every term of the same degree". A term two degrees short of the highest is the same term times `sin^2 + cos^2`, which is one, so `sin + sin^2 cos` is `sin (sin^2 + cos^2) + sin^2 cos`, of degree three throughout, and the substitution `t = tan(x)` turns the quotient into the rational function it always was. The reader lifts every term to the highest degree that way where the degrees share a parity; a term an odd number short is a genuine boundary, since no power of one bridges it, and stays declined. ## Measured Every answer differentiated back. Rubi corpus, 463-problem sample, against the master it was cut from (#1292), both measured on the same evening: master 349/463, 0 wrong, 0 timeouts, 87 s with this 350/463, 0 wrong, 0 timeouts, 88 s One more, nothing lost: Timofeev's `cos(x)/(sin(x)(2 + sin(2x)))`. 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
…ed by an ansatz in the half-angle tangent (#1296) Timofeev's `e^x (1 - sin(x))/(1 - cos(x))` had no antiderivative, and it is `-e^x cot(x/2)`. Nothing read it: the exponential-times-trigonometric rule wants a polynomial in sine and cosine, the half-angle substitution wants no exponential, and by parts goes round in a circle. Under `t = tan(x/2)` the trigonometric part is a rational function `r(t)`, so the integrand is `e^(a x) r(t)` with `dt/dx = (1 + t^2)/2`, and the ansatz `F = e^(a x) P(t)/Q(t)` differentiates to `e^(a x) [a P/Q + (P'Q - P Q')(1 + t^2)/(2 Q^2)]`. Asking that this equal `e^(a x) n(t)/d(t)` is one polynomial identity, `[a P Q + (P'Q - P Q')(1 + t^2)/2] d = n Q^2`, linear in the coefficients of `P`; `Q` is tried from `d`'s written factors as the exponential ansatz tries its denominators, and the derivative of what the solve returns is checked against the integrand at sampled points before it is an answer. Timofeev's has `r = (1 - t)^2/(2 t^2)`, `Q = t`, `P = -1`. The identity is exact, so the absence of a solution is a decline: `e^x/(1 + cos(x))` needs the sine beside it and `e^x tan(x/2)` has no such `P/Q` at all, and both stay declined. ## Measured Every answer differentiated back. Rubi corpus, 463-problem sample, against the master it was cut from (#1294), both measured on the same evening: master 353/463, 0 wrong, 0 timeouts, 85 s with this 354/463, 0 wrong, 0 timeouts, 85 s One more, nothing lost: Timofeev's `e^x (1 - sin(x))/(1 - cos(x))`. 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
… rational function of x and ln(x)
Hearn's `(-1 + (1 - x) ln(x))/(e^x ln(x)^2)` is `(x e^(-x)/ln(x))'` and Hebisch's
`e^(x + 1/ln(x)) (-1 + (1 + x) ln(x)^2)/ln(x)^2` is `(x e^(x + 1/ln(x)))'`. Neither had an
antiderivative, and neither is reached by parts or by any substitution, since the
logarithm is not a whole subtree to replace. They are the exponential ansatz one
level up the tower: `x` and `ln(x)` are algebraically independent, so with `L`
standing for `ln(x)` and `L' = 1/x`, the derivative of `F = e^h P(x, L)/(D(x) L^k)`
divided by `e^h` is a rational function of `x` and `L`, and asking it to equal the
integrand's is one polynomial identity in the two -- linear in the coefficients of
`P`, one equation per monomial `x^i L^j`. The exponent may hold the logarithm
itself, as Hebisch's does; `h'` is `dh/dx + dh/dL / x` and goes into every column.
The denominator is tried from the integrand's: its `x`-part as the exponential
ansatz tries its denominators, times `L^k` for every `k` from zero up to the written
power, smallest first so that the answer carries no common factor. The columns are
built one monomial at a time, each candidate's powers of `L` folded into one before
differentiating -- the quotient rule on `L/L` left `(L - L)/L^2` behind, which
nothing read -- and cleared by one common denominator. The identity is exact, so a
solution is an answer and its absence a decline: `e^x ln(x)` and `e^x/ln(x)` have no
such `P` and stay declined, and the derivative of what comes out is checked against
the integrand at sampled points all the same.
Every answer differentiated back.
Rubi corpus, 463-problem sample, on the same evening:
master at #1294 353/463, 0 wrong, 0 timeouts, 85 s (measured)
master at #1295 356/463 (#1295's own +3)
with this 358/463, 0 wrong, 0 timeouts, 86 s
Two more, nothing lost: Hearn's and Hebisch's above.
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
… rational function of x and ln(x) (#1297) Hearn's `(-1 + (1 - x) ln(x))/(e^x ln(x)^2)` is `(x e^(-x)/ln(x))'` and Hebisch's `e^(x + 1/ln(x)) (-1 + (1 + x) ln(x)^2)/ln(x)^2` is `(x e^(x + 1/ln(x)))'`. Neither had an antiderivative, and neither is reached by parts or by any substitution, since the logarithm is not a whole subtree to replace. They are the exponential ansatz one level up the tower: `x` and `ln(x)` are algebraically independent, so with `L` standing for `ln(x)` and `L' = 1/x`, the derivative of `F = e^h P(x, L)/(D(x) L^k)` divided by `e^h` is a rational function of `x` and `L`, and asking it to equal the integrand's is one polynomial identity in the two -- linear in the coefficients of `P`, one equation per monomial `x^i L^j`. The exponent may hold the logarithm itself, as Hebisch's does; `h'` is `dh/dx + dh/dL / x` and goes into every column. The denominator is tried from the integrand's: its `x`-part as the exponential ansatz tries its denominators, times `L^k` for every `k` from zero up to the written power, smallest first so that the answer carries no common factor. The columns are built one monomial at a time, each candidate's powers of `L` folded into one before differentiating -- the quotient rule on `L/L` left `(L - L)/L^2` behind, which nothing read -- and cleared by one common denominator. The identity is exact, so a solution is an answer and its absence a decline: `e^x ln(x)` and `e^x/ln(x)` have no such `P` and stay declined, and the derivative of what comes out is checked against the integrand at sampled points all the same. Every answer differentiated back. Rubi corpus, 463-problem sample, on the same evening: master at #1294 353/463, 0 wrong, 0 timeouts, 85 s (measured) master at #1295 356/463 (#1295's own +3) with this 358/463, 0 wrong, 0 timeouts, 86 s Two more, nothing lost: Hearn's and Hebisch's above. 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
…factors differ, and a rational function offers only the powers of x its exponents allow (#1298) Welz's `1/((1 + x^2)^2 sqrt(x^2 - 1))` had no antiderivative. Euler's first substitution turns it into `16 t^3 (t^2 - 1)/((t^4 + 6t^2 + 1)^2 (t^2 - 1))` -- with the common factor written `(2t)^2 - 2(t^2 + 1)` above and `2t^2 - (t^2 + 1)` below, one twice the other, which the cancellation by written factors cannot see. The degree read off the uncancelled quotient was ten, the bound is eight, and the rule declined. The gcd of the two sides as polynomials cancels it; taken only where the bound would otherwise refuse the quotient, since the gcd hands back expanded sides and the rational integrator does better with the written ones, and only where the uncancelled degree is within twice the bound -- the gcd of two degree-thirty polynomials with the coefficients `(3 - 2x + x^2)^(11/2)` produces did not return in ninety seconds, where the bound alone had declined that integrand in a moment. That last one was the first draft's timeout. What the cancellation lets through then met the substitution rule, at every level below: a degree-eight rational function in `t` has `t^3`, `t^4`, `t^5`, `t^6`, `t^7` as candidates for `u = x^k`, each one simplification of the quotient, one to two seconds apiece, and Timofeev's `(1 + x^4)/((1 + x + x^2) sqrt(2 + x + x^2))` spent thirteen of its fourteen seconds that way. For a rational function `u = x^k` is exact only when every exponent below the bar is a multiple of `k` and every one above is `k - 1` more than one, the `x^(k-1)` of `du`; the candidate is read off the exponents first, and the base of a written power is offered only for a polynomial, where `x (x^2 + 1)^3` wants it, and not below the bar of a quotient, where partial fractions have it anyway. Timofeev's takes one second. ## Measured Every answer differentiated back. Rubi corpus, 463-problem sample, on the same evening: master at #1294 353/463, 0 wrong, 0 timeouts, 85 s (measured) master at #1295 356/463 (#1295's own +3) with this 361/463, 0 wrong, 0 timeouts, 76 s Five more, nothing lost, and the wall clock nine seconds shorter: Welz's `1/((1 + x^2)^2 sqrt(x^2 - 1))` and `1/((3x^2 - 4)^2 sqrt(x^2 - 1))`, Timofeev's `(1 + x^4)/((1 + x + x^2) sqrt(2 + x + x^2))`, and Charlwood's `ln(1 + x sqrt(1 + x^2))` and `arctan(sqrt(1 + x) - sqrt(x))`, whose by-parts remainders the cancellation reaches. 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
… for any b
Welz's `(x + sqrt(b + x^2))^a` had no antiderivative, and neither had `sqrt(x + sqrt(a^2 + x^2))/x`
or Bondarenko's `1/(1 + sqrt(x + sqrt(1 + x^2)))`: a power, symbolic or fractional, of
`x + sqrt(Q)` is neither a rational function of the root nor a radical any substitution
reads. But `x + sqrt(Q)` is Euler's first substitution variable itself, `t = sqrt(Q) + x`,
so the power is `t^b` exactly and for any `b`; and `x - sqrt(Q)` is the same
substitution with the root's sign flipped -- the same `x(t)`, `sqrt(Q) = x - t` in place
of `t - x`, `t = x - sqrt(Q)` on the way back -- so `(x - sqrt(Q))^b` is `t^b` too. Both
signs in one integrand are neither, and are declined.
What the substitution leaves is not a quotient of polynomials, so it goes to the
chain in `t` rather than to the rational integrator: `t^a` times Laurent monomials for
Welz's, which the power rule answers term by term, and a rational function of
`sqrt(t)` for Bondarenko's, which the linear-radical substitution answers. Before it
goes, the powers of `t` with an exponent that is not a whole number are set aside
and the two polynomials left are cancelled by their gcd -- `1/sqrt(Q)` brings `t^2 + c`
below the bar and `dx/dt` brings it above, in two spellings nothing later cancels;
`(x - sqrt(a + x^2))^b/sqrt(a + x^2)` is `-t^(b-1)` after that and was declined before it.
Every answer differentiated back with the parameters pinned; the flipped-sign
answers are complex at real points and compared as such.
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 362/463, 0 wrong, 0 timeouts, 92 s
Seven more, nothing lost: Welz's `(x + sqrt(b + x^2))^a`, `(x - sqrt(a + x^2))^b`,
`(x - sqrt(a + x^2))^b/sqrt(a + x^2)`, `sqrt(x + sqrt(a^2 + x^2))/sqrt(a^2 + x^2)`,
`sqrt(x + sqrt(a^2 + x^2))/x` and `1/(x sqrt(a^2 + x^2) sqrt(x + sqrt(a^2 + x^2)))`, and
Bondarenko's `1/(1 + sqrt(x + sqrt(1 + x^2)))`. The harness counts five of them and
lists the two flipped-sign ones as "not checkable on the reals", which is what they
are: complex at every real sample point, with the parameters it pins. The probe,
which compares complex values, verifies both.
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
…a root gathers with a whole power of its own base (#1300) 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. 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
… for any b (#1299) Welz's `(x + sqrt(b + x^2))^a` had no antiderivative, and neither had `sqrt(x + sqrt(a^2 + x^2))/x` or Bondarenko's `1/(1 + sqrt(x + sqrt(1 + x^2)))`: a power, symbolic or fractional, of `x + sqrt(Q)` is neither a rational function of the root nor a radical any substitution reads. But `x + sqrt(Q)` is Euler's first substitution variable itself, `t = sqrt(Q) + x`, so the power is `t^b` exactly and for any `b`; and `x - sqrt(Q)` is the same substitution with the root's sign flipped -- the same `x(t)`, `sqrt(Q) = x - t` in place of `t - x`, `t = x - sqrt(Q)` on the way back -- so `(x - sqrt(Q))^b` is `t^b` too. Both signs in one integrand are neither, and are declined. What the substitution leaves is not a quotient of polynomials, so it goes to the chain in `t` rather than to the rational integrator: `t^a` times Laurent monomials for Welz's, which the power rule answers term by term, and a rational function of `sqrt(t)` for Bondarenko's, which the linear-radical substitution answers. Before it goes, the powers of `t` with an exponent that is not a whole number are set aside and the two polynomials left are cancelled by their gcd -- `1/sqrt(Q)` brings `t^2 + c` below the bar and `dx/dt` brings it above, in two spellings nothing later cancels; `(x - sqrt(a + x^2))^b/sqrt(a + x^2)` is `-t^(b-1)` after that and was declined before it. Every answer differentiated back with the parameters pinned; the flipped-sign answers are complex at real points and compared as such. 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 362/463, 0 wrong, 0 timeouts, 92 s Seven more, nothing lost: Welz's `(x + sqrt(b + x^2))^a`, `(x - sqrt(a + x^2))^b`, `(x - sqrt(a + x^2))^b/sqrt(a + x^2)`, `sqrt(x + sqrt(a^2 + x^2))/sqrt(a^2 + x^2)`, `sqrt(x + sqrt(a^2 + x^2))/x` and `1/(x sqrt(a^2 + x^2) sqrt(x + sqrt(a^2 + x^2)))`, and Bondarenko's `1/(1 + sqrt(x + sqrt(1 + x^2)))`. The harness counts five of them and lists the two flipped-sign ones as "not checkable on the reals", which is what they are: complex at every real sample point, with the parameters it pins. The probe, which compares complex values, verifies both. 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.
cos(x)/(sin(x)(2 + sin(2x)))had no antiderivative. Its arguments unified, it iscos/(2 sin + 2 sin^2 cos), and the third of Bioche's rules declined it: thedenominator has terms of degree one and three, and the rule read "homogeneous" as
"every term of the same degree". A term two degrees short of the highest is the
same term times
sin^2 + cos^2, which is one, sosin + sin^2 cosissin (sin^2 + cos^2) + sin^2 cos, of degree three throughout, and the substitutiont = tan(x)turns the quotient into the rational function it always was. The readerlifts every term to the highest degree that way where the degrees share a parity;
a term an odd number short is a genuine boundary, since no power of one bridges it,
and stays declined.
Measured
Every answer differentiated back.
Rubi corpus, 463-problem sample, against the master it was cut from (#1292), both
measured on the same evening:
One more, nothing lost: Timofeev's
cos(x)/(sin(x)(2 + sin(2x))).Part of #718.
🤖 Generated with Claude Code
https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura