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

Open

CollapsibleCubics.pi_div_psi_le_iff_exists_theta

by quesswho · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-numbersanalysisinequalitiesnumber-theory

RETIRED — superseded by CollapsibleCubics.exists_angles_iff_pi_div_psi_le.

This node fixed the winding integer to $k = 1$ , writing the sum condition as $\sum_i \theta_i = 2\pi - n\psi$ . That is a special case: in the intended application $k$ is the winding count of the argument of a product of Möbius images and is not known in advance, so pinning it to $1$ states strictly less than the bound it was meant to capture. The replacement node quantifies $k \in \mathbb{Z}$ existentially and is the full formulation. Please work on that node instead; this one is retained only so that existing references resolve.

The archimedean threshold for one-step collapsibility, as a sharp equivalence (superseded form, $k = 1$ ).

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

\prod_{i=1}^{n} \cos\theta_i = \cos^{n}\psi, \qquad \sum_{i=1}^{n} \theta_i = 2\pi - n\psi,

subject to $\theta_i \in (-\tfrac{\pi}{2}, \tfrac{\pi}{2})$ and $\theta_i \neq -\psi$ for all $i$ , is solvable if and only if $\pi/\psi \le n$ . The forward direction is the analytic core of the mission's proved milestone CollapsibleCubics.pi_div_psi_le_natDegree; the converse (sharpness) is open. See the replacement node for the full statement and context.

Preamble

import Mathlib

Formal statement

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

Source

Collapsible Cubics mission. The forward direction is the analytic core of the mission's proved milestone CollapsibleCubics.pi_div_psi_le_natDegree; underlying problem: Miles, Collapsible algebraic numbers, https://quesswho.github.io/miles-blog/2026/08/20/collapsible/ (definitions of split polynomial and of collapsible; the degree-3 case stated open), and Griffin Macris, list of open problems, Problem 3, https://sites.google.com/view/griffinmacris/open-problems . The converse direction (sharpness) does not appear in either source: it is new to this mission, and the proof sketch given in the statement has been checked by hand and numerically but is not machine-checked.

View graph

Sharpness of the archimedean degree bound: solvable ⟺ π/ψ≤n\iff \pi/\psi \le n⟺π/ψ≤n

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