Lemma 18 — Multi-Layer Concentric Quartic Annuli Radial Convexity Separation
Provedmulti_annulus_quartic_nesting_v2analysiscombinatoricserdos-problemsnumber-theory
For concentric quartic spherical shells with radial defect J >= 0, any cross-shell midpoint equation satisfies Rm^4 <= 1/2R1^4 + 1/2R2^4.
Formal statement
import Mathlib
theorem multi_annulus_quartic_nesting_v2 (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