Quality — what IsHypergraphMetric certifies

IsHypergraphMetric d is the formal spec a candidate distance must satisfy to enter ProofAtlas's metric registry. Layer 3 (δ-hyperbolicity, Hausdorff, Gromov–Hausdorff) quantifies over any d carrying this witness — so the spec is what makes the whole "swap any metric, all theorems still hold" pitch concrete.

The seven checks

structure IsHypergraphMetric (defined in ProofAtlas/Metric/Axioms.lean) demands seven fields:

Four metric axioms. For every hypergraph $H$, every walk parameter choice $\pi$, and all vertices $u, v, w$:

1. d_self — $d(u, u) = 0$
2. d_symm — $d(u, v) = d(v, u)$
3. d_triangle — $d(u, w) \le d(u, v) + d(v, w)$
4. d_nonneg — $0 \le d(u, v)$

Three BDF-sensitivity witnesses. The distance must actually depend on the BDF structure — not just be a constant or a function of $|V|$:

5. sensitive_to_direction — there exist $H, H'$ differing only by swapping a hyperedge's inputs and outputs, plus a pair $(u, v)$ on which $d$ differs.
6. sensitive_to_ordering — there exist $H, H'$ differing only by permuting one hyperedge's input positions, plus a pair on which $d$ differs.
7. sensitive_to_coloring — there exists $H$ and two colour weightings $(\pi, \pi')$ on which $d$ differs.

Fields 1–4 are the textbook metric axioms. Fields 5–7 are ProofAtlas-specific: they enforce that the metric uses the four BDF structural properties (direction, ordering, colouring, acyclicity) rather than discarding them.

Why the spec is necessary

Without 5–7, the discrete metric $d(u, v) = \mathbf{1}_{u \ne v}$ would satisfy fields 1–4 trivially. It would also be useless — it tells us nothing about the proof structure beyond "same or different". Fields 5–7 rule it out: the discrete metric does not depend on direction or ordering or colour, so it fails all three sensitivity witnesses.

More subtle counterexamples: ad-hoc distances that depend only on the underlying undirected graph (failing direction sensitivity), or only on the unordered hyperedge structure (failing ordering sensitivity), or only on the combinatorial hypergraph without colour weighting (failing colour sensitivity). The spec formalises "this metric actually uses everything BDF gives us".

Current registry

Two metrics are certified, two are in progress:

"In progress" means the instance theorem exists but its body still uses sorry. The certified ones have all seven fields discharged sorry-free; the ergodic preconditions and sensitivity witnesses are hoisted to instance parameters (see the Resistance instance for the canonical pattern).

The check is mechanical: Lean.collectAxioms walks the proof's transitive axiom closure. Sorry-free ⟺ sorryAx is not in that set.

Adding a new metric

The recipe documented in CONTRIBUTING.md:

1. Define your metric in ProofAtlas/Metric/YourMetric/Basic.lean.
2. Prove yourMetricDist_isHypergraphMetric in ProofAtlas/Metric/YourMetric/Instance.lean.
3. Run #atlas.status yourMetricDist — it should show ✓.
4. CI checks automatically (scripts/check_bdf_metric_instances.sh).

Once certified, every theorem in Layer 3 immediately applies to your metric. You get δ-hyperbolicity, Hausdorff distance, and Gromov–Hausdorff distance for free.

Try it

→ #atlas.status myDist looks up the registry and runs the sorry check live.

References

ProofAtlas/Metric/Axioms.lean — the IsHypergraphMetric definition.
scripts/check_bdf_metric_instances.sh — the CI variant of the same check.