Named positions on subdivided core edges

The Dhar configurations used for low-genus Brill--Noether arguments place chips at a few elementary expressions in edge lengths: a minimum, or a (truncated) difference. This file packages those expressions as actual vertices of SubdivisionGraph.Spec, with the elementary endpoint and interiority facts kept independent of any particular configuration.

def Utilities.Certificate.SubdivisionGraph.Spec.pathPosition {n p : ℕ} (spec : Spec n p) (edge : Fin p) (offset : ℕ) (hOffset : offset ≤ spec.length edge) : spec.PathPosition edge

The path position at a natural offset known to be no further than the head endpoint.

Equations

• spec.pathPosition edge offset hOffset = ⟨offset, ⋯⟩

@[simp]

theorem Utilities.Certificate.SubdivisionGraph.Spec.pathPosition_val {n p : ℕ} (spec : Spec n p) (edge : Fin p) (offset : ℕ) (hOffset : offset ≤ spec.length edge) : ↑(spec.pathPosition edge offset hOffset) = offset

theorem Utilities.Certificate.SubdivisionGraph.Spec.pathPosition_eq_of_val_eq {n p : ℕ} (spec : Spec n p) {edge : Fin p} {left right : spec.PathPosition edge} (h : ↑left = ↑right) : left = right

Equality of path positions follows from equality of their numerical offsets.

theorem Utilities.Certificate.SubdivisionGraph.Spec.pathVertex_eq_of_val_eq {n p : ℕ} (spec : Spec n p) (edge : Fin p) {left right : spec.PathPosition edge} (h : ↑left = ↑right) : spec.pathVertex edge left = spec.pathVertex edge right

On one core slot, equal numerical positions give equal subdivision vertices.

theorem Utilities.Certificate.SubdivisionGraph.Spec.pathVertex_eq_iff_val_eq {n p : ℕ} (spec : Spec n p) (edge : Fin p) (left right : spec.PathPosition edge) : spec.pathVertex edge left = spec.pathVertex edge right ↔ ↑left = ↑right

The numerical coordinate completely detects equality of vertices along a single subdivided, loopless core slot.

theorem Utilities.Certificate.SubdivisionGraph.Spec.pathPosition_eq_zero_iff {n p : ℕ} (spec : Spec n p) (edge : Fin p) (offset : ℕ) (hOffset : offset ≤ spec.length edge) : spec.pathPosition edge offset hOffset = ⟨0, ⋯⟩ ↔ offset = 0

@[simp]

theorem Utilities.Certificate.SubdivisionGraph.Spec.pathPosition_eq_length_iff {n p : ℕ} (spec : Spec n p) (edge : Fin p) (offset : ℕ) (hOffset : offset ≤ spec.length edge) : spec.pathPosition edge offset hOffset = ⟨spec.length edge, ⋯⟩ ↔ offset = spec.length edge

theorem Utilities.Certificate.SubdivisionGraph.Spec.isInteriorPosition_pathPosition_iff {n p : ℕ} (spec : Spec n p) (edge : Fin p) (offset : ℕ) (hOffset : offset ≤ spec.length edge) : spec.IsInteriorPosition edge (spec.pathPosition edge offset hOffset) ↔ 0 < offset ∧ offset < spec.length edge

A named position is interior exactly when its numerical offset is strictly between the two endpoints.

def Utilities.Certificate.SubdivisionGraph.Spec.minLengthPosition {n p : ℕ} (spec : Spec n p) (edge left right : Fin p) (hBound : min (spec.length left) (spec.length right) ≤ spec.length edge) : spec.PathPosition edge

The minimum of two core-edge lengths, viewed as a position on an edge which is at least that long.

Equations

• spec.minLengthPosition edge left right hBound = spec.pathPosition edge (min (spec.length left) (spec.length right)) hBound

@[simp]

theorem Utilities.Certificate.SubdivisionGraph.Spec.minLengthPosition_val {n p : ℕ} (spec : Spec n p) (edge left right : Fin p) (hBound : min (spec.length left) (spec.length right) ≤ spec.length edge) : ↑(spec.minLengthPosition edge left right hBound) = min (spec.length left) (spec.length right)

theorem Utilities.Certificate.SubdivisionGraph.Spec.minLengthPosition_pos {n p : ℕ} (spec : Spec n p) (edge left right : Fin p) (hBound : min (spec.length left) (spec.length right) ≤ spec.length edge) : 0 < ↑(spec.minLengthPosition edge left right hBound)

theorem Utilities.Certificate.SubdivisionGraph.Spec.minLengthPosition_isInterior {n p : ℕ} (spec : Spec n p) (edge left right : Fin p) (hBound : min (spec.length left) (spec.length right) ≤ spec.length edge) (hStrict : min (spec.length left) (spec.length right) < spec.length edge) : spec.IsInteriorPosition edge (spec.minLengthPosition edge left right hBound)

theorem Utilities.Certificate.SubdivisionGraph.Spec.minLengthPosition_eq_left {n p : ℕ} (spec : Spec n p) (edge left right : Fin p) (hBound : min (spec.length left) (spec.length right) ≤ spec.length edge) (h : spec.length left ≤ spec.length right) : spec.minLengthPosition edge left right hBound = spec.pathPosition edge (spec.length left) ⋯

theorem Utilities.Certificate.SubdivisionGraph.Spec.minLengthPosition_eq_right {n p : ℕ} (spec : Spec n p) (edge left right : Fin p) (hBound : min (spec.length left) (spec.length right) ≤ spec.length edge) (h : spec.length right ≤ spec.length left) : spec.minLengthPosition edge left right hBound = spec.pathPosition edge (spec.length right) ⋯

def Utilities.Certificate.SubdivisionGraph.Spec.differencePosition {n p : ℕ} (spec : Spec n p) (edge minuend subtrahend : Fin p) (hBound : spec.length minuend - spec.length subtrahend ≤ spec.length edge) : spec.PathPosition edge

The truncated difference of two core-edge lengths, viewed as a position on an edge which is at least that far from its tail.

Equations

• spec.differencePosition edge minuend subtrahend hBound = spec.pathPosition edge (spec.length minuend - spec.length subtrahend) hBound

@[simp]

theorem Utilities.Certificate.SubdivisionGraph.Spec.differencePosition_val {n p : ℕ} (spec : Spec n p) (edge minuend subtrahend : Fin p) (hBound : spec.length minuend - spec.length subtrahend ≤ spec.length edge) : ↑(spec.differencePosition edge minuend subtrahend hBound) = spec.length minuend - spec.length subtrahend

theorem Utilities.Certificate.SubdivisionGraph.Spec.differencePosition_isInterior {n p : ℕ} (spec : Spec n p) (edge minuend subtrahend : Fin p) (hBound : spec.length minuend - spec.length subtrahend ≤ spec.length edge) (hPositive : 0 < spec.length minuend - spec.length subtrahend) (hStrict : spec.length minuend - spec.length subtrahend < spec.length edge) : spec.IsInteriorPosition edge (spec.differencePosition edge minuend subtrahend hBound)

theorem Utilities.Certificate.SubdivisionGraph.Spec.differencePosition_pos_iff {n p : ℕ} (spec : Spec n p) (edge minuend subtrahend : Fin p) (hBound : spec.length minuend - spec.length subtrahend ≤ spec.length edge) : 0 < ↑(spec.differencePosition edge minuend subtrahend hBound) ↔ spec.length subtrahend < spec.length minuend

A non-truncated difference is positive precisely when the subtracted length is strictly smaller.