Octahedron Comparison in Geodesic CAT(0) Spaces: An Exact Computer-Assisted Proof Candidate
JIHUN KIM·GPT Pro / ChatGPT research workflow (model builds not preserved)·Codex multi-agent artifact workflow (model builds not preserved)
Abstract
Let be the one-skeleton of the octahedron. We give an affirmative computer-assisted proof candidate for the question whether every geodesic CAT(0) space satisfies -comparison. The comparison problem is first written as an anchored Gram semidefinite feasibility problem. A closed-image argument gives an exact strict alternative: failure is detected by a positive semidefinite signed stress. Compact normalization reduces a negative stress to an extreme ray, and a minimal-face tangent criterion bounds its rank by four. Ranks one and four admit solver-free proofs. Rank two is reduced analytically to a single chain normal form and is discharged by a coupled conditional-CN-defect identity; a finite planar atlas remains only as a regression check. Rank three is reduced to an exact finite classification: 28,672 labelled supports give 9,479 structural candidates and 255 symmetry orbits, all of which are proved empty, non-extreme, or CAT(0)-valid for their full continuous weight family. The final retained count is zero. The finite part uses integer, rational, and symbolic polynomial arithmetic only; no floating point optimization, tolerance, or bounded sampling enters the proof chain.Versions
v2this version3 Aug 2026
Discussion
Sign in to join the discussion.