Repository navigation
A biquadratic denominator is decomposed over the reals (#233) - #1145
Merged
Merged
Conversation
Both existing partial fraction steps factor over Q and stop where Q does, so `x^4 + 1` -- irreducible over the rationals -- was left whole and `x^2/(x^4 + 1)` came back unevaluated. Over the reals it is `(x^2 - sqrt(2)x + 1)(x^2 + sqrt(2)x + 1)`, and both halves are read by the rule for a linear numerator over a quadratic. Nothing was missing but a factorisation the rational step is right to refuse. `1/(x^4 + 1)`, `1/(x^4 - 2)`, `1/(x^4 + 3x^2 + 1)` and `(x^3 + 1)/(x^4 + 1)` come with it. This is the fourth of the five integrals #233 lists. Biquadratic only, and that is a boundary rather than a first cut: a general quartic factors into real quadratics through its resolvent cubic, whose roots carry Cardano's nested radicals, while `x^4 + px^2 + q` is the case where the resolvent is solvable by inspection and both factors stay inside one square root. The sign of `p^2 - 4q` picks the shape -- negative gives `(x^2 + ax + b)(x^2 - ax + b)`, positive the even `(x^2 + u)(x^2 + v)`, zero a repeated quadratic that is declined for the reason the step above declines one. Each split is closed form rather than a linear solve. Tried last, after both rational steps, so a denominator that factors over Q is still taken apart in exact arithmetic and never given a square root it does not need. Declining stays as cheap as it was: every guard is rational arithmetic on coefficients already read, and `(1 - x^4)/(1 + x^4 + x^8)` returns the same unevaluated integral in the same fraction of a second. Two identities are checked rather than one, because here the factorisation is a claim of its own rather than exact by construction -- a wrong term common to both factors cancels between the halves of the numerator identity and passes it, while the denominator identity sees it. Three tests recorded `x^2/(x^4 + 1)` as declined and now record it as answered. Two of them are about other code -- the power substitution still rejects it, and should -- so they keep their subject and take a witness with an odd power, which is out of reach of this step as well. A test that something is declined stops testing its own subject the moment any other capability answers the case. `sqrt(tan(x))`, the last entry on #233's list, is not answered by this. It reduces under `u = sqrt(tan x)` to `2 * integral(u^2/(u^4 + 1), u)`, which is now integrable, but the substitution that gets there is a separate capability. Part of #233. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura
Rafael-SOWNet
added a commit
that referenced
this pull request
Sep 2, 2026
Two substitutions, in one change because neither reaches `sqrt(tan(x))` without the other. That integral is the last of the five #233 lists, and the one it calls "very painful, requires different solvers", which it is: int sqrt(tan(x)) dx u = tan(x), dx = du/(1 + u^2) -> int sqrt(u)/(1 + u^2) du t = sqrt(u), a fractional power -> int 2t^2/(1 + t^4) dt 1 + t^4 factored over the reals -> logarithms and arctangents Take any one of the three away and it comes back unevaluated. The third landed in #1145. The fractional power. A power substitution rewrites the other powers of the variable into powers of itself: for `u = x^r` the identity is `x^n = u^(n/r)`, applied wherever `n/r` is whole. A whole `r` reaches only the powers it divides, which is all this did before; an `r` of `1/2` reaches every one of them, the bare `x` included, which a whole `r` never can. So `int sqrt(x)/(1 + x^2)` becomes `int 2u^2/(1 + u^4) du`, and `1/(1 + sqrt(x))`, `1/(sqrt(x) * (1 + x))`, `1/(sqrt(x) * (1 + x^2))` and `1/(sqrt(x) + x)` come with it. The rewrite takes two passes, written powers first and a leftover bare `x` second, because the tree is rewritten from the leaves up: in one pass the `x` inside `sqrt(x)` is reached before the `sqrt(x)` node is, and `u = sqrt(x)` turns it into `sqrt(u^2)` rather than `u` -- an integrand free of `x` and no more integrable than it started. The tangent. An integrand that is a function of `tan(x)` and of nothing else becomes a rational function under `u = tan(x)`, with `dx` as `du/(1 + u^2)`. The test is the rewrite itself: replace every `tan(x)` and see whether an `x` survives. It is a step of its own rather than a candidate for the general substitution. The general one divides by `du/dx` and asks what is left, which works while the substitution survives the division; here it does not, since `sqrt(tan(x))` over the derivative of `sqrt(tan(x))` is `2 tan(x) cos(x)^2`, which is `sin(2x)` and is simplified to it -- a correct answer to a question that has stopped being about the tangent. The corpus gate now reads 40 solved of 40. Its one unsolved problem was `int:hard`, which is `sqrt(tan(x))`, chosen for that list as the standing example of an integral out of reach; the gate reached the verdict by differentiating the answer back rather than by comparing it with anything. Baseline refreshed as its message directs. What is still declined is recorded in the tests rather than left to be inferred: `cotan` is its own node and not a reciprocal of the tangent, so `sqrt(cotan(x))` never starts; `tan(x)^2` and `tan(x)^3` become improper fractions, which the rational integrator does not divide out; `1/(1 + tan(x)^2)` becomes a repeated irreducible quadratic; and `sqrt(x)/(1 + x^4)` becomes a degree-eight denominator that is neither factorable over the rationals nor a biquadratic. All five integrals the issue lists are now solved. Not closing it: its title asks for more integral solvers generally, and that is broader than the five. Part of #233. Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura Co-authored-by: Claude Opus 5 <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.
Both existing partial fraction steps factor over
Qand stop whereQdoes, sox^4 + 1—irreducible over the rationals — was left whole and
x^2/(x^4 + 1)came back unevaluated. Overthe reals it is
(x^2 - sqrt(2)x + 1)(x^2 + sqrt(2)x + 1), and both halves are read by theexisting rule for a linear numerator over a quadratic. Nothing was missing but a factorisation
the rational step is right to refuse.
This is the fourth of the five integrals #233 lists, and the first of them to need a
factorisation rather than a rule.
1/(x^4 + 1),1/(x^4 - 2),1/(x^4 + 3x^2 + 1)and(x^3 + 1)/(x^4 + 1)come with it.Biquadratic only, and why that is a boundary rather than a first cut
A general quartic factors into real quadratics through its resolvent cubic, whose roots carry
Cardano's nested radicals. A biquadratic
x^4 + px^2 + qis the case where the resolvent issolvable by inspection and both factors stay inside a single square root. The sign of
p^2 - 4qpicks the shape:p^2 - 4q(x^2 + ax + b)(x^2 - ax + b),b = sqrt(q),a = sqrt(2b - p)x^4 + 1ata = sqrt(2),b = 1(x^2 + u)(x^2 + v),u, v = (p -+ sqrt(p^2 - 4q))/2x^4 - 2,x^4 + 3x^2 + 1(x^2 + p/2)^2— a repeated quadratic, declinedx^4 + 2x^2 + 1Each split is closed form. Matching coefficients gives two sums and two differences in the
first branch, and two independent pairs in the second, so neither needs a symbolic linear
solve. The zero case is declined for the reason the step above declines a repeated quadratic:
there is no rule for a numerator over
(x^2 + c)^k, so decomposing it ends in the integral itstarted from.
A quartic with an odd power in it is still declined —
x^4 + x^3 + 1,x^4 + x + 1— andso is anything of degree five and up that does not factor over
Q. Both are pinned by tests.Where it sits, and what it costs
Tried last, after both rational steps, so a denominator that factors over
Qis still takenapart in exact arithmetic and never given a square root it does not need:
x^4 + 3x^2 + 2isdecomposed by the step above and never reaches this one.
Declining stays as cheap as it was. Every guard is rational arithmetic on coefficients already
read, and the entity work happens only for a genuine biquadratic.
(1 - x^4)/(1 + x^4 + x^8)—the case the existing guard's comment records as 18s before that guard and 203ms after —
returns the same unevaluated integral in the same fraction of a second, and there is now a test
asserting it.
Two identity checks rather than one
The step above checks one identity because its factorisation is exact by construction. Here the
factors are built by matching coefficients through a square root, so the factorisation is a
claim of its own and is checked too.
They do not imply each other, which is worth stating because it is not obvious: a wrong term
present in both factors cancels between the two halves of the numerator identity and passes
it, while the denominator identity sees it immediately.
Three tests changed their verdict
x^2/(x^4 + 1)was recorded as declined in three places. It is now answered, so all threechange — but two of them are about other code and keep their subject rather than being
weakened:
PowerSubstitutionIntegralTest.AnIntegralThisDoesNotReachIsStillDeclinedasserts theu = x^2rewrite rejects the integrand. That is still true; the integrand simply stoppedbeing a witness once a neighbouring step began answering it. It now uses
x^2/(x^4 + x + 1)andx^2/(x^4 + x^3 + 1), which carry an odd power and so are out ofreach of this step as well.
RationalIntegralsTest.ADenominatorThatDoesNotFactorIsStillDeclinedlikewise.PartialFractionsTest.WhatCannotBeSplitIsLeftAlonedrops it and gains it as an answer.The general point, recorded in the tests: a test that something is declined stops testing its
own subject the moment any other capability answers the case. Only one of the three files was
about the code this changes.
Not in this change
sqrt(tan(x)), the last entry on #233's list, is not answered. It reduces underu = sqrt(tan x)to2 * integral(u^2/(u^4 + 1), u), which is now integrable — but thesubstitution that gets there is a separate capability and is not built here.
Verification
Full suite: 9324 passed, 0 failed, 14 skipped. Every new answer is checked by
differentiating it back and comparing at four points, through the file's existing helper, which
asserts the antiderivative contains no
integral(before comparing — without that guard thecheck passes vacuously, since
d/dxof an unevaluatedintegral(f, x)isf.BREAKING-CHANGES.mdcarries the entry, and corrects the #919 entry in place: it namesx^4 + 1as still declined, which this makes false.Part of #233.