Repository navigation
The other two Pythagorean identities are not known #725
Description
Activity
#726 fixes the arrangements that are adjacent in the tree, which is all six listed above plus the two solved-for-one-square forms found while doing it:
1 - sin(t)^2 => cos(t)^2 1 - cos(t)^2 => sin(t)^2 1 - sin(t)^2 - cos(t)^2 => 0 1 + tan(t)^2 => sec(t)^2 1 + cotan(t)^2 => csc(t)^2 sec(t)^2 - tan(t)^2 => 1 provided not cos(t) = 0 csc(t)^2 - cotan(t)^2 => 1 provided not sin(t) = 0Correcting the diagnosis above
The report guessed that
1/sin(x)^2andcsc(x)^2fail to reach a common form. That was wrong — they do:csc(t)^2 - 1/sin(t)^2 => 0 provided not sin(t) = 0The actual cause is adjacency. Every rule here matches a pattern, so the two parts of the identity have to be neighbours in the tree, and in a sum of three terms the sorting separates them 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 notThe same three terms written in sines and cosines do reduce (
1 + cos(t)^2/sin(t)^2 - 1/sin(t)^2is 0), so this is not the mathematics being out of reach — it is that the rule fires before the terms are gathered, and by the time they are gathered there is no rule.There is an asymmetry inside that too, worth recording:
1 + sin(t)^2/cos(t)^2 - 1/cos(t)^2stops at1 - 1/cos(t)^2 + tan(t)^2, collapsing its quotient back to a tangent, where the sine half of the same pair reduces.What is left
Stating the identity over the gathered terms of a sum rather than over an adjacent pair. That is a larger change than the eight rules in #726 and is left for its own piece of work; it is also the last thing between #557's second expression and 0. Pinned in
PythagoreanIdentityTest.TheThirdTermOfTheIdentityHasToBeAdjacentas a skipped theory carrying the diagnosis, beside a passing one showing the sin/cos spellings that do reduce.Leaving this open until that lands.
- added a commit that references this issue
on Aug 5, 2026 - added a commit that references this issue
on Sep 17, 2026
sin(x)^2 + cos(x)^2simplifies to1. Neither of the other two forms of the same identity does, in either direction:Patterns.TrigonometricRulescarriessin^2 + cos^2in both orders and nothing for the other two. They are the same identity divided through bysin^2and bycos^2, so a library that knows one and not the others is inconsistent about which way an expression happens to have been written.Where it bites
This is the last thing standing between
Simplifyand 0 on the second expression in #557. That one reduces as far asand stops — a difference of two equal things, left in two different notations. Everything else the reporter's expression needs is already there: the multiple-angle expansion opens
sin(2t), and the rational cancellation oversin/cosworks ((2*cos(t)^2*sin(t)^6 - cos(t)^2*sin(t)^6 - sin(t)^6*(cos(t)^2 - sin(t)^2))/sin(t)^8gives1).So #557's first expression is already answered on
master---- and the second is not, and this is the whole of the difference.
What it needs
Two rules, and a normal form to compare against. The identities themselves are one line each; what they also need is for
1/sin(x)^2andcsc(x)^2to reach a common form, since it is the mismatch between those two spellings that leaves the difference standing.CollapseTrigonometricFunctionsalready rewritesa / sin(x)toa * csc(x)but does not see through a power.Measured against
masterat 7a38a8a.