Skip to content

Simplify drops a condition the answer's own domain condition states, read in the codomain - #1402

Merged
Rafael-SOWNet merged 2 commits into
masterfrom
provided-has-a-value
Sep 17, 2026
Merged

Rafael-SOWNet merged 2 commits into
masterfrom
provided-has-a-value

Conversation

@Rafael-SOWNet

@Rafael-SOWNet Rafael-SOWNet commented Sep 17, 2026 •

Copy link
Copy Markdown
Member

#1394, second half, on the maintainer's reading: a provided is validated against what the expression accepts under the codomain, and the library already says that per node — DomainConditionIn(codomain). #1396 had hard-coded the shapes (a quotient by d, a negative power of d, a logarithm of d, d^f with f vanishing); this replaces the list with the answer's own domain condition.

Change. IsUndefinedAtTheZerosOf(answer, e) is now: does answer.DomainConditionIn(MathS.Settings.Codomain) already exclude the zeros of e — a conjunct not d = 0 or d > 0 with d vanishing at them (e itself, a positive power of it, a product holding it, a sine, tangent, arcsine or arctangent of such a thing, or a polynomial in the variable e is with no constant term), or a disjunction every side of which does (x^x's not x = 0 or x > 0). Nothing in the rule decides what a node accepts; that stays with the node, so the rule follows the codomain: when #217 gives 1/0 a value under the codomains that admit a complex infinity, a quotient's domain condition changes there and 1/x provided not x = 0 stops being redundant by itself. (Two earlier versions of this branch hard-coded "a pole is a value" and then evaluated 1/0, ln 0 against the codomain; both were rebuilding this mechanism, and the thread on #1394 has the trail.)

#1396 Is
"x^x".Differentiate("x").Simplify(), "ln(x)/x"…, "x^n"… bare the same
"ln(x) provided not x = 0".Simplify() ln(x) the same — ln's domain condition over CC excludes zero, the library's own statement that ln 0 is a limit and not a value
"tan(x) provided not cos(x) = 0".Simplify() unchanged tan(x)
"sin(x)/x provided not x = 0".Simplify() unchanged sin(x)/x
"1/(1 + x^2) provided not x = 0".Simplify(), "x/x provided not x = 0" unchanged unchanged
"(x + sin(x))/x".Limit("x", "+oo") 1 1

Recorded in the Providedf section of SimplificationContract.md, the comparison page's provided paragraph, and the #1396 entry of BREAKING-CHANGES (which now describes the mechanism rather than the list, with the two new rows). The wiki's Simplification page gains a section on provided with four examples run on this build — committed on a local clone, pushed once this merges, since the wiki has no branches.

Measured. All four test suites green (11,484). Performance gate PASSED: SimplifyEasy +0.9%, SimplifyHard +0.7%, allocation as the baseline says on all 19 gated rows — the domain condition is asked once per provided answer at the Simplify boundary.

Part of #1394.

🤖 Generated with Claude Code

https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura

…he condition beside it

#1394's reading: a provided says where the expression has a value, and 1/x at zero has one,
the point at infinity, so 1/x provided not x = 0 is a different expression from 1/x and keeps
its condition. #1396 dropped it, reading a quotient by d, a negative power of d and a logarithm
of d as undefined at the zeros of d; those arms go, and only 0^0 and 0/0 -- d^f or n/d with
both vanishing at the zeros of the condition's expression -- are read, a sine, tangent,
arcsine or arctangent of something vanishing counting as vanishing. x^x's derivative stays
bare, ln(x)/x's derivative keeps its condition as before #1396, and (x + sin(x))/x still has
limit 1 at infinity since sin(x)/x is 0/0 at zero.

The reading is recorded in the Providedf section of SimplificationContract.md, with the
codomain caveat, in the comparison page's provided paragraph, and in the #1396 entry of
BREAKING-CHANGES, rewritten to the net behaviour with the day the wider rule stood on master
noted. Four suites green; the performance gate passed.

Part of #1394.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura
…read in the codomain

#1396 decided by the shape of the node -- a quotient by d, a negative power of d, a logarithm
of d, d^f with f vanishing -- what the library already says per node: DomainConditionIn(codomain)
is what an expression accepts under the reading it is asked in, a nonzero divisor, a nonzero
base or a positive exponent, a nonzero antilogarithm over the complex plane and a positive one
over the reals, a cosine that is not zero for a tangent. A provided not e = 0 is redundant
where that domain condition already excludes the zeros of e: a conjunct not d = 0 or d > 0
with d vanishing there -- e itself, a positive power of it, a product holding it, a sine,
tangent, arcsine or arctangent of such a thing, or a polynomial in the variable e is with no
constant term -- or a disjunction every side of which does, as x^x's not x = 0 or x > 0.
Nothing in the rule decides what a node accepts, so it follows the codomain: when #217 gives
1/0 a value under the codomains that admit a complex infinity, the quotient's domain condition
changes there and the condition beside 1/x stops being redundant by itself.

The answers are #1396's, and the shapes the list missed: tan(x) provided not cos(x) = 0 and
sin(x)/x provided not x = 0 drop their conditions too. Recorded in the Providedf section of
SimplificationContract.md, in the comparison page's provided paragraph and in the #1396 entry
of BREAKING-CHANGES. Four suites green; the performance gate passed.

Part of #1394.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura
@Rafael-SOWNet Rafael-SOWNet changed the title A pole is a value, so only an indeterminate form lets Simplify drop the condition beside it Simplify drops a condition the answer's own domain condition states, read in the codomain Sep 17, 2026
@Rafael-SOWNet

Copy link
Copy Markdown
Member Author

Reworked (second commit, 56df0be → this) on the thread's conclusion: the rule now asks the answer's own DomainConditionIn(MathS.Settings.Codomain) instead of hard-coding shapes — #1396's answers, plus tan(x) provided not cos(x) = 0 and sin(x)/x provided not x = 0 dropping theirs; description and title rewritten to match. Four suites green, gate PASSED (SimplifyEasy +0.9%).

@Rafael-SOWNet
Rafael-SOWNet merged commit 3226805 into master Sep 17, 2026
31 checks passed
@Rafael-SOWNet
Rafael-SOWNet deleted the provided-has-a-value branch September 17, 2026 18:47
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.

1 participant