Solution set to non-linear equation of $3$ variables I have the following trigonometric equation of $3$ variables:
$$f(\theta,\lambda,\phi)=3 \cos (\theta ) \cos (\lambda ) \cos (\phi
   )-(\cos (\theta )+3) \sin (\lambda ) \sin
   (\phi )$$
$$-\sin (\theta ) \cos (\lambda )+\sin
   (\theta ) \cos (\phi )+3 \cos (\theta )+\cos
   (\lambda ) \cos (\phi )-7$$
I want to prove that the solution set to the equation $f(\theta,\lambda,\phi)=0$ is
$$S_f=\{(2\pi k,\lambda+2\pi m,-\lambda+2\pi n):k,m,n\in\mathbb{Z},\lambda\in\mathbb{R}\}$$
Graphically, it is easy to see that this is the case but everything I have tried so far has failed to prove the conjecture. Perhaps my best attempt was extrapolating this equation into an unwieldy polynomial of $3$ variables
$$P(x,y,z)=9 x^4 y^2+16 x^4-18 x^3 y^2-192 x^3+9 x^2
   y^4+z^4 \left(\left(x^2-1\right)
   y^2+1\right) \left(16 \left(x^2-1\right)
   y^2+(3 x+5)^2\right)-64 x^2 y^2+z^2
   \left((x-1) (x+1) \left(9 x^2+30 x+41\right)
   y^4+2 x (x (48 (x-5) x+187)+234) y^2+x (x (9
   (x-2) x-64)-78)-74 y^2+151\right)+736 x^2+2
   y z^3 \left(9 x^4+12 x^3-20 x^2+(x-1) (x+1)
   (x (31 x-78)-33) y^2-96 x-33\right)+2 y z
   \left(31 x^4-270 x^3+560 x^2+(x (x (3 x (3
   x+4)-20)-96)-33) y^2-210 x-111\right)+30 x
   y^4-78 x y^2-960 x+25 y^4+151 y^2+400$$
over the domain $(x,y,z)\in [-1,1]^3$. If I can prove that the solution set to $P(x,y,z)=0$ over this domain is
$$S_P=\{(1,y,y):y\in[-1,1]\}$$
then the original conjecture would be solved. The motivation behind this is actually proving a certain type of quantum error detection encoding exists. It's a little difficult to explain (although if anyone wants details I am more than happy to provide them) but suffice to say that after a lot of work I managed to whittle my existence proof down to the conjecture above.
 A: You can get a more tractable, hand-bashable quadratic equation if you do the famous half tangent substitution:
$$\tan\frac\theta 2 = x,\,\, \tan\frac\phi 2 = y,\,\,\tan\frac\lambda 2 = z.$$
Then for example, one has:
$$\cos\theta = \dfrac{1-x^2}{1+x^2}\text{  and  } \sin\theta = \dfrac{2x}{1+x^2}.$$
This saves us the trouble of repeated squaring and once you multiply everything out, you will get a quadratic in $x$ whose discriminant is:
$$\Delta  = -16(y+z)^2(21y^2z^2+13y^2+13z^2+16yz+21)<0$$
unless $y+z = 0.$
The whole thing took me about 20 mins of hand checking, but once you know the plan of attack with the right substitution, it's nothing but guaranteed to be completed.
A: We prove $f(\theta,\lambda,\phi) \le 0$ for each $\theta,\lambda,\phi$ and that equality holds exactly when you conjecture it does.
Write $$f(\theta,\lambda,\phi) = \cos(\theta)a+\sin(\theta)b+\cos(\lambda)\cos(\phi)-3\sin(\lambda)\sin(\phi)-7$$ for $a = 3\cos(\lambda)\cos(\phi)-\sin(\lambda)\sin(\phi)+3$ and $b = \cos(\phi)-\cos(\lambda)$. To maximize $f$, we of course to choose $\theta$ so that $\cos(\theta)a \ge 0$ and $\sin(\theta)b \ge 0$. So, for ease, let's just pretend $a,b \ge 0$ so that $\cos(\theta),\sin(\theta) \ge 0$. To maximize $xa+\sqrt{1-x^2}b$ for $x \in [0,1]$, one takes $x = \frac{a}{\sqrt{a^2+b^2}}$ (easy to prove by basic calculus), yielding a maximum of $\sqrt{a^2+b^2}$; and note that any other $x$ yields a strictly smaller value. Therefore, we wish to show $$\sqrt{(3\cos(\lambda)\cos(\phi)-\sin(\lambda)\sin(\phi)+3)^2+(\cos(\phi)-\cos(\lambda))^2}+\cos(\lambda)\cos(\phi)-3\sin(\lambda)\sin(\phi)-7 \le 0$$ with equality if and only if $\lambda = -\phi+2\pi m$ for some $m \in \mathbb{Z}$ (since then $\cos(\theta)$ will be $1$). For ease, let $x = \cos(\lambda)\cos(\phi)$ and $y = \sin(\lambda)\sin(\phi)$. We can rewrite the above as $$\sqrt{(3x-y+3)^2+(\cos(\phi)-\cos(\lambda))^2}+x-3y-7 \le 0.$$ We will show $$\sqrt{(3x-y+3)^2+(\cos(\phi)-\cos(\lambda))^2+(\sin(\phi)+\sin(\lambda))^2}+x-3y-7 \le 0$$ with equality if and only if $\lambda = -\phi+2\pi m$, which clearly suffices. The point of introducing the $(\sin(\phi)+\sin(\lambda))^2$ is that $$(\cos(\phi)-\cos(\lambda))^2+(\sin(\phi)+\sin(\lambda))^2 = 2-2x+2y.$$ So, we just wish to show that $$\sqrt{(3x-y+3)^2+2-2x+2y}+x-3y-7 \le 0$$ for $\{(x,y) \in [-1,1]^2 : |x-y| \le 1\}$ with equality if and only if $x-y = 1$. Note that $|3x-y+3| = |2x+(x-y)+3| \le 6$ and $|2-2x+2y| = 2|1-(x-y)| \le 4$, so $\sqrt{(3x-y+3)^2+2-2x+2y} \le \sqrt{40}$. Therefore, we cannot have $y \ge 0$ and $x \le 0$.
Let's first start with $y \ge 0$. Then, as just explained, $x \ge 0$. We will show that $$\sqrt{(3x-y+3)^2+2-2x+2y}+x-7 \le 0$$ with equality if and only if $x=1,y=0$. Note the derivative of the term inside the square root with respect to $y$ is $2y+2-6(x+1)$, which is negative, so we choose $y=0$ to maximize. We then wish to show $$\sqrt{(3x+3)^2+2-2x} -7 \le 0$$ with equality if and only if $x = 1$. But this is equivalent to $(3x+3)^2+2-2x \le 49$, which is true for $x \le 1$ with equality at and only at $x=1$.
Now let's deal with the case $x \le 0$. As explained before, this means $y \le 0$. We show $$\sqrt{(3x-y+3)^2+2-2x+2y}+x-3y-7 \le 0$$ for any $x,y \in [-1,0]^2$ with equality if and only if $y=-1,x=0$. The derivative of the term inside the square root with respect to $y$ is, as before, $2y+2-6(x+1)$, which is negative, so we take $y=-1$ to maximize. We then obtain $$\sqrt{9x^2+22x+16}+x-4,$$ which is maximized at $x=0$, yielding the value $0$. We're done.
A: Let $\;x=\tan\dfrac\theta2,\;y=\dfrac{\lambda+\varphi}2,\;z=\dfrac{\lambda-\varphi}2,\;$ then
$$g(x,y,z) = (1-x^2)(2\cos2y+\cos 2z+3)+4x\sin y\sin z\\
+(1+x^2)(-\cos2y+2\cos2z-7)\\
= (-3\cos2y+\cos2z-10)x^2+4x\sin y\sin z+\cos2y+3\cos2z-4\\
= (-6\cos^2y-2\sin^2z-6)x^2+4x\sin y\sin z - 2\sin^2y-6\sin^2z=0,$$
$$-6(1+\cos^2y)x^2-2(x\sin z-\sin y)^2-6\sin^2z=0.\tag1$$
From $(1)$ should
$$x=0,\quad y=\pi j,\quad z=\pi l,\tag2$$
and finally
$$\color{green}{\mathbf{\theta=2\pi k,\quad \lambda=\pi m,\quad \varphi=2\pi n-\lambda,\quad k,m,n\in\mathbb Z.}}$$
