Degrees of and lowness for isometric isomorphism

Franklin and McNicholl

define a metric on a graph by: d_G(v₀,v₁) = 0 if v₀ = v₁ 1 if (v₀,v₁) ∈ E; 2 otherwise

They say this is "clearly" a metric. We prove this formally and generalize it, by replacing 1 and 2 by real numbers 0 < a ≤ 2b, b ≤ 2a (the fact that 0 < b follows but does not need to be mentioned).

noncomputable def franklinMcNicholl {U : Type} (G : SimpleGraph U) (a : ℝ) (b : ℝ) : U → U → ℝ

Equations

• franklinMcNicholl G a b x y = if x = y then 0 else if G.Adj x y then a else b

theorem franklinMcNicholl_ultrametric {U : Type} (G : SimpleGraph U) (a : ℝ) (h : 0 ≤ a) : let d := franklinMcNicholl G a a; ∀ (x y z : U), d x y ≤ max (d x z) (d y z)

When a=b we do have an ultrametric.

noncomputable instance franklinMcNichollMetric {U : Type} (G : SimpleGraph U) (a : ℝ) (b : ℝ) (h₀ : 0 < a) (h₁ : a ≤ b + b) (h₂ : b ≤ a + a) : MetricSpace U

Equations

• franklinMcNichollMetric G a b h₀ h₁ h₂ = MetricSpace.mk ⋯