Lemma 18 — Multi-Layer Concentric Quartic Annuli Radial Convexity Separation

Proved

multi_annulus_quartic_nesting_v3

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

analysiscombinatoricserdos-problems

For concentric quartic spherical shells with radial gap defect $J \ge 0$ , any cross-shell midpoint equation satisfies $R_m^4 \le \frac{1}{2}R_1^4 + \frac{1}{2}R_2^4$ , forcing radial confinement.

Formal statement

import Mathlib

theorem multi_annulus_quartic_nesting_v3 (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