A listed solution set is filtered by a decided condition - #1443
Merged
Merged
Conversation
"x^2 = 4 and not x = 2".Solve("x") was the conjunction left as written: #1036 taught the
solver not to intersect a listed set with a condition a search had left open, since 1 is a
root of x^6 + x y + 1 = 0 only when y is -2, and the rule stopped at the shape. The two are
told apart now: a member at which the condition is decided is kept where it is True and
dropped where it is False, and the conjunction stays written the moment one member is
undecided, so #1036's case is as it was. Decided by evaluation, and by simplification where
evaluation leaves it open -- the solution of 2 v + 1 = 2 u + 1 arrives as -(1 - 2u - 1)/2,
and `not that = u` is the simplifier's -- so that the injectivity of a linear map,
forall u in RR : forall v in RR : 2 u + 1 = 2 v + 1 implies u = v, is True: the reference's
Def 7.4.6, item 6 of #1409.
#1409
#1036
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
1 participant
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.
Measuring the reference's injectivity rows for item 6 of #1409:
forall u in RR : forall v in RR : 2 u + 1 = 2 v + 1 implies u = vstayed written. The inner statement's negation,2 v + 1 = 2 u + 1 and not v = u, was solved to the conjunction as written — #1036 taught the solver not to intersect a listed set with a condition a search had left open (1 is a root ofx^6 + x y + 1 = 0only whenyis −2), and the rule stopped at the shape (aFiniteSetbeside aConditionalSet) rather than at what it was for.Now the two are told apart: a member of the listed set at which the condition is decided is kept where it is
Trueand dropped whereFalse, and the conjunction stays written the moment one member is undecided — #1036's case is as it was (AnUndecidedConditionLeavesTheConjunctionWritten). Decided by evaluation, and by simplification where evaluation leaves it open, since the solution of2 v + 1 = 2 u + 1arrives as-(1 - 2u - 1)/2andnot that = uis the simplifier's to settle.x^2 = 4 and not x = 2{ x : x^2 = 4 and not x = 2 }{ -2 }(x - 1)(x - 2) = 0 and not x = 1 and not x = 2{}forall u in RR : forall v in RR : 2 u + 1 = 2 v + 1 implies u = vTrueforall u in RR : forall v in RR : u^2 = v^2 implies u = vFalse(a witness)Falsex^6 + x y + 1 = 0 and x - 1 = 0(#1036)The cubic's injectivity stays open: the solutions of
v^3 = u^3come as(u^3)^(1/3)and its two rotations, and(u^3)^(1/3) = uis not an identity on the reals in principal roots, so nothing is claimed.ConjunctionFilterTest, 6 rows. BREAKING-CHANGES.md rows measured on a v2.5.0 build. Full suite 12218 passed, 0 failed; benchmark gate PASSED (the Solve benchmarks within 0.1% of the baseline).Part of #1409.
🤖 Generated with Claude Code
https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura