Distortion of countably branching diamonds from midpoint and tree energies

Lean formalization in OpenAI math repository (Result 331)

Model / AI: OpenAI (unreleased)

OpenAI's internal frontier model proved and formalized in Lean the main result of 'Distortion of countably branching diamonds from midpoint and tree energies'. We derive quantitative distortion bounds for countably branching diamond graphs from midpoint estimates and direct tree energies. In the dual of a finite-height segment forest, every distortion-D embedding of the depth-k diamond satisfies D^2\ge1+k/4. The same bound holds in the infinite-height coordinate predual. We also obtain power-type distortion bounds for path-cost and recursive tree norms.

Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 331). The Lean development was not rebuilt locally.

• Paper — Paper
• Lean — Lean formalization note
• Code — OpenAI math repository