Verification Appendix
This appendix records the computer-assisted certificate used for the scalar inequality in Theorem 2. All reported bounds use directed outward rounding.
Certified statement. For the exact decimal parameters \(\alpha=0.6342\) and \(\lambda=0.4506\),
\[ J(0.6342,0.4506)<-0.00005<0. \]Validated computation
The verification uses Arb ball arithmetic through
python-flint 0.9.0 at 80 decimal digits. It partitions
\([0,1/2]\) into \(2^{16}\) rational cells. On each cell, sign-verified interval
brackets enclose the unique optimizer in the definition of \(\Gamma_\lambda\), and
directed rounding encloses the resulting value. Coordinatewise monotonicity controls
the cell adjacent to \(t=0\).
Summing the cellwise upper bounds gives an upper endpoint below \(-0.0000512188\), which is strictly smaller than \(-0.00005\). Ordinary high-precision quadrature is used only as an independent numerical check, not as part of the proof.
Reproduction
From the project root, install the pinned dependency and run:
python -m pip install -r verification/requirements.txt python verification/certify_j_arb.py --cells 65536 --dps 80
The verification program, dependency specification, and technical notes accompany the manuscript.