A perfect square written with symbols is read as one - #1477
Merged
Merged
Conversation
`(A + B x)(d + e x)/(a^2 + 2 a b x + b^2 x^2)^(5/2)` was left as written, though the radicand is `(a + b x)^2` and the power is `|a + b x|^5`. Three conditions said no, and each is a different kind of mistake: The discriminant `4 a^2 b^2 - 4 a^2 b^2` is a zero `InnerSimplified` does not collect, so a guard asking what it evaluates to read the square as an ordinary quadratic. The leading coefficient `b^2` is not a number, though it is positive for a real parameter -- `IsPositiveForARealParameter` is the library's own answer to that, and the condition `b^2 > 0` travels with the answer as it does elsewhere. And the rule's bound on how large a radicand it reads, which is there so that it costs nothing at every level of the descent, is lifted at the top only: there any half-odd power of a square is the power of the modulus, while below it the square root alone is safe, a sign written for a substitution's variable being a factor the rest of the search has to carry. The sign goes in front of the integral rather than into the integrand. Left inside, a rule below differentiates it: `sqrt(a^2 + 2abx + b^2x^2) sqrt(c + ex + dx^2)` threw `CannotEvalException: derivative(sgn(...))`, which the corpus found and no probe had. Family 1 of the Rubi suite: 156 -> 158 of 228, 0 wrong, 0 error; family 6 377/417 and the 1774-problem suite 1707 unchanged. Suite 12665 passed; allocation gate passed on all 19 gated benchmarks. Part of #718. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura
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.
(A + B x)(d + e x)/(a^2 + 2 a b x + b^2 x^2)^(5/2)was left as written, though the radicand is(a + b x)^2and the power is|a + b x|^5. Three conditions said no, and they are three different kinds of mistake:4 a^2 b^2 - 4 a^2 b^2is a zeroInnerSimplifieddoes not collect, so the guard read the square as an ordinary quadratic. (Third instance of this shape tonight, after An exponential times a trigonometric at the same frequency no longer divides by zero, and a phase is expanded #1472 and A symbolic constant factor no longer stops the rounds of parts #1473.)b^2is not one, but it is positive for a real parameter —IsPositiveForARealParameteris the library's own answer to that, and its conditionb^2 > 0travels with the answer as it does elsewhere. Requiring positivity is right; requiring a literal is not.a^2 + 2abx + b^2x^2is over it. Lifted at the top, where the rule may work harder; below it, the square root only, for the reason A power of x beside a function of a symbolic power of x is integrated by substituting the power, and a square root of a perfect square is the modulus at every depth #1462 measured (a sign written for a substitution's variable is a factor the rest of the search carries:(1 + 2u + u^2)^(5/2)underu = e^(2x)cost twenty seconds).And one defect the corpus found that no probe of mine had: with the sign written into the integrand, a rule below differentiates it, and
sqrt(a^2 + 2abx + b^2x^2) sqrt(c + ex + dx^2)threwCannotEvalException: derivative(sgn(...)). The first measured run of this change reported 1 error where there had been none. The sign now goes in front of the integral, which is what every rule here that writes one does, and that row answers in half a second.Measured (final build):
familycap.sh 1 6): 156 → 158/228, 0 wrong, 0 error — 1.2.1.3:2008 and 1.2.1.6:99; one row moved Unsolved → Timeout at the 5 s cap ((d + ex)^(9/2)/(a^2 + 2abx + b^2x^2)^(3/2), which is a new answer path rather than a loss).bench.sh: PASSED on all 19 gated benchmarks.Part of #718.
🤖 Generated with Claude Code
https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura