[Rafael-SOWNet]

Part of #212: the family of sqrt(y) - x, the first of the items left there.

sqrt(y) = x in x and y was declined. Solved for y, it is x^2 provided x = 0 or -pi/2 < arg(x) <= pi/2, where sqrt takes its values (#2183). The family (t_1, t_1^2 provided …) was then checked as though it claimed every t_1, and sqrt(t_1^2) - t_1 is not zero.

• A family that says where it holds is now checked there. The non-square solver takes the conditions out of the family's own entries and decides forall t_1 in CC : condition implies residual = 0. A condition that Simplify introduces is not the family's, and is checked as before.
• Under that hypothesis, a new reader in QuantifierFacts takes the principal root of a whole power, (t^n)^(1/n) for n >= 2, as t. That holds where the facts put t at 0 or in the sector -pi/n < arg(t) <= pi/n, which is how the inversion writes it, or on t >= 0, as Complex.pow_cpow_nat_inv has it. Outside a quantifier sqrt(t^2) is not t.

	master (d9ff463)	now
sqrt(y) - x in x, y	null	[[t_1, t_1 ^ 2 provided t_1 = 0 or -1/2 * pi < arg(t_1) and arg(t_1) <= 1/2 * pi]]
y^(1/3) - x in x, y	null	the same with 1/3 * pi
forall t in RR : t >= 0 implies sqrt(t^2) = t	as written	True
forall t in CC : (t = 0 or -pi/2 < arg(t) <= pi/2) implies sqrt(t^2) = t	as written	True

The last item on #212 is the parameters' names in the result, an API question for the thread.

Tests: RootByFactsTest (4 decided, 3 not claimed, one of them the square root's sector asked of a cube root, and nothing assumed outside a quantifier) and AFamilyThatSaysWhereItHoldsIsCheckedThere. The latter checks the family at points in the sector, i/2 on its edge among them, and that the condition is false at a negative t_1. Full suite 17868/0, interactive trio, AOT smoke 64/0, all frameworks build.

🤖 Generated with Claude Code

https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura

[codecov]

Codecov Report

❌ Patch coverage is 71.42857% with 12 lines in your changes missing coverage. Please review.
✅ Project coverage is 86.57%. Comparing base (d9ff463) to head (0faa157).

Files with missing lines	Patch %	Lines
...s/AngouriMath/Functions/Boolean/QuantifierFacts.cs	69.69%	4 Missing and 6 partials ⚠️
...us/Solvers/EquationSolver/NonSquareSystemSolver.cs	75.00%	0 Missing and 2 partials ⚠️

Additional details and impacted files

@@            Coverage Diff             @@
##           master    #2206      +/-   ##
==========================================
- Coverage   86.57%   86.57%   -0.01%     
==========================================
  Files         301      301              
  Lines       66838    66878      +40     
  Branches    19410    19428      +18     
==========================================
+ Hits        57864    57897      +33     
  Misses       4879     4879              
- Partials     4095     4102       +7     

Flag	Coverage Δ
cpp	37.77% <ø> (ø)
csharp	87.12% <71.42%> (-0.01%)	⬇️
fsharp	32.97% <ø> (ø)
interactive	40.72% <ø> (ø)

Flags with carried forward coverage won't be shown. Click here to find out more.

Files with missing lines	Coverage Δ
...nuous/Evaluation.Continuous.Arithmetics.Classes.cs	86.72% <100.00%> (+0.01%)	⬆️
...us/Solvers/EquationSolver/NonSquareSystemSolver.cs	88.23% <75.00%> (-0.31%)	⬇️
...s/AngouriMath/Functions/Boolean/QuantifierFacts.cs	86.41% <69.69%> (-1.90%)	⬇️

... and 5 files with indirect coverage changes

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.