Table 3: Nelsen 18 is not Schur-ordered in its parameter #
nelsen18_not_schur_antitone (in SchurUnordered.lean) excludes a decreasing order.
Here the convex test z ↦ (z-5/8)₊ at threshold 1/9 shows C₂ ≰_∂S C₄, so the family
is not increasing either. Together with Archimedean symmetry, neither both-direction
monotonicity holds.
theorem
Papers.AnsariRockel2024.nelsen18_not_schur_monotone :
¬∀ (θ η : ℝ) (hθ : 2 ≤ θ) (hθη : θ ≤ η), (Verification.nelsen18 θ hθ).SchurLE (Verification.nelsen18 η ⋯)