Sharpness of the archimedean degree bound: solvable $\iff \pi/\psi \le n$

The archimedean threshold for one-step collapsibility, as a sharp equivalence.

Fix $\psi \in (0, \tfrac{\pi}{2})$ and an integer $n \ge 1$. Consider the system

$$\prod_{i=1}^{n} \cos\theta_i = \cos^{n}\psi, \qquad \sum_{i=1}^{n} \theta_i = 2\pi k - n\psi \quad (k \in \mathbb{Z}),$$

in unknowns $\theta_1,\dots,\theta_n$ and $k$, subject to $\theta_i \in (-\tfrac{\pi}{2}, \tfrac{\pi}{2})$ for all $i$ and $\theta_i \neq -\psi$ for all $i$. The assertion is that this system is solvable if and only if $\pi/\psi \le n$.

The statement is pure real analysis and needs no definition beyond $\cos$. The background below explains where the system comes from and why the equivalence is the natural thing to want.

Background: where the system comes from

Call $f \in \mathbb{Q}[x]$ split if $\deg f \ge 1$, its leading coefficient is a nonzero rational, and all of its roots are rational — equivalently $f = c\prod_{i=1}^{n}(x-r_i)$ with $c \in \mathbb{Q}^{\times}$ and every $r_i \in \mathbb{Q}$. An algebraic number $\alpha$ is collapsible if $f(\alpha) \in \mathbb{Q}$ for some split $f$. These are the notions in this mission's definition bundle CollapsibleCubics_basic, and the mission's headline conjecture CollapsibleCubics.cubic_collapsible asserts that every algebraic number of degree $3$ is collapsible.

Let $m = x^3 + dx + e$ be irreducible with negative discriminant, so $m$ has one real root and a pair of complex conjugate roots. Write

$$m = (x + 2u)\big((x-u)^2 + v^2\big), \qquad u, v \in \mathbb{R},\ v \neq 0,$$

so the real root is $\alpha_1 = -2u$ and the complex roots are $u \pm iv$; put $\alpha_2 = u + iv$ and, in the normalisation $uv > 0$,

$$\psi = \arctan(3u/v) \in (0, \tfrac{\pi}{2}).$$

Suppose $f = c\prod_{i=1}^{n}(x - r_i)$ is split with $f(\alpha) \in \mathbb{Q}$ for $\alpha$ a root of $m$. Since $f$ has rational coefficients and $f(\alpha)$ is rational, $f$ takes the same value at every conjugate of $\alpha$; comparing $\alpha_1$ and $\alpha_2$ gives

$$\prod_{i=1}^{n} z_i = 1, \qquad z_i = \frac{\alpha_1 - r_i}{\alpha_2 - r_i}.$$

As $r$ ranges over $\mathbb{R} \cup \{\infty\}$, the point $z = (\alpha_1 - r)/(\alpha_2 - r)$ traces a fixed circle through $0$ and $1$, with polar equation $|z| = \sec\psi \, \cos(\arg z - \psi)$. Substituting $\theta_i = \arg z_i - \psi$, the modulus of $\prod_i z_i = 1$ becomes the product equation and its argument becomes the sum equation, the integer $k$ being the winding count that the argument is only defined up to. Here $n = \deg f$, the constraint $\theta_i \in (-\tfrac{\pi}{2}, \tfrac{\pi}{2})$ is automatic, and $\theta_i = -\psi$ corresponds to $z_i = 1$, that is to $r_i = \infty$, which is not an admissible root.

So the system is exactly the archimedean shadow of one-step collapsibility, with every arithmetic condition on the $r_i$ discarded. The integer $k$ is quantified existentially and is not fixed in advance: that is what makes the forward direction a statement about every split $f$, not merely those of one winding number.

What is known and what is open

The forward direction $(\Rightarrow)$ is the archimedean lower bound on the degree, and it is known. It is the analytic core of this mission's proved milestone CollapsibleCubics.pi_div_psi_le_natDegree, which concludes $\pi/\arctan(3u/v) \le \deg f$ for every split $f$ collapsing a root of $x^3+dx+e$. That milestone is already proved on this platform, but the analytic statement here is not itself a published node, so this direction must be proved again as part of the equivalence. It is the shorter half.

The converse $(\Leftarrow)$ is the open content. It asserts that the bound is sharp: at every $n \ge \pi/\psi$ the system really is solvable, so no further archimedean obstruction exists at any degree. This direction does not appear in the source literature and is not known to be machine-checked anywhere.

Two things to be aware of

The hypothesis $\theta_i \neq -\psi$ is essential, not decoration. As noted above, $\theta_i = -\psi$ means $z_i = 1$, that is a root at infinity, which is not a root at all. Dropping it makes the forward direction false — the degenerate configuration with every $\theta_i = -\psi$ and $k = 0$ satisfies both equations for every $n$ — and on the converse side it would allow a construction that yields fewer than $n$ genuine roots, which does not establish sharpness.

This does not settle collapsibility. The $\theta_i$ supplied by the converse correspond to real $r_i$, not rational ones. The equivalence closes the archimedean side of the one-step problem completely, and thereby isolates the whole remaining difficulty as arithmetic; it does not bear on CollapsibleCubics.cubic_collapsible in either direction.

import Mathlib

namespace CollapsibleCubics
theorem exists_angles_iff_pi_div_psi_le {n : ℕ} (hn : 0 < n) (ψ : ℝ)
    (hψ : ψ ∈ Set.Ioo 0 (Real.pi / 2)) :
    (∃ (θ : Fin n → ℝ) (k : ℤ),
        (∀ i, θ i ∈ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)) ∧
        (∀ i, θ i ≠ -ψ) ∧
        (∏ i, Real.cos (θ i)) = (Real.cos ψ) ^ n ∧
        (∑ i, θ i) = 2 * Real.pi * k - n * ψ) ↔
      Real.pi / ψ ≤ n := by sorry
end CollapsibleCubics