Step 2 · Metrics overview

ProofAtlas separates the spec of a metric from any particular instance of one. The spec is one file. The instances are many.

Two layers

1. Hypergraph metric (spec). The IsHypergraphMetric specification: four metric-space axioms (identity, symmetry, triangle inequality, non-negativity) plus three sensitivity witnesses (direction, ordering, colour). Any candidate distance that satisfies this spec is registered as a hypergraph metric and automatically usable downstream. Registration is checked at CI time.

2. Registered metrics. Concrete distances that have a sorry-free IsHypergraphMetric instance theorem. The framework is open — more can be added at any time. The metrics we currently ship:

   • Resistance distance — effective resistance in the clique-expanded conductance network. Measures how hard two propositions are to disconnect by removing inference steps.
   • Commute time distance — expected random-walk round-trip time. Dual to resistance via Doyle–Snell.
   • Jensen–Shannon distance — information-theoretic divergence between the stationary neighbourhoods of two vertices.
   • Diffusion distance — $L^2$ distance between heat-kernel rows at finite time, capturing multi-scale proximity.

Why split spec from instance

Three reasons:

• Replaceability. Any downstream theorem that needs "a metric" takes an IsHypergraphMetric hypothesis, not a specific distance. Swap in a new metric and every downstream result still applies.

• Honesty about sensitivity. The three sensitivity witnesses force every registered metric to demonstrate it distinguishes the four structural axes — a metric that quietly ignored direction or colour would fail to register.

• CI discipline. scripts/check_bdf_metric_instances.sh walks the registry and refuses to merge if any instance is sorry'd. The spec is the contract; CI is the enforcer.