First public release of the exact computer-assisted proof candidate for Petrunin Problem 9 (octahedron comparison in geodesic CAT(0) spaces). Status: proof candidate; not human peer reviewed. Preserved record: https://doi.org/10.5281/zenodo.21772560. Canonical artifact SHA-256: c0cd61d2b67af21ff6c5a4e448b2c8dae4aeba82ae07fed9a306a7af25c09e19.