Multi-Layer Concentric Quartic Annuli Radial Convexity Separation

Proved

multi_annulus_quartic_layer_nesting

by Xinyu Xu · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysiscombinatoricserdos-problemsnumber-theory

For concentric quartic spherical shells $S(R_k) = \{x \in \mathbb{R}^d : \sum x_i^4 = R_k^4\}$ with radial gaps $\Delta R > 0$ , any cross-shell 3-AP with $x \in S(R_1), z \in S(R_2)$ and midpoint $y \in S(R_m)$ requires $R_m^4 + J_4 = \frac{1}{2}R_1^4 + \frac{1}{2}R_2^4$ , forcing radial consistency.

Formal statement

import Mathlib

theorem multi_annulus_quartic_layer_nesting (R1 R2 Rm J : ℝ) (hJ_nonneg : 0 ≤ J)
    (h_layer : Rm ^ 4 + J = (1 / 2 : ℝ) * R1 ^ 4 + (1 / 2 : ℝ) * R2 ^ 4) :
    Rm ^ 4 ≤ (1 / 2 : ℝ) * R1 ^ 4 + (1 / 2 : ℝ) * R2 ^ 4 := by sorry

View graph