Repository navigation
Factor was throwing the content away with an irreducibility proof - #1059
Merged
Rafael-SOWNet merged 1 commit intoAug 25, 2026
Merged
Rafael-SOWNet merged 1 commit into
Rafael-SOWNet merged 1 commit into
Conversation
…with it
Kronecker's substitution does not merely fail to find a factorisation -- it
proves there is none. A splitting of the polynomial into two parts of positive
degree in the main variable maps to a splitting of the one-variable image,
because the substitution is a ring homomorphism on the monomials that can
appear, and every splitting of the image is one of the subsets the
recombination tries. So where nothing recombines, nothing exists.
That proof was being reported as null, and the content went with it:
x * y + y * z was null, is y * (x + z)
a * x + a * y + a * z was null, is a * (x + y + z)
x ^ 2 * y - y ^ 3 was null, is y * (x + y) * (x - y)
The content had already been taken out and the factorisation assembled; the
single-factor rest then threw the whole thing away. It also disagreed with the
one-variable path, where Factor("x ^ 2 + 1", "x") has always been x ^ 2 + 1,
so x ^ 2 + y ^ 2, x ^ 2 - a and x * y + z now answer the same way.
The proof has a precondition, and it is now checked rather than assumed.
DivideExact answers null both for "does not divide" and for "ran out of room",
and only the first is evidence -- so it says which, and the irreducibility
claim is withheld where a division was cut short by a term or degree budget.
Where FromImage cannot read a candidate back the recombination now refuses
instead of skipping it silently, since a skipped candidate is a subset that was
never tried and the proof is over all of them.
The XML documentation on Factor still said "Univariate only", with a worked
example asserting that Factor("x * y + y", "x") is null. That has been false
since #1053 and is public API documentation, which nothing in the suite or in
the docsamples harness reads.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Bjumi5K7fg8yx6UK1mZTQd
Rafael-SOWNet
added a commit
that referenced
this pull request
Aug 26, 2026
…ot reach (#1087) `Factor` in several variables is Kronecker's substitution, and its one-variable image has degree `Π (d_i + 1) - 1` -- a product, so it leaves the one-variable factoriser's reach after very few variables. `x2 + y2 + z2 + w2 + 1` needs an image of degree 80 against a ceiling of 32, and the answer was `null`. Evaluating instead of substituting gives an image of degree `d_main`, whatever the variable count. That image cannot be lifted back to a factorisation without Hensel lifting, which is still outstanding -- but it does not need to be for one conclusion. Substitution is a ring homomorphism, so `f = g*h` gives `f(x,a) = g(x,a)*h(x,a)`; degrees in the main variable add, so if the image kept the total then neither part lost any. **An irreducible image of full degree is therefore a proof that its source is irreducible**, and since #1059 that is an answer rather than a refusal. One direction only, and the tests are mostly about the direction it does not claim. A reducible image says nothing at all -- `x2 + y` is irreducible and its image at y = -4 is `(x-2)(x+2)` -- so several points are tried and `x7 - y7` is still refused. A factor free of the main variable is invisible to an image in that variable, so the content is computed and anything but a constant declines, or `y * (x + 1)` would be certified on an image of `2x + 2`. The `true` half is the one nothing downstream can check: a factorisation is verified by division and "there is no factorisation" is not. So seventeen of the twenty-three tests assert that a certificate is *not* issued, and every case in them is written as a product or is a difference of like powers -- reducible by construction, whatever a factoriser would say. The count in the positive test is what stops all of that passing vacuously: a certificate that always declined would satisfy every one of them. Asked second, after the substitution refuses, because the substitution is the one that can actually factor and this only ever says that there is nothing to find. This is the first step of Hensel lifting with an evaluation homomorphism -- choosing a point whose image keeps the degree -- used for the conclusion that needs no lifting. The lifting itself is unchanged and still outstanding on #746 tier 1. Claude-Session: https://claude.ai/code/session_01Bjumi5K7fg8yx6UK1mZTQd 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
2 participants
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.
Kronecker's substitution does not merely fail to find a factorisation — it proves there is none. A splitting of the polynomial into two parts of positive degree in the main variable maps to a splitting of the one-variable image, because the substitution is a ring homomorphism on the monomials that can appear; and every splitting of the image is one of the subsets the recombination tries. So where nothing recombines, nothing exists.
That proof was being reported as
null, and the content went out with it.Factor("x * y + y * z", "x")nully * (x + z)Factor("a * x + a * y + a * z", "x")nulla * (x + y + z)Factor("x ^ 2 * y - y ^ 3", "x")nully * (x + y) * (x - y)Factor("x ^ 2 + y ^ 2", "x")nullx ^ 2 + y ^ 2Factor("x * y + z", "x")nullx * y + zFactor("x ^ 2 - a", "x")nullx ^ 2 - aFactor("x + y", "x")nullx + yThe first three are the real loss: the content had already been taken out and the factorisation assembled, and then the single-factor rest threw the whole thing away. The rest are a contract that disagreed with itself — the one-variable path has always answered
Factor("x ^ 2 + 1", "x")withx ^ 2 + 1.The proof has a precondition, and it is now checked
DivideExactanswersnullboth for "does not divide" and for "ran out of room" — a term count past its budget, a monomial past the degree bound, the step limit — and only the first is evidence. Drawing "irreducible" from the second would be stating exhaustion as a mathematical fact.So it says which, through a new overload, and the irreducibility claim is withheld where any trial division was cut short. Where
FromImagecannot read a candidate back the recombination now refuses rather than skipping it, because a skipped candidate is a subset that was never tried and the proof is over all of them.The documentation was two PRs stale
The XML doc on
MathS.Polynomials.Factorstill read "Univariate only. A polynomial in more than one variable is refused rather than answered", with a worked example assertingFalse since #1053, and it is public API documentation — nothing in the suite reads it, and the
docsamplesharness checks the wiki and the website rather than XML comments. Rewritten and every printed value in it re-measured.The existing
FactorisationRefusesRatherThanReturningTheInputtheory kept three rows that are now proofs rather than refusals; those moved to the new theory, and the test keeps the rows where a refusal is still right — not a polynomial, and past the degree bound.Full suite:
Failed: 0, Passed: 8591, Skipped: 14, Total: 8605.🤖 Generated with Claude Code
https://claude.ai/code/session_01Bjumi5K7fg8yx6UK1mZTQd