Repository navigation
An infinity over a vanishing divisor is the infinity of the signs - #2295
Merged
Rafael-SOWNet merged 1 commit intoOct 31, 2026
Conversation
limit(ln(x^2) / (cos(x) - 1), x, 0) was NaN, the claim that there is no limit, where it is +oo from both sides. Each side's descent put the parts' limits in place of the parts and read (-oo) / 0, which says nothing about the side the divisor vanishes from and is NaN, and DivergesAtAVanishingDivisor, which reads that side, asked for a finite dividend. An infinity with a sign over a divisor vanishing from one side is no more indeterminate than a number is: it is the infinity of the two signs' product. The rule now takes one. AnInfinityOverAVanishingDivisorTest takes four two-sided limits that were NaN, four one-sided and two-sided ones that were answered and are unchanged, and three that have no limit and stay NaN, x^x at 0 among them; the four fail on master. The suite, the trio, F#, AOT and the eight harnesses pass. #2275's entry for ln(x^2) / ln(cos(x)) now reads +oo. The issue put the cause at WhereBothSidesAgree's real-codomain gate. Opening the gate changed nothing: each side was still (-oo) / 0. Fixes #2274. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## master #2295 +/- ##
=======================================
Coverage 86.73% 86.73%
=======================================
Files 310 310
Lines 67960 67960
Branches 19740 19740
=======================================
+ Hits 58946 58947 +1
Misses 4881 4881
+ Partials 4133 4132 -1
Flags with carried forward coverage won't be shown. Click here to find out more.
🚀 New features to boost your workflow:
|
Rafael-SOWNet
deleted the
a-two-sided-limit-asks-each-side-where-the-expression-is-real-on-both
branch
October 31, 2026 06:13
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.
limit(ln(x^2) / (cos(x) - 1), x, 0)was NaN, the claim that there is no limit, where it is+oofrom both sides. Each side's descent replaced the parts with their limits and read(-oo) / 0. That says nothing about the side the divisor vanishes from, so it is NaN.DivergesAtAVanishingDivisor, which does read that side, required a finite dividend. An infinity with a sign, over a divisor vanishing from one side, is no more indeterminate than a number is: the result is the infinity whose sign is the product of the two. The rule now takes an infinite dividend too.limit(ln(x^2) / (cos(x) - 1), x, 0)NaNNaN+oolimit(ln(x^2) / ln(1 - x^2/2), x, 0)NaNNaN+oolimit(ln(abs(x)) / ln(cos(x)), x, 0)NaNNaN+oolimit(ln(x^2) / ln(cos(x)), x, 0)-ooNaN(#2275)+ooAnInfinityOverAVanishingDivisorTestcovers three groups. The four limits above fail on master. Four limits that were already answered are unchanged, and three with no limit stay NaN,x^xat 0 (#719) among them. The suite (18,447), the trio, F#, AOT and the eight harnesses pass locally. #2275's BREAKING row forln(x^2) / ln(cos(x))now says+oo.The issue placed the cause in
WhereBothSidesAgree's real-codomain gate, and that was wrong. I opened the gate for expressions that are real on each side, and nothing changed: each side was still(-oo) / 0, which evaluates to NaN. This rule is the cause, and the gate is unchanged.Fixes #2274.
🤖 Generated with Claude Code