Repository navigation
The third trigonometric substitution, and the sign that makes its second interval right - #1277
Merged
Merged
Conversation
…ond interval right `sqrt(9*x^2 - 1)/x^2`, `1/(x^3*sqrt(x^2 - 16))` and `(x^2 - 10)^(5/2)/x` had no antiderivative. #1273 shipped the tangent and sine substitutions and left this one out, saying its domain is two intervals rather than one and that the answer owed a condition it did not write. That was the right call at the time and the condition turns out not to be what it needs. A > 0, c > 0 y = r tan(t) -> sin^m cos^(-m-k-2) one interval, all of R A > 0, c < 0 y = r sin(t) -> sin^m cos^(k+1) one interval, between the roots A < 0, c > 0 y = r sec(t) -> sin^(k+1) cos^(-m-k-2) two intervals, outside them There is no fourth: both coefficients negative is a radicand negative everywhere, which has no real integrand to integrate, and it is declined. ## The sign, which took two attempts `(a tan(t)^2)^(k/2)` is `a^(k/2) |tan(t)|^k`, and `tan(t)` is negative for `t` in `(pi/2, pi)` -- which is where `y < -r` lands. Writing `tan(t)^k` there is wrong by a sign for odd `k`. The first attempt patched the three back-substitutions, putting an absolute value on `sin(t)` and a signum on `tan(t)`. That got `y > r` right and left **eight of thirteen** shapes still sign-reversed on the other side, because the sign it is wrong by depends on the power outside the radical as well and the three replacements do not compose into it. What is true without cases: the integrand `y^m (b y^2 - a)^(k/2)` is even or odd under `y -> -y` according to `m`, so an antiderivative `F` valid for `y > r` gives the whole answer as `sign(y)^(m+1) F(|y|)`. So everything is written in `|y|`, where the substitution's own interval is the principal one and every sign is positive, and the reflection is applied once at the end. Thirteen of thirteen. ## A whole power is not this substitution's, and that is correctness `(2*x + 3*x^2)^2` completes the square to a negative constant, so it reaches the secant branch -- and it is a **polynomial**, real on the whole line, where the substitution is defined only outside `|y| > r`. It came back with the sign reversed at `x = -0.5`. That is a wrong answer, not a missing condition, and the branch now takes only an odd half-power, where the integrand is a square root of something negative in the middle and so is undefined exactly where the substitution is. Caught by `ExpandedPowerIntegralTest`, which exists for that shape and fired. ## Measured Every case checked on **both** intervals -- two points above `r` and two below `-r`. An answer right only to the right of the gap passes a one-sided test, which is how the first attempt looked correct. master (5070a36) 5/13 answered, 0 wrong with it 13/13 answered, 0 wrong Rubi corpus, 463-problem sample, both arms in the foreground: master (5070a36) 255/463, 0 wrong, 3 timeouts, 158 s with it 257/463, 0 wrong, 3 timeouts, 158 s Two more, no timeout added, wall clock unmoved. The five test suites are green. `RootOverSquareIntegralsTest` pinned `1/(x^3*sqrt(x^2 - 1))` as unevaluated and it is now answered. That test is about its own formula rather than about the integrand, so it now says so and checks the answer instead of its absence -- the second case it pins is still unevaluated, since a negative power of the variable beside a quadratic with a linear term is outside this rule too. 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 11, 2026
…d it is the sign that kept them out (#1279) The table of standard integrals carries `arcsin`, `arccos`, `arctan` and `arccotan`, each of them integration by parts against 1 -- a shape the by-parts solver does not look for, since there is no product to split. The other two were missing. They are missing for a reason rather than by oversight. The four that are there have a derivative that is a function of `u` alone, so by parts leaves something the table already holds. `d/dx arcsec(u)` is `1/(|u| sqrt(u^2 - 1))`, so the `u` that by parts multiplies it by leaves sgn(u)/sqrt(u^2 - 1) rather than 1/sqrt(u^2 - 1) and the domain is `|u| >= 1`, two intervals. Without the `signum` the answer is right for `u > 1` and sign-reversed for `u < -1`: int arcsec(u) du = u arcsec(u) - sgn(u) ln|u + sqrt(u^2 - 1)| int arccsc(u) du = u arccsc(u) + sgn(u) ln|u + sqrt(u^2 - 1)| That is the third time today a two-interval domain has needed the sign written out rather than assumed -- #1277 is the same lesson for the secant substitution -- so every case in the test is checked on **both** intervals. An answer without the sign passes a one-sided test. ## Measured Each answer verified by differentiating back at five points, two of them below `-1`: master (b7ab36f) arcsec, arccsc: no antiderivative with it both, and with a linear argument Rubi corpus, 463-problem sample, both arms in the foreground: master (b7ab36f) 258/463, 0 wrong, 3 timeouts, 159 s with it 259/463, 0 wrong, 3 timeouts, 160 s 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 11, 2026
…ten answers
`int x arcsin(x) dx` was unanswered. By parts differentiates the arcsine into
something algebraic and leaves `int x^2/sqrt(1 - x^2) dx`, which is squarely what
against it. The reason is real and measured: a rule that answers a sub-integral
which used to come back unanswered lets the search that asked carry on into ground
that was always doomed, and the cost lands on integrands the rule never fires on.
`sec(x)^6*tan(x)^3` went from a 637 ms decline to not returning in 400 s that way.
**But that is a property of what the caller does with the answer, not of the
rule.** Where the sub-integral is one the caller *uses* -- by parts asks for
`int x^2/sqrt(1 - x^2)` and then builds its answer out of it -- the scope refuses
the one thing that would have finished the job.
Each of the five ungated on its own, same build, Rubi sample of 463, foreground:
| ungated | solved | timeouts | wall clock |
|---|--:|--:|--:|
| (all scoped, master) | 258 | 3 | 159 s |
| `SolveBySecantPowerReduction` | 258 | 3 | 160 s |
| `SolveByTrigonometricPowerSubstitution` | 258 | 3 | 159 s |
| `SolveABinomialDifferential` + `SolveAPolynomialTimesAnExponentialAndATrigonometric` | 259 | 3 | 158 s |
| **`SolveARadicalOfAQuadraticAsTrigonometric`** | **268** | 3 | 161 s |
One of the five, and only one. So the scope stays on the other four and comes off
this one, rather than a policy being changed for all of them on the strength of a
single measurement.
And it measures free. A probe of fourteen integrands that are declined either way
-- including `x tan(x)^3 sec(x)^4`, `1/(1 + sin(x)^3)` and
`(1 + x^4)/((1 + x + x^2) sqrt(2 + x + x^2))` -- totals **28.8 s scoped and 28.8 s
not**. The five test suites are green and the calculus suite is unmoved at 1m20.
master (b7ab36f) 258/463, 0 wrong, 3 timeouts, 159 s
with it 268/463, 0 wrong, 3 timeouts, 159 s
The rule's own summary said there were two substitutions and that the secant one
was "left out rather than guessed at". #1277 added it, and updated the helper's
documentation without updating this one. It now names all three, says what decides
between them, and says there is no fourth.
Scope answers **a rule whose answers are only ever a distraction**: something the
surrounding search would have stopped on, and now does not. It is the wrong
instrument for **a rule whose answers are what the caller was asking for**. The
four it remains on are power reductions and substitutions that answer an integrand
in its own terms; the one it comes off is the one integration by parts routinely
needs a level down. That is a question worth asking of each new rule rather than a
default to copy.
Part of #718. Part of #1265.
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 11, 2026
…ten answers (#1280) `int x arcsin(x) dx` was unanswered. By parts differentiates the arcsine into something algebraic and leaves `int x^2/sqrt(1 - x^2) dx`, which is squarely what against it. The reason is real and measured: a rule that answers a sub-integral which used to come back unanswered lets the search that asked carry on into ground that was always doomed, and the cost lands on integrands the rule never fires on. `sec(x)^6*tan(x)^3` went from a 637 ms decline to not returning in 400 s that way. **But that is a property of what the caller does with the answer, not of the rule.** Where the sub-integral is one the caller *uses* -- by parts asks for `int x^2/sqrt(1 - x^2)` and then builds its answer out of it -- the scope refuses the one thing that would have finished the job. Each of the five ungated on its own, same build, Rubi sample of 463, foreground: | ungated | solved | timeouts | wall clock | |---|--:|--:|--:| | (all scoped, master) | 258 | 3 | 159 s | | `SolveBySecantPowerReduction` | 258 | 3 | 160 s | | `SolveByTrigonometricPowerSubstitution` | 258 | 3 | 159 s | | `SolveABinomialDifferential` + `SolveAPolynomialTimesAnExponentialAndATrigonometric` | 259 | 3 | 158 s | | **`SolveARadicalOfAQuadraticAsTrigonometric`** | **268** | 3 | 161 s | One of the five, and only one. So the scope stays on the other four and comes off this one, rather than a policy being changed for all of them on the strength of a single measurement. And it measures free. A probe of fourteen integrands that are declined either way -- including `x tan(x)^3 sec(x)^4`, `1/(1 + sin(x)^3)` and `(1 + x^4)/((1 + x + x^2) sqrt(2 + x + x^2))` -- totals **28.8 s scoped and 28.8 s not**. The five test suites are green and the calculus suite is unmoved at 1m20. master (b7ab36f) 258/463, 0 wrong, 3 timeouts, 159 s with it 268/463, 0 wrong, 3 timeouts, 159 s The rule's own summary said there were two substitutions and that the secant one was "left out rather than guessed at". #1277 added it, and updated the helper's documentation without updating this one. It now names all three, says what decides between them, and says there is no fourth. Scope answers **a rule whose answers are only ever a distraction**: something the surrounding search would have stopped on, and now does not. It is the wrong instrument for **a rule whose answers are what the caller was asking for**. The four it remains on are power reductions and substitutions that answer an integrand in its own terms; the one it comes off is the one integration by parts routinely needs a level down. That is a question worth asking of each new rule rather than a default to copy. Part of #718. Part of #1265. 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 11, 2026
…e pinned verdict one of them falsifies `x/(a + b*x)` had no antiderivative. `x/(3 + 5*x)` did. Nine shapes from the Rubi sample were like that -- answered with a number in the coefficient, declined with a symbol -- and probing each in both spellings found three separate causes. A fourth gap, the nested radical `sqrt(x + sqrt(1 + x))`, is one word. The division declined a divisor whose leading coefficient was a symbol, because the quotient loses the value that makes it zero: `x/(a + b x)` divided out is undefined at `b = 0`. #1269 wrote that guard and its test pinned the decline as "the honest report". It was measured against the wrong neighbours. Every rule beside it gives the generic answer: int 1/(a x + b) dx = ln(a x + b) / a undefined at a = 0 int sin(a x) dx = -cos(a x) / a undefined at a = 0 int x^n dx = x^(n+1) / (n+1) undefined at n = -1 int (a x + b)^7 dx = (a x + b)^8 / (8 a) undefined at a = 0 The first of those divides by the very coefficient the guard refused to divide by. Long division was the one rule in the integrator holding out for a condition none of its neighbours carry. The guard is right for the simplifier, whose rewrite has to be an equivalence, and `PolynomialLongDivision` serves both. So it takes a `genericCase` flag: the integrator's two call sites pass it, the simplifier's rule set does not, and `Simplify` on `x/(a + b*x)` is unchanged. Item 18 of #180 is this integral, and it is answered; the piecewise with the degenerate branch beside it is a further step no neighbouring rule takes either. With that guard lifted, `a x^2/(b + a x)` still declined while `x^2/(b + a x)` came out. The division chose its variable as *whichever came first*, and with `a` in the numerator too that could be `a` -- dividing in the parameter gives `x - b x/(b + a x)`, true and useless, and it consumes the one attempt. The integrator now passes `inTermsOf: x`; a caller that does not say keeps the old choice. In the replaced pass the variable is behind a temporary, so the test there is that the subtree it stands for mentions the caller's variable. `x ln(b + a x)` is what this was for: by parts leaves exactly that fraction. `d^x cos(x)` came out and `d^x x cos(x)` did not, which named the polynomial read as the place. The exponential-times-trigonometric reader multiplies the polynomial part by the base to the constant part of the exponent, and with no constant part that was `MathS.Pow(d, 0)` written out -- folded away for a numeric base, left standing for a symbolic one, and enough to stop `TryPolynomial`. Nothing is multiplied in when there is nothing to multiply. The corpus then found `a^x/b^x` answered too: `a^0 b^0` had been standing in for the polynomial there. `SolveByLinearRadicalSubstitution` **refused** an integrand holding a radical over something not linear. `sqrt(x + sqrt(1 + x))` holds two: the inner one is what the substitution is for, and the outer one is over a sum containing it. With `u^2 = 1 + x` the outer radical is `sqrt(u^2 + u - 1)`, free of `x`, and the integrand is `2u sqrt(u^2 + u - 1)`, which the quadratic-radical rule answers. `return null` is now `continue`; the check that no `x` survives the substitution is what makes skipping safe. That exposed a latent defect in the quadratic-radical rule's back-substitution (#1273, #1277): `Replace` rewrites children before parents, so a bare `t` was substituted before its enclosing `tan(t)` could match, and the answer held `tan(arccos(...))` -- correct, and `EvalNumerical` throws on it. Two passes now, the trigonometric functions of `t` first. Every answer differentiated back, or -- for the secant-branch answers that carry a `sign`, which the library does not differentiate -- checked as `F(b) - F(a)` against Simpson's rule. Rubi corpus, 463-problem sample, this branch against the master it was cut from (6294e7a, without #1282 which is still open): master 271/463, 0 wrong, 3 timeouts, 169 s with it 278/463, 0 wrong, 3 timeouts, 173 s Seven more answered and nothing lost: `x/(a+b*x)`, `x*ln(b+a*x)`, `a^x/b^x`, `d^x*x*cos(x)`, `d^x*x^3*cos(x)` (Hearn); `1/(x-sqrt(1+sqrt(1+x)))`, `sqrt(1+x)/(x+sqrt(1+sqrt(1+x)))` (Bondarenko). An eighth, `x/(x+sqrt(1-sqrt(1+x)))`, now answers and is complex at every real sample point, which the harness reports as unverifiable rather than solved. `ImproperFractionIntegralTest.ASymbolicLeadingCoefficientIsDeclined` recorded the gap and is now `...IsDividedOut`, with the reasoning that changed written against it. The five test suites are green. Part of #718. Part of #180. 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 11, 2026
…e pinned verdict one of them falsifies (#1283) `x/(a + b*x)` had no antiderivative. `x/(3 + 5*x)` did. Nine shapes from the Rubi sample were like that -- answered with a number in the coefficient, declined with a symbol -- and probing each in both spellings found three separate causes. A fourth gap, the nested radical `sqrt(x + sqrt(1 + x))`, is one word. The division declined a divisor whose leading coefficient was a symbol, because the quotient loses the value that makes it zero: `x/(a + b x)` divided out is undefined at `b = 0`. #1269 wrote that guard and its test pinned the decline as "the honest report". It was measured against the wrong neighbours. Every rule beside it gives the generic answer: int 1/(a x + b) dx = ln(a x + b) / a undefined at a = 0 int sin(a x) dx = -cos(a x) / a undefined at a = 0 int x^n dx = x^(n+1) / (n+1) undefined at n = -1 int (a x + b)^7 dx = (a x + b)^8 / (8 a) undefined at a = 0 The first of those divides by the very coefficient the guard refused to divide by. Long division was the one rule in the integrator holding out for a condition none of its neighbours carry. The guard is right for the simplifier, whose rewrite has to be an equivalence, and `PolynomialLongDivision` serves both. So it takes a `genericCase` flag: the integrator's two call sites pass it, the simplifier's rule set does not, and `Simplify` on `x/(a + b*x)` is unchanged. Item 18 of #180 is this integral, and it is answered; the piecewise with the degenerate branch beside it is a further step no neighbouring rule takes either. With that guard lifted, `a x^2/(b + a x)` still declined while `x^2/(b + a x)` came out. The division chose its variable as *whichever came first*, and with `a` in the numerator too that could be `a` -- dividing in the parameter gives `x - b x/(b + a x)`, true and useless, and it consumes the one attempt. The integrator now passes `inTermsOf: x`; a caller that does not say keeps the old choice. In the replaced pass the variable is behind a temporary, so the test there is that the subtree it stands for mentions the caller's variable. `x ln(b + a x)` is what this was for: by parts leaves exactly that fraction. `d^x cos(x)` came out and `d^x x cos(x)` did not, which named the polynomial read as the place. The exponential-times-trigonometric reader multiplies the polynomial part by the base to the constant part of the exponent, and with no constant part that was `MathS.Pow(d, 0)` written out -- folded away for a numeric base, left standing for a symbolic one, and enough to stop `TryPolynomial`. Nothing is multiplied in when there is nothing to multiply. The corpus then found `a^x/b^x` answered too: `a^0 b^0` had been standing in for the polynomial there. `SolveByLinearRadicalSubstitution` **refused** an integrand holding a radical over something not linear. `sqrt(x + sqrt(1 + x))` holds two: the inner one is what the substitution is for, and the outer one is over a sum containing it. With `u^2 = 1 + x` the outer radical is `sqrt(u^2 + u - 1)`, free of `x`, and the integrand is `2u sqrt(u^2 + u - 1)`, which the quadratic-radical rule answers. `return null` is now `continue`; the check that no `x` survives the substitution is what makes skipping safe. That exposed a latent defect in the quadratic-radical rule's back-substitution (#1273, #1277): `Replace` rewrites children before parents, so a bare `t` was substituted before its enclosing `tan(t)` could match, and the answer held `tan(arccos(...))` -- correct, and `EvalNumerical` throws on it. Two passes now, the trigonometric functions of `t` first. Every answer differentiated back, or -- for the secant-branch answers that carry a `sign`, which the library does not differentiate -- checked as `F(b) - F(a)` against Simpson's rule. Rubi corpus, 463-problem sample, this branch against the master it was cut from (6294e7a, without #1282 which is still open): master 271/463, 0 wrong, 3 timeouts, 169 s with it 278/463, 0 wrong, 3 timeouts, 173 s Seven more answered and nothing lost: `x/(a+b*x)`, `x*ln(b+a*x)`, `a^x/b^x`, `d^x*x*cos(x)`, `d^x*x^3*cos(x)` (Hearn); `1/(x-sqrt(1+sqrt(1+x)))`, `sqrt(1+x)/(x+sqrt(1+sqrt(1+x)))` (Bondarenko). An eighth, `x/(x+sqrt(1-sqrt(1+x)))`, now answers and is complex at every real sample point, which the harness reports as unverifiable rather than solved. `ImproperFractionIntegralTest.ASymbolicLeadingCoefficientIsDeclined` recorded the gap and is now `...IsDividedOut`, with the reasoning that changed written against it. The five test suites are green. Part of #718. Part of #180. 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.
sqrt(9*x^2 - 1)/x^2,1/(x^3*sqrt(x^2 - 16))and(x^2 - 10)^(5/2)/xhad noantiderivative. #1273 shipped the tangent and sine substitutions and left this one
out, saying its domain is two intervals rather than one and that the answer owed a
condition it did not write. That was the right call at the time and the condition
turns out not to be what it needs.
There is no fourth: both coefficients negative is a radicand negative everywhere,
which has no real integrand to integrate, and it is declined.
The sign, which took two attempts
(a tan(t)^2)^(k/2)isa^(k/2) |tan(t)|^k, andtan(t)is negative fortin(pi/2, pi)-- which is wherey < -rlands. Writingtan(t)^kthere is wrong bya sign for odd
k.The first attempt patched the three back-substitutions, putting an absolute value
on
sin(t)and a signum ontan(t). That goty > rright and left eight ofthirteen shapes still sign-reversed on the other side, because the sign it is
wrong by depends on the power outside the radical as well and the three
replacements do not compose into it.
What is true without cases: the integrand
y^m (b y^2 - a)^(k/2)is even or oddunder
y -> -yaccording tom, so an antiderivativeFvalid fory > rgivesthe whole answer as
sign(y)^(m+1) F(|y|). So everything is written in|y|,where the substitution's own interval is the principal one and every sign is
positive, and the reflection is applied once at the end. Thirteen of thirteen.
A whole power is not this substitution's, and that is correctness
(2*x + 3*x^2)^2completes the square to a negative constant, so it reaches thesecant branch -- and it is a polynomial, real on the whole line, where the
substitution is defined only outside
|y| > r. It came back with the sign reversedat
x = -0.5. That is a wrong answer, not a missing condition, and the branch nowtakes only an odd half-power, where the integrand is a square root of something
negative in the middle and so is undefined exactly where the substitution is.
Caught by
ExpandedPowerIntegralTest, which exists for that shape and fired.Measured
Every case checked on both intervals -- two points above
rand two below-r. An answer right only to the right of the gap passes a one-sided test, whichis how the first attempt looked correct.
Rubi corpus, 463-problem sample, both arms in the foreground:
Two more, no timeout added, wall clock unmoved. The five test suites are green.
RootOverSquareIntegralsTestpinned1/(x^3*sqrt(x^2 - 1))as unevaluated and itis now answered. That test is about its own formula rather than about the
integrand, so it now says so and checks the answer instead of its absence -- the
second case it pins is still unevaluated, since a negative power of the variable
beside a quadratic with a linear term is outside this rule too.
Part of #718.
🤖 Generated with Claude Code
https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura