Write down what a simplification rule may assume

[Rafael-SOWNet]

Adds Docs/Contributing/SimplificationContract.md, linked from the contributing index and from
AGENTS.md. Documentation only — no code changes.

Why

#885 fixed four rewrites that had been wrong since 2020 and shipped in every release. While they
were wrong, every harness was green:

casbench	117/119, 0 wrong
propcheck	1340 checks, 0 failures
rootcheck	596/596 clean
simpsweep	10463 comparisons, 0 disagreements

And Simplify was answering 3 for arcsin(sin(3)), whose value is pi - 3.

Sampling structurally cannot find this class: a rule wrong only at a branch cut, or only off the
real line, is wrong exactly where a sweep does not look — and simpsweep additionally builds its
expressions from a grammar that never nests an inverse function around its own forward function,
so the shape was outside its space. The check has to be a reading, and a reading needs
something to read against. That is what this file is.

Its acceptance is the one stated when the work was scoped: a new rule can be judged sound or
unsound by reading the contract.

What is in it

Transformations.md already asks a rewrite what relation it claims and how well justified the
claim is. Every rule set answers SoundUnderAssumptions and names no assumptions — honest, and
says nothing. This is the missing third of that vocabulary.

• What the library already knows, so a rule stops reinventing it: DomainCondition (each
  node's IntrinsicCondition conjoined with its children's — the whole "undefined here" story in
  one property), Codomain (Domain.Any for a bare symbol), MathS.Settings.Codomain (complex
  unless asked), and Providedf, with the two costs of using it — a condition competes on
  complexity, and it travels.
• Four things that are not the same: the reading, a fact about a point, a fact about a
  neighbourhood, and the domain of definition. Conflating any two is how rules go wrong; the first
  two being distinct is Unify Codomain with a "provided ... in RR" condition #721, and lim x->0- (x^x) is the case that separates them.
• A condition is not an assumption — the trap that looks most like a fix. Attaching
  provided x >= -pi/2 and x <= pi/2 to arcsin(sin(x)) claims the expression is undefined
  outside the interval when it merely has another value there. A Providedf narrows the domain; an
  assumption narrows when the rule may fire. Opposite moves.
• Ten numbered obligations, so a review can cite them. Including O7, which is the standing
  guard against over-guarding: if the assumption is checkable somewhere else, the rule is in the
  wrong place and moving it is the fix — a^n / b^n is gathered into (a/b)^n unconditionally, which is wrong for bases of opposite sign #802 being the worked case where nothing was sacrificed.
  And O9: Simplify selects by node count, so an unsound rewrite only has to be short to win,
  and a rule that appears not to fire has not been shown to be safe.
• Judged rules, worked and measured: sound with no assumption (sin(arcsin(z)), |-x| = |x|),
  unsound and fixable by deciding the assumption (Simplify returns wrong answers: arcsin(sin(x)) -> x and three siblings are applied off the principal branch #884), unsound with the assumption belonging
  elsewhere (log_b(a^c), a^n/b^n), sound with a condition (x/x), and correctly declining
  (sqrt(x^2)).
• The branch-cut conventions, measured on a 2.0.0 build rather than asserted.

The convention worth publishing on its own

	value
(-8)^(1/3)	-2 — the real root
(-8)^(2/3)	4 — the real root
(-8)^(1/4)	1.1892 + 1.1892i — principal, there being no real fourth root
(-8)^0.3333333333	1.0 + 1.7320i — principal

For a negative base, an exact Rational exponent with an odd denominator takes the real root;
write the same exponent as a decimal and it takes the principal value, and the two differ by far
more than rounding. So a rewrite that moves between an exact rational and a decimal exponent, or
that reduces 2/6 to 1/3, changes which convention applies. Whether the convention itself is
right is #204 and deliberately a major-version question; that a rule may not silently cross it is
not.

Two inconsistencies it exposes, recorded not fixed

• ln and sqrt disagree about which reading their domain describes. Under the default
  Domain.Complex, DomainCondition of ln(x) is x > 0 — the real reading, since a complex
  logarithm is defined for every x != 0 — while sqrt(x) reports True, the complex one.
  arcsin(x) also reports True, though over the reals it needs |x| <= 1.
• DomainCondition never reads MathS.Settings.Codomain. It is fixed at construction, so it
  cannot say "defined here, given that we are doing real analysis". Unify Codomain with a "provided ... in RR" condition #721 in a second place.

I have not filed these as issues yet — they may be one issue or two depending on whether the
intended reading is per-node or per-setting, and that is a maintainer's call.

Also in this branch's workspace, not in this PR

work/probe gains domain:: and codomain:: operations, which is how the tables above were
measured, and the harness notes lose a limitation that is now closed: with 2.0.0 on nuget.org I
checked the quickstart against the published package rather than a project reference — a fresh
dotnet new console, dotnet add package AngouriMath --version 2.0.0, and its own program printed
x + sin(y * x) and 1 + cos(y * x) * y; the same for F# with AngouriMath.FSharp.

What it does not settle

Per-symbol assumptions (SymPy's Symbol('x', positive=True) with refine/ask, which most of the
assumption sets here would be dischargeable by), whether Providedf should express a
neighbourhood (#721), the fractional-power convention (#204), and the Soundness tiers, which
remain declared rather than checked — nothing here promotes a rule set to Sound.

The harness that would check this class is specified in §8 and does not exist. It has to be
built from the rules rather than from a grammar: for each rewrite, construct the set where its
assumption fails — poles named by DomainCondition, either side of each cut, one period outside a
principal interval, purely imaginary arguments, negative bases at odd and even denominators — and
compare the two sides there, counting both undefined as agreement. That would have found all four
rules of #884 immediately.