Heights by direct induction on an ordered translation quiver

@[instance_reducible]

noncomputable def MagnitudeConjecture.DirectMeshHeight.instDecidablePred_magnitudeConjecture : DecidablePred fun (p : Prop) => p

@[irreducible]

def MagnitudeConjecture.DirectMeshHeight.height {V : Type u} (rank : V → ℕ) (E : V → V → Prop) (hE : ∀ (x y : V), E x y → rank x < rank y) (x : V) : ℕ

Choose one predecessor at each nonsource vertex and count backwards.

theorem MagnitudeConjecture.DirectMeshHeight.height_eq_zero {V : Type u} (rank : V → ℕ) (E : V → V → Prop) (hE : ∀ (x y : V), E x y → rank x < rank y) (x : V) (hx : ¬∃ (y : V), E y x) : height rank E hE x = 0

An empty incoming neighborhood has height zero.

theorem MagnitudeConjecture.DirectMeshHeight.height_arrow {V : Type u} (rank : V → ℕ) (E : V → V → Prop) (hE : ∀ (x y : V), E x y → rank x < rank y) (hmesh : ∀ (x : V), (∀ (a b : V), E a x → E b x → a = b) ∨ ∃ (t : V), ∀ (y : V), E y x → E t y) (x y : V) : E x y → height rank E hE y = height rank E hE x + 1

A boundary vertex has at most one predecessor; at an interior vertex all predecessors receive an arrow from its translate. These local conditions force every arrow to increase height by exactly one.

theorem MagnitudeConjecture.DirectMeshHeight.height_mesh {V : Type u} (rank : V → ℕ) (E : V → V → Prop) (hE : ∀ (x y : V), E x y → rank x < rank y) (hmesh : ∀ (x : V), (∀ (a b : V), E a x → E b x → a = b) ∨ ∃ (t : V), ∀ (y : V), E y x → E t y) (t x : V) (hx : ∃ (y : V), E y x) (ht : ∀ (y : V), E y x → E t y) : height rank E hE x = height rank E hE t + 2

Every nonempty mesh places its target two levels above its translate.

theorem MagnitudeConjecture.DirectMeshHeight.height_path {V : Type u} (rank : V → ℕ) (E : V → V → Prop) (hE : ∀ (x y : V), E x y → rank x < rank y) [Quiver V] (hmesh : ∀ (x : V), (∀ (a b : V), E a x → E b x → a = b) ∨ ∃ (t : V), ∀ (y : V), E y x → E t y) (hedge : ∀ {x y : V} (a : x ⟶ y), E x y) {x y : V} (p : Quiver.Path x y) : height rank E hE y = height rank E hE x + p.length

Along any path, height increases by its length.

theorem MagnitudeConjecture.DirectMeshHeight.path_length_eq {V : Type u} (rank : V → ℕ) (E : V → V → Prop) (hE : ∀ (x y : V), E x y → rank x < rank y) [Quiver V] (hmesh : ∀ (x : V), (∀ (a b : V), E a x → E b x → a = b) ∨ ∃ (t : V), ∀ (y : V), E y x → E t y) (hedge : ∀ {x y : V} (a : x ⟶ y), E x y) {x y : V} (p q : Quiver.Path x y) : p.length = q.length

Any two paths with the same endpoints have equal length.