Know the Pythagorean identity in more than one arrangement (#725)

[Rafael-SOWNet]

Closes #725. Takes the first of the two expressions in #557 from unsimplified to 0; #557 itself stays open for the second, see below.

What was wrong

sin(x)^2 + cos(x)^2 = 1 was one syntactic pattern — an adjacent sum of the two squares, in either order — so the same fact written any other way was not recognised. The library's answer depended on which of several equivalent spellings an expression happened to arrive in:

input	was	is
1 - sin(t)^2	unchanged	cos(t)^2
1 - cos(t)^2	unchanged	sin(t)^2
1 - sin(t)^2 - cos(t)^2	unchanged	0
1 + tan(t)^2	unchanged	sec(t)^2
1 + cotan(t)^2	unchanged	csc(t)^2
sec(t)^2 - tan(t)^2	unchanged	1 provided not cos(t) = 0
csc(t)^2 - cotan(t)^2	unchanged	1 provided not sin(t) = 0
(sin(2t)*csc(t))^2/4 - cos(2t) - sin(t)^2	unchanged	0 provided not sin(t) = 0

Two of those are the identity solved for one square rather than for 1; four are it divided through by sin^2 and by cos^2. Eight rules, no machinery.

The direction is one-way on purpose: 1 - sin(:)^2 becomes cos(:)^2 and not the reverse. The two sides are interchangeable, so stating it both ways would undo each rewrite as fast as it fired.

The conditions on the last three are the functions' own — a tangent and a secant are undefined where the cosine vanishes — and carrying them is right rather than a loss: a bare 1 would claim a value at a point the expression does not reach.

One existing test moved

MultipleAngleTest.PythagoreanPairAcrossASubtractionIsStillMissed pinned this gap from the other side: cos(2x) - (2cos(x)^2 - 1) stopped at 1 - cos(x)^2 - sin(x)^2 because the pair sat either side of a subtraction. It reduces to 0 now, so the case moves into IdentitiesReduceToZero with its note kept. What that note said — that this was not something opening the angle could reach — was right, and nothing about the angle expansion changed.

What this does not reach, recorded rather than claimed

Every rule here matches a pattern, so the two parts of the identity have to be adjacent in the tree. In a sum of three terms the sorting separates the pair before the rules are tried:

1 + cotan(t)^2              =>  csc(t)^2                  (reduces)
csc(t)^2 - 1/sin(t)^2       =>  0                         (reduces)
1 + cotan(t)^2 - 1/sin(t)^2 =>  unchanged                 (does not)

Written in sines and cosines the same statements do reduce (1 + cos(t)^2/sin(t)^2 - 1/sin(t)^2 is 0), so nothing there is a wrong answer — only an unreduced one. Reaching them wants the identity stated over the gathered terms of a sum rather than over an adjacent pair, which is a larger change than this one.

That same gap is the last thing standing between #557's second expression and 0: it reduces as far as 1/sin(t)^2 - (1 + cotan(t)^2), a difference of two equal things left in two notations. Everything else that expression needs is already in the library — the multiple-angle expansion opens sin(2t), and the rational cancellation over sin/cos works.

Both are pinned as a skipped theory with the diagnosis in its summary, next to a passing theory showing the sin/cos spellings that do reduce.

Measured

19 regression cases in a new PythagoreanIdentityTest, one of them the skipped record above. Unit tests 4825 passing with none failing; F# 130 of 130; the 117-problem solver corpus stays at 112 solved with 0 wrong, 0 error and 0 timeout.

🤖 Generated with Claude Code