Hypergraph metric (the spec)

IsHypergraphMetric is the specification a candidate distance must satisfy to count as a metric on hypergraphs in the sense of ProofAtlas. It lives in ProofAtlas/Metric/Axioms.lean. A distance that registers against this spec — and that registration is checked at CI time — is automatically usable in the geometric profile pipeline, the hyperbolicity machinery, and every downstream theorem.

This page describes the seven fields of IsHypergraphMetric, the registration mechanism, and how each concrete metric in the next layer fills them in.

Signature

A candidate distance has type

— a function of a hypergraph $H$, a colour-weighting parameter $\pi \in \mathrm{WalkParams}$, and two vertices $u, v \in V$.

The seven fields

The structure IsHypergraphMetric (d : Hypergraph V C → WalkParams C → V → V → ℝ) bundles four metric-space axioms and three sensitivity witnesses. Pulled live from Metric/Axioms.lean ? error:

Metric-space axioms

1. Identity.

2. Symmetry.

3. Triangle inequality.

4. Non-negativity.

These four together force $d_H^\pi$ to be a pseudometric (a true metric if separation $d_H^\pi(u, v) = 0 \Rightarrow u = v$ also holds, but ProofAtlas does not require separation in the spec).

Sensitivity witnesses

A distance that ignored which side an edge points, what order its inputs are in, or which inference rule it represents, would be geometry on the wrong object. The spec demands non-trivial sensitivity to each of the four structural dimensions (D, O, C, plus A holds structurally).

5. Direction-sensitive. There exist hypergraphs $H, H'$ differing only by swapping one hyperedge's inputs and outputs, together with params and vertices $u, v$, such that $d_H^\pi(u, v) \ne d_{H'}^\pi(u, v)$.

6. Ordering-sensitive. There exist $H, H'$ differing only by permuting one hyperedge's input positions, together with params and $u, v$, such that $d_H^\pi(u, v) \ne d_{H'}^\pi(u, v)$.

7. Colour-sensitive. There exist $H$, two colour weightings $\pi, \pi'$ on the same combinatorial $H$, and $u, v$, such that $d_H^\pi(u, v) \ne d_H^{\pi'}(u, v)$.

The three witnesses are existential: a candidate metric proves it can tell two such hypergraphs apart on at least one example. This is intentionally weak — it lets us register a metric without quantifying how sensitive it is everywhere.

Registration

A metric is registered by:

1. Defining it as noncomputable def myDist ... : ℝ somewhere in ProofAtlas/Metric/.
2. Proving the instance theorem theorem myDist_isHypergraphMetric : IsHypergraphMetric (fun H π u v => myDist H π u v) in ProofAtlas/Metric/<MyDist>/Instance.lean.
3. Adding <myDist, ProofAtlas/Metric/<MyDist>/Instance.lean> to the registry in scripts/check_bdf_metric_instances.sh.

The CI check refuses to ship if the instance theorem still contains sorry. Every metric in the next layer of these docs is registered this way.

What lives in the next layer

The four registered metrics:

• Resistance distance
• Commute time distance
• Jensen–Shannon distance
• Diffusion distance

Each page describes the metric's mathematical definition, intuition, Lean signature, and the current state of its seven IsHypergraphMetric fields (proved, parameterised over a hypothesis, or still sorry).