Facts about a symbol that rewrite it: abs(z) = 1, a real parameter, a relation such as alpha^7 = 1 #2148

Modenov's method in Chapter III of Problems in Geometry (#2131) rests on facts about a symbol that change how it simplifies:

• a point on the unit circle, abs(a) = 1, so conj(a) = 1/a;
• a real parameter, so conj(λ) = λ;
• a normalisation such as σ₃ = abc = 1, so c = 1/(ab);
• a root of unity, α^7 = 1, so conj(α) = α^6.

Every reader of the book applied these by hand. Without them the conjugate (#2145) leaves conj(a) where the book writes 1/a.

Today a provided clause is carried but not consulted:

• sqrt(c^2) provided c > 0 stays as it is;
• an angle-sum identity under provided A + B + C = pi stays as it is.

There is also no way to say that t is real, so abs(e^(i*t)) stays as it is, as it must.

The domain conditions (#721, DomainConditionIn) say which number set a value lies in. These are relations, and using them means simplifying modulo an equation.

This is #746's "assumptions travelling with nodes" (tier 1), and it shares a design with #1237 (typed variables). That is why it is 3.0.