An absolute value cannot equal a negative (#812) - #815
Merged
Conversation
"abs(x) = -1".ToEntity().Solve("x")
was { -e ^ (i * r_1) provided r_1 in RR }
is { }
The old answer was wrong rather than merely loose. At r_1 = 0 its member is
-1, and abs(-1) is 1, not -1; every member has modulus 1 and solves nothing.
abs(f(x)) = value is inverted by writing f(x) as value * e ^ (i * r) over
real r, which is the circle of radius |value|. That solves the equation only
where |value| and value agree -- where value is real and not negative -- and
the condition saying so was missing. It is now carried alongside the one on
r, so a decidable negative collapses the set to empty, a decidable
non-negative drops it and leaves the previous answer untouched, and a
symbolic one is kept:
abs(x) = 3 { 3 * e ^ (i * r_1) provided r_1 in RR } unchanged
abs(x) = 0 { 0 provided r_1 in RR } unchanged
abs(x) = a { a * e ^ (i * r_1) provided r_1 in RR and a >= 0 } new condition
The last of those is what #318 asked this inversion to return, in the
sentence that named both halves of it; the r in RR half was already
implemented and the a >= 0 half is this.
The tests check solutions by substituting them back with the circle's
parameter given a value, not by comparing printed form. Checked for teeth
against origin/master: four of the seven fail without the fix, and the three
that do not are the ones asserting the previously-correct answers are
unchanged.
5558 unit tests and 130 F# tests pass; casbench 113/117 with 0 wrong,
propcheck 0 failures, rootcheck 596/596, simpsweep 10463/10463.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Rafael-SOWNet
force-pushed
the
fix/812-abs-inversion-guard
branch
from
August 8, 2026 12:35
cbfca0a to
c86c0bf
Compare
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.
Closes #812. Partly closes #318 — see below.
The old answer was wrong, not merely loose
At
r_1 = 0its member is-1, andabs(-1)is1, not-1. Every member has modulus 1 and solves nothing.Cause
abs(f(x)) = valueis inverted by writingf(x)asvalue * e ^ (i * r)over realr— the circle of radius|value|. That solves the equation only where|value|andvalueagree, which is wherevalueis real and not negative. The condition saying so was missing.It is now carried alongside the one on
r:abs(x) = -1{ }← fixedabs(x) = 3{ 3 * e ^ (i * r_1) provided r_1 in RR }← unchangedabs(x) = 0{ 0 provided r_1 in RR }← unchangedabs(x) = a{ a * e ^ (i * r_1) provided r_1 in RR and a >= 0 }← new conditionA decidable negative collapses the set to empty; a decidable non-negative drops the condition and leaves the previous answer untouched; a symbolic one is kept rather than guessed at.
This is the missing half of #318
#318 asks for exactly this inversion and names both halves in one sentence:
The
r in RRhalf was already implemented. This is thea >= 0half. What remains of #318 after this is only the internal return type —InvertisinternalandInvertNodeisprivate protected, so that part breaks nobody and is not urgent. Detail in this comment.Tests
Solutions are checked by substituting them back with the circle's parameter given a value, not by comparing printed form.
Checked for teeth against
origin/master: four of the seven fail without the fix. The three that pass on both sides are the ones asserting the previously-correct answers are unchanged, which is what they are for.Verification
5558 unit tests, 130 F# tests. casbench 113/117 with 0 wrong, propcheck 0 failures, rootcheck 596/596, simpsweep 10463/10463.
🤖 Generated with Claude Code