# Verification of the spherical simplex bound

The analytic argument checks positive spherical duality, inverse Gram coordinates, determinant cancellation, the pointwise quadratic square, every hypothesis of the classical geometric-mean integration theorem, and its equality characterization. The second variation is derived from half-normal moments, with a dominated-derivative argument and a dimension-dependent local remainder bound.

The reproducibility script passes 104 exact symbolic or rational checks and 46 numerical sanity conditions. Normal and optimized Python reports agree. The symbolic tests include the full edge-variable moment polynomials in dimensions two through six, rather than only selected numeric coefficients. Rational matrix tests cover dimensions one through seven. Seeded approximate Gaussian CDF evaluations cover 35 positive definite matrices in dimensions two through eight, supplemented by seven planar formulas and four orthants.

The proof is all-dimensional and does not depend on the finite checks. This audit is by the originating researcher, not an independent referee or formal proof checker. The underlying functional inequality is classical, and historical novelty of the spherical corollary or second-variation formula is not certified.