Gromov δ-hyperbolicity

A single real number that summarises the large-scale shape of a metric space. For hypergraphs it answers: how tree-like is the proof landscape?

The four-point condition

A metric space $(X, d)$ is δ-hyperbolic if every four-tuple of points $w, x, y, z$ satisfies

d(w, x) + d(y, z) \;\le\; \max\bigl(d(w, y) + d(x, z),\; d(w, z) + d(x, y)\bigr) + 2\delta.

Equivalently, defining the three pairings

S_1 = d(w, x) + d(y, z), \quad S_2 = d(w, y) + d(x, z), \quad S_3 = d(w, z) + d(x, y),

the four-point deviation is $\mathrm{fpd}(w, x, y, z) = \max(S_1, S_2, S_3) - \operatorname{med}(S_1, S_2, S_3)$ , and the Gromov δ-hyperbolicity constant is

\delta \;=\; \tfrac{1}{2} \cdot \sup_{w, x, y, z} \mathrm{fpd}(w, x, y, z).

A real tree is exactly $\delta = 0$ . Hyperbolic spaces (the hyperbolic plane, Cayley graphs of free groups, $\delta$ -thin metric spaces) have small bounded $\delta$ . Euclidean $\mathbb{R}^2$ has $\delta = \infty$ — for every $\delta_0$ you can find four points violating the inequality.

Intuition — large-scale tree-likeness

Two equivalent reformulations make the intuition vivid:

Thin triangles. A geodesic triangle is $\delta$ -slim if every side lies within distance $\delta$ of the union of the other two. In a $\delta$ -hyperbolic space every triangle is $\delta$ -slim. So "hyperbolic" $\approx$ "no fat triangles".

Stability of quasi-geodesics. In a hyperbolic space, any $(K, C)$ -quasi-geodesic stays within bounded distance of an actual geodesic with the same endpoints. The bound depends only on $\delta, K, C$ , not the length of the path. Translation: small detours don't compound — you can't drift far off-course by accumulating local error.

Boundary at infinity. A hyperbolic space carries a canonical boundary $\partial_\infty X$ — the equivalence classes of geodesic rays under finite-distance proximity. For hypergraphs this gives a candidate notion of limit theory even though the hypergraph itself is finite.

For proofs the consequence is: tree-like proof landscapes have predictable global geometry. Even noisy navigation through the hypergraph stays close to optimal.

The δ/diam ratio

The bare δ depends on the absolute scale of the metric — multiplying all distances by $c$ multiplies $\delta$ by $c$ . The scale-invariant version is

\widetilde\delta \;=\; \frac{\delta}{\operatorname{diam}(H)}.

This is the normalised tree-likeness ratio of paper §7. Values near $0$ mean tree-like; values near $1/2$ mean about as non-tree-like as possible.

For the demos on the front page:

Demo	δ	diam	δ/diam
`id Nat` (triangle)	0	2/3	0
`Nat.add_zero ⨯ Nat.add_comm`	≈ 0.24	≈ 3.21	≈ 0.074
3-decl glue	≈ 0.24	≈ 3.21	≈ 0.074

Numbers in the few-percent range say "almost tree-like" — exactly what you'd expect for proof terms with high reuse via const-sharing.

Metric-agnostic

The δ-hyperbolicity machinery quantifies over an arbitrary IsHypergraphMetric d, not a specific metric. Every theorem in ProofAtlas/Hyperbolicity/Basic.lean reads

{d : Hypergraph V C → WalkParams C → V → V → ℝ}
{isMetric : IsHypergraphMetric d}

so swapping resistance for Jensen–Shannon (once the latter certifies) does not invalidate any δ-result. That is what "Layer 3 is metric-agnostic" buys us.

Compute side

For $|V| \le 30$ the $O(n^4)$ enumeration over four-tuples is fine — Pipeline/Hyperbolicity.lean does it directly. For larger hypergraphs a Monte-Carlo sampling pass is the planned route (not yet wired). The compute side runs on Float and is called by #atlas.delta.

Open problem

The sole intentional sorry in the project is paper Conjecture 7.3 (ProofAtlas/Open.lean): the worst-case hyperbolicity of the universal hypergraph. Statement is type-checked; proof is open.

Try it

→ #atlas.delta A [B C ...] reports δ, diam, and δ/diam for the const-shared glue of any declaration list.

References

[BDF26] §7 — δ-hyperbolicity, Theorem 7.1, Conjecture 7.3.
[Gro87] Gromov, Hyperbolic groups, in Essays in group theory, MSRI Publ. 8, 1987.