Skip to content

Polynomial long division carries its divisor's domain (#1174) - #1177

Merged
Rafael-SOWNet merged 1 commit into
masterfrom
zero-over-undefined
Sep 5, 2026
Merged

Rafael-SOWNet merged 1 commit into
masterfrom
zero-over-undefined

Conversation

@Rafael-SOWNet

Copy link
Copy Markdown
Member

n / d = quotient + remainder is only the quotient where d has a value. ln(x) / ln(x) divides out
to 1 + 0 / ln(x), which is 1 at x = 0 while the quotient it came from is undefined there —
ln(0) is a pole, and the remainder term carries only ln(x) != 0.

"ln(x) / ln(x)".Simplify()   was  1 provided not ln(x) = 0                 at x = 0: 1
                             is   1 provided not ln(x) = 0 and not x = 0   at x = 0: NaN

Closes #1174.

Why #1176 did not close it

#1176 corrected all seven cancellation-rule sites, and afterwards every registered set answered
correctly when asked directly:

Common / Power / CommonDenominator (+2 variants)  ->  1 provided not ln(x) = 0 and not x = 0
PolynomialLongDivision                            ->  0 + 1 + 0 / ln(x)

The public API still said 1, because this rewrite produced a shorter candidate and Simplify rated
it best. A rule being right is not the same as the answer being right, and only asking the entry
point tells them apart — which is why that PR said the issue stayed open rather than closing it.

Ordinary divisions are untouched

That is the whole reason this is safe: a divisor that cannot be undefined has a domain condition of
True, and it folds away.

(x^2 - 1) / (x - 1)        ->  x + 1 provided not x - 1 = 0        unchanged
(x^3 + 1) / (x + 1)        ->  x ^ 2 - x + 1 provided not x + 1 = 0  unchanged
(x^2 + 2*x + 1) / (x + 1)  ->  1 + x provided not 1 + x = 0        unchanged
x^2 / x, x^3 / x^2         ->  x provided not x = 0                unchanged

One recorded test moves

x!/x! now carries the factorial's domain instead of not x! = 0 — the same change
(x + 1)!/(x + 1)! took in #1176. That one went through a cancellation rule and this one through this
rewrite, which is why they moved a commit apart; the note in SimplifyTest that called the
difference out is updated rather than left describing a state that lasted one commit.

Measured at x = -4, -3, -2, -1, 0, 1, 3, 1/2 and -1/2: the old condition and the new one agree with
the unsimplified quotient at every point — NaN at the four gamma poles and 1 elsewhere. So the
printed form moves and the value does not. Recorded in BREAKING-CHANGES.md.

Both spellings changed together, MatchedRules and Patterns.cs.

Checks

Full suite 9560 passed, 0 failed, 14 skipped.

🤖 Generated with Claude Code

https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura

`n / d = quotient + remainder` is only the quotient where d has a value.
`ln(x) / ln(x)` divides out to `1 + 0 / ln(x)`, which is 1 at x = 0 while the
quotient it came from is undefined there -- ln(0) is a pole, and the remainder
term carries only `ln(x) != 0`. Closes #1174.

This was the candidate Simplify actually rated best, so it is what a caller
saw. #1176 corrected the seven cancellation-rule sites and every registered
set then answered `1 provided not ln(x) = 0 and not x = 0` -- and the public
API still said 1, because this rewrite produced a shorter candidate that won.
A rule being right is not the same as the answer being right, and only asking
the entry point tells them apart.

    ln(x) / ln(x)          1 provided not ln(x) = 0 and not x = 0    NaN at 0
    log(2, x) / log(2, x)  1 provided not x = 0 and not log(2, x)=0  NaN at 0
    y * ln(x) / ln(x)      y provided not ln(x) = 0 and not x = 0    NaN at 0

Ordinary divisions are untouched, and that is the whole reason this is safe:
a divisor that cannot be undefined has a domain condition of True and it folds
away. `(x^2 - 1)/(x - 1)`, `(x^3 + 1)/(x + 1)`, `(x^2 + 2x + 1)/(x + 1)`,
`x^2 / x` and `x^3 / x^2` all answer exactly what they answered.

One recorded test moves. `x!/x!` now carries the factorial's domain instead of
`not x! = 0`, which is the same change `(x + 1)!/(x + 1)!` took in #1176 --
that one went through a cancellation rule and this one through this rewrite,
which is why they moved a commit apart. The note in SimplifyTest that called
the difference out is updated rather than left describing a state that lasted
one commit. Measured at x = -4, -3, -2, -1, 0, 1, 3, 1/2 and -1/2: the old
condition and the new one agree with the unsimplified quotient at every point,
NaN at the four gamma poles and 1 elsewhere.

Both spellings changed together, MatchedRules and Patterns.cs.

Full suite 9560 passed, 0 failed.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura
@Rafael-SOWNet
Rafael-SOWNet merged commit 5d802ba into master Sep 5, 2026
31 checks passed
@Rafael-SOWNet
Rafael-SOWNet deleted the zero-over-undefined branch September 5, 2026 15:22
Rafael-SOWNet added a commit that referenced this pull request Sep 6, 2026
* The growth census is held by a test, not quoted in a remark

`Saturation.RulesUpTo` argues in prose from the split of rules across
RewriteRuleGrowth, and the figures it quoted were stale by a factor of four:
"26 collect, 17 rearrange, 9 expand and 270 are unjudged", and "84% of the
library", all measured before the growth declarations went in. The unjudged
count went 261 to 152 over that work; the true split is 97 / 45 / 30 / 152.

The argument survives the correction -- a ceiling that refuses Unknown still
refuses 47% of the rules, so the dial is still whether unjudged rules may fire
at all. The arithmetic in it did not, which is the reason to hold a number
somewhere that fails when it moves rather than to reason from it in a comment.

RuleAuthoringGuideTest already pinned the 152. It pins all four now, so the
next time they move this remark fails with them.

Full suite 9564 passed, 0 failed.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura

* The 1915th, and every release beside it on one machine

The performance column the release checklist asks for, and the first one where
all five entries in key-commits.txt were measured -- one benchmark, five
kernels, one machine, one hour. The four release-pair sections below it had to
approximate that by measuring two commits at a time.

v2.1.0 and v2.2.0 appear for the first time. They did not build until #1178.

Since 2.4.0 the Simplify and Solve family is up 0.15% to 0.65% -- SimplifyHard
+0.65%, SolveMediumHard +0.31%, SolveHard +0.23%. Small, consistent in sign,
and above the noise on those rows by three orders of magnitude. Well inside
PerformanceGate's 3%, so not a reason to hold a release; recorded because the
alternative is claiming the period was free. The likeliest cause is the
definedness conditions of #1176 and #1177, which give every cancelled quotient
a larger condition tree. CompileEasy and CompileHard are flat against 2.4.0 and
about half what they were at 2.3.0.

And a rider on this file's own central claim, which the run happened to be able
to test. It says allocation is deterministic -- "the same commit measured twice
gives the same bytes". The five columns were run twice, for an unrelated reason,
and that is true for the large benchmarks and false for the small ones:

    SolveHard    @ v2.1.0   1,356,524,520 -> 1,356,525,608   0.00008%
    SimplifyHard @ v2.1.0   3,733,177,488 -> 3,733,136,616   0.001%
    CompileEasy  @ v2.1.0          16,280 ->        16,519   1.47%
    CompileEasy  @ v2.3.0          16,510 ->        16,206   1.84%

The compile benchmarks have an allocation floor of about 2%. That matters
because PerformanceGate fails at 3%: for CompileEasy that is one and a half
noise-widths of margin rather than the comfortable threshold it reads as. A
CompileEasy allocation move under 2% is not evidence; the same move on SolveHard
is evidence a thousand times over.

The script also gained a warning it needed. A branch name resolves to whatever
this checkout's copy of it points at, and in a worktree the local `master`
belongs to whichever checkout last moved it -- the first run of this table
measured a `master` five days behind its remote and labelled the column
`master`. Only the SHA printed beside the row gave it away. It now says so when
a name resolves behind its remote-tracking counterpart.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura

---------

Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

a / a = 1 excludes the zero of a but not the points where a is undefined

1 participant