MATLAB Code for the Computer‐Assisted Proof

This repository contains MATLAB code supporting the computer‐assisted proof presented in

Ryoki Endo and Xuefeng Liu,
The second Dirichlet eigenvalue over any non‐equilateral triangle is simple.

The code implements a verified numerical method based on interval arithmetic (using the INTLAB toolbox) to obtain rigorous upper and lower bounds for the Laplacian eigenvalues on triangular domains. These bounds are crucial for proving that the second eigenvalue, $\lambda_2$, is strictly separated from the third eigenvalue, $\lambda_3$, which in turn establishes the simplicity of $\lambda_2$ for nearly degenerate triangles (i.e., triangles with a minimum angle less than $\pi/36$).

Theoretical Background

The MATLAB routines in this repository serve to: - Estimate eigenvalue bounds: Compute certified upper and lower bounds for $\lambda_2$ and $\lambda_3$ by comparing the Laplacian eigenvalue problem on triangular domains with auxiliary eigenvalue problems derived from the asymptotic expansion in the collapsing limit. - Validate eigenvalue separation: Employ the Rayleigh–Ritz method combined with verified error estimates and rigorous zero-finding (via INTLAB functions) to confirm that $\lambda_2 < \lambda_3$ rigorously. - Control numerical errors: Use interval arithmetic to guarantee that rounding errors are properly controlled and that the computed bounds are mathematically rigorous.

For a detailed exposition of the underlying theory, please refer to the main paper.

Running Environment

• The code is developed for MATLAB (R2020a or later) and requires the INTLAB toolbox for interval arithmetic.
• Rigorous evaluation is not available in GNU Octave due to the absence of an equivalent ldl function for indefinite symmetric matrices.
• The INTLAB toolbox is expected to be located in the folder Intlab_V12 (instead of replicated copies). Additional folders such as mode_swith_interface, verified_eig_estimation, upper_bound_matrix, functions, and results are added to the MATLAB path via the configuration script.

Configuration

Before running the main scripts, please configure your computing environment by editing (or using) the file my_intlab_mode_config.m. An excerpt of the configuration file is given below:

% my_intlab_mode_config.m
function my_intlab_mode_config()
    % The path of INTLAB toolbox and initialization.
    addpath('Intlab_V12');

    % The path of the codes for switching between verified and approximate computing.
    addpath('mode_swith_interface');
    addpath('verified_eig_estimation');
    addpath('upper_bound_matrix');
    addpath('functions');
    addpath('results');

    % Initialize INTLAB.
    startintlab;

    % Set global mode for interval arithmetic (1: verified mode).
    global INTERVAL_MODE;
    INTERVAL_MODE = 1;
end

This configuration script sets up all the required paths and initializes INTLAB.

Reproducing the Results

To reproduce the results reported in the paper:

1. Eigenvalue Bound Computation:
   Execute the shell script run_loop.sh (if available) or run the main script step1_compute_mu_hat.m. These scripts compute certified upper and lower bounds for $\lambda_2$ and $\lambda_3$ over a discretized family of triangular domains and write the results to CSV files in the results directory.

2. Verified Zero-Finding:
   Run the scripts step2_1_compute_zeros.m and step2_2_compute_no_zeros.m to rigorously compute the zeros of the implicit equation (involving the Airy function) and to certify intervals where no zeros occur. These steps are part of the overall proof strategy for showing the eigenvalue separation.

3. Testing and Development:
   The file test.m is provided for experimental purposes and testing.

File Descriptions

• README.md
  This file; it provides an overview and instructions for the repository.

• my_intlab_mode_config.m
  The configuration file that sets up the computing environment. It adds the required directories (Intlab_V12, mode_swith_interface, verified_eig_estimation, upper_bound_matrix, functions, and results) to the MATLAB path and initializes INTLAB.

• step1_compute_mu_hat.m
  The main MATLAB script for computing the eigenvalue bounds $\hat{\mu}_k$ using the Rayleigh–Ritz method with interval arithmetic. This script constructs the stiffness and mass matrices over the interval $I^{t_0}$ and computes an upper bound for $\hat{\mu}_2^{t_0}(s)$.

• step2_1_compute_zeros.m
  A script that implements verified zero-finding (using INTLAB functions) to locate the zeros of the nonlinear equation (involving the Airy function) which provides the necessary bounds for $\bar{\mu}_3(s)$.

• step2_2_compute_no_zeros.m
  A complementary script that certifies the absence of zeros in certain intervals for the implicit equation, ensuring that the computed intervals for $\kappa_3(s)$ are correct.

• upper_bound_matrix/
  A directory containing functions and scripts used to compute and handle the matrices required for the Rayleigh–Ritz method.

• functions/
  A directory containing library functions used for finite element methods (FEM) on triangular domains and other supporting computations.

• verified_eig_estimation/
  A directory with functions for rigorous eigenvalue estimation using interval arithmetic.

• results/
  A directory where the output CSV files with computed eigenvalue bounds are saved.

Citing the Code

If you use this code in your research, please cite our paper as follows:

@article{EndoLiu2024,
  title={The second Dirichlet eigenvalue over any non-equilateral triangle is simple},
  author={Endo, Ryoki and Liu, Xuefeng},
  journal={Preprint},
  year={2024},
  note={Available at \url{https://ganjin.online/ryoki/DirichletSimplicityCpllapse}}
}

Contact

For any questions or issues regarding the code, please contact:

• Ryoki Endo: endo@m.sc.niigata-u.ac.jp
• Xuefeng Liu: xfliu@cis.twcu.ac.jp