The seam displacement calculus

Fix a graph H, two marks x ≠ y, the seam divisor α = (x) - (y) (seamDivisor, from EdgeAddition.lean), and a base divisor C. For m : ℤ the m-twist is C + m • α (seamTwist). A firing script f : V → ℤ acts on divisors through prin H f (the note's Δf), and its displacement is t(f) = f x - f y (displacement). The displacement set of the m-twist is

d(A_m) = { t(f) : C + m • α + Δf ≥ 0 } (IsDisplacement).

The junction class of the pair m | m+1 is ξ_m = [C + m•α - (y)] = [C + (m+1)•α - (x)] (junction), and the junction has a gap when every displacement of the (m+1)-twist strictly exceeds every displacement of the m-twist (HasGap). The main theorem, hasGap_iff, is Theorem C together with Theorem C′ of §5/§12:

HasGap C x y m ↔ ¬ winnable H (junction C x y m).

Index of the main results

• script_min_at_of_qReduced — the master lemma (level-set firing).
• script_const_of_prin_eq_zero, displacement_eq_of_prin_eq — t is well defined on representatives (uses connectedness).
• winnable_sub_one_chip_iff_of_qReduced — the chip test for reduced divisors.
• isMaxDisplacement_of_qReduced_y, isMinDisplacement_of_qReduced_x — Proposition 1, extremal half: b_m is attained at the y-reduced representative, a_m at the x-reduced one.
• isDisplacement_succ_of_junction_winnable, isDisplacement_succ_of_isMaxDisplacement — Theorem C.
• isDisplacement_pred_of_junction_winnable, isDisplacement_of_isMinDisplacement_succ — Theorem C from the x-side (the same junction class controls the junction from both sides).
• le_displacement_of_qReduced_succ, exists_isDisplacement_succ_ge, isMaxDisplacement_mono, exists_isDisplacement_le — Lemma M.
• lt_script_of_qReduced_no_chip, hasGap_of_junction_not_winnable — Theorem C′, and hasGap_iff for the equivalence.
• not_hasGap_of_rank_pos — Corollary C1.

Phase-0 API survey (.lake/packages/chip-firing-with-lean)

What the library has (all of it used below):

• CFDiv G = G.V → ℤ, oneChip v, effective D = ∀ v, D v ≥ 0, deg, winnable G D, linearEquiv G D D', principalDivisors G (ChipFiringWithLean.Basic).
• Firing scripts as plain functions: firingScript G = G.V → ℤ together with the additive map prin G : firingScript G →+ CFDiv G, given by prin G σ v = ∑ u, (σ u - σ v) * numEdges G v u. This is the Δ of the note (the negative of the Laplacian action; see the docstring of prin). principal_iff_eq_prin identifies principalDivisors with the image of prin. There is also firingVector, setFiring, laplacianMatrix, applyLaplacian, none of which are needed here.
• qReduced G q D: qEffective q D together with "every nonempty S ⊆ V ∖ {q} contains a vertex v with D v < ∑ w ∉ S, numEdges G v w" — i.e. no q-avoiding set is legal.
• exists_q_reduced_representative and unique_q_reduced (both need graphConnected), q_reduced_unique, qReducedRep (RRGHelpers), winnable_iff_q_reduced_effective, effective_of_winnable_and_q_reduced.
• winnable_equiv_winnable, winnable_of_effective, rank, rank_geq_iff, rank_nonneg_iff_winnable, Riemann–Roch.
• seamDivisor x y = oneChip x - oneChip y (Utilities.EdgeAddition).

What the library lacks, and how it is handled here:

• Dhar's algorithm as a certified firing path. Algorithms.lean defines dhar_outdeg, dharBurningSet, findQReducedDivisor, dhar, burn, but proves nothing about them: there is no lemma "every effective divisor reaches its q-reduced representative by a finite sequence of legal q-avoiding firings". Consequently the interval half of Proposition 1 of the note ("every intermediate displacement is attained") is not formalized here. Nothing below needs it: the extremal half of Proposition 1, Lemma M, Theorem C and Theorem C′ are all proved by direct level-set (threshold-firing) arguments, unconditionally.
• Level sets of a script. Basic.lean contains a private lemma maxset_of_script with exactly the required inequality, but it is private and hard-wired to one particular level set. It is re-proved here as topSet, prin_le_neg_outdeg_S, and the botSet mirror outdeg_S_le_prin.
• "A q-reduced D satisfies D q ≥ 1 iff [D] - (q) is effective". Absent; proved here as winnable_sub_one_chip_iff_of_qReduced.
• "Two scripts with the same principal divisor differ by a constant". Absent (only the connectivity-free qReducer shadow, which is private); proved here as script_const_of_prin_eq_zero.
• ℚ-valued potentials and effective resistance: absent. Theorems B and D of the note need them and are deliberately not attempted.

No sorry, no new axioms, no stated-but-unproved hypotheses: every result below is proved outright from the library's API.

Pointwise lemmas for chips and seams

theorem Utilities.one_chip_self {H : CFGraph} (v : H.V) : oneChip v v = 1

theorem Utilities.sub_one_chip_apply_self {H : CFGraph} (D : CFDiv H) (q : H.V) : (D - oneChip q) q = D q - 1

theorem Utilities.sub_one_chip_apply_of_ne {H : CFGraph} (D : CFDiv H) {q v : H.V} (h : v ≠ q) : (D - oneChip q) v = D v

theorem Utilities.seamDivisor_apply_of_ne {H : CFGraph} {x y v : H.V} (hvx : v ≠ x) (hvy : v ≠ y) : seamDivisor x y v = 0

theorem Utilities.seamDivisor_apply_left {H : CFGraph} {x y : H.V} (hxy : x ≠ y) : seamDivisor x y x = 1

theorem Utilities.seamDivisor_apply_right {H : CFGraph} {x y : H.V} (hxy : x ≠ y) : seamDivisor x y y = -1

theorem Utilities.seamDivisor_nonneg_of_ne_right {H : CFGraph} (x y : H.V) {w : H.V} (hw : w ≠ y) : 0 ≤ seamDivisor x y w

Away from y the seam divisor is nonnegative.

Level sets of a firing script

The argmax level set topSet g and its mirror botSet g = topSet (-g). One fact drives the whole calculus: at a vertex of topSet g the script g removes at least the out-degree of the level set (prin_le_neg_outdeg_S), so a level set avoiding q is a legal firing set and therefore certifies non-q-reducedness.

def Utilities.topSet {H : CFGraph} (g : firingScript H) : Finset H.V

The set of vertices where a firing script attains its maximum.

Equations

• Utilities.topSet g = {v : H.V | ∀ (u : H.V), g u ≤ g v}

def Utilities.botSet {H : CFGraph} (g : firingScript H) : Finset H.V

The set of vertices where a firing script attains its minimum.

Equations

• Utilities.botSet g = Utilities.topSet (-g)

theorem Utilities.mem_topSet {H : CFGraph} {g : firingScript H} {v : H.V} : v ∈ topSet g ↔ ∀ (u : H.V), g u ≤ g v

theorem Utilities.mem_botSet {H : CFGraph} {g : firingScript H} {v : H.V} : v ∈ botSet g ↔ ∀ (u : H.V), g v ≤ g u

theorem Utilities.topSet_nonempty {H : CFGraph} (g : firingScript H) : (topSet g).Nonempty

theorem Utilities.botSet_nonempty {H : CFGraph} (g : firingScript H) : (botSet g).Nonempty

theorem Utilities.lt_of_not_mem_topSet {H : CFGraph} {g : firingScript H} {v u : H.V} (hv : v ∈ topSet g) (hu : u ∉ topSet g) : g u < g v

Outside the argmax level set the script is strictly smaller.

theorem Utilities.prin_le_neg_outdeg_S {H : CFGraph} {g : firingScript H} {v : H.V} (hv : v ∈ topSet g) : (prin H) g v ≤ -outdegreeSet H (topSet g) v

The level-set inequality. Firing a script whose maximum is attained at v costs v at least its out-degree from the maximal level set.

theorem Utilities.outdeg_S_le_prin {H : CFGraph} {g : firingScript H} {v : H.V} (hv : v ∈ botSet g) : outdegreeSet H (botSet g) v ≤ (prin H) g v

The argmin mirror of prin_le_neg_outdeg_S.

theorem Utilities.script_const_of_prin_eq_zero {H : CFGraph} (hconn : graphConnected H) {g : firingScript H} (h : (prin H) g = 0) (u v : H.V) : g u = g v

Connectivity ⇒ the kernel of Δ consists of the constant scripts.

q-reduced divisors: the chip test

A q-reduced divisor stays q-reduced after a chip is removed at q, which converts "the class minus (q) is effective" into the pointwise test D q ≥ 1.

theorem Utilities.q_reduced_sub_one_chip {H : CFGraph} {q : H.V} {D : CFDiv H} (h : qReduced H q D) : qReduced H q (D - oneChip q)

theorem Utilities.winnable_sub_one_chip_iff_of_qReduced {H : CFGraph} {q : H.V} {D : CFDiv H} (h : qReduced H q D) : winnable H (D - oneChip q) ↔ 1 ≤ D q

The chip test. For a q-reduced divisor D, the class [D] - (q) is effective exactly when D already carries a chip at q.

Scripts, twists and displacements

def Utilities.seamTwist {H : CFGraph} (C : CFDiv H) (x y : H.V) (m : ℤ) : CFDiv H

The m-th seam twist C + m • α of the base divisor C.

Equations

• Utilities.seamTwist C x y m = C + m • Utilities.seamDivisor x y

def Utilities.displacement {H : CFGraph} (x y : H.V) (f : firingScript H) : ℤ

The displacement t(f) = f x - f y of a firing script.

Equations

• Utilities.displacement x y f = f x - f y

def Utilities.IsDisplacement {H : CFGraph} (C : CFDiv H) (x y : H.V) (m t : ℤ) : Prop

t is a displacement of the m-twist: some script puts the m-twist into effective position with displacement t.

Equations

• Utilities.IsDisplacement C x y m t = ∃ (f : firingScript H), effective (Utilities.seamTwist C x y m + (prin H) f) ∧ Utilities.displacement x y f = t

def Utilities.displacementSet {H : CFGraph} (C : CFDiv H) (x y : H.V) (m : ℤ) : Set ℤ

The displacement set d(A_m) of the m-twist.

Equations

• Utilities.displacementSet C x y m = {t : ℤ | Utilities.IsDisplacement C x y m t}

@[simp]

theorem Utilities.mem_displacementSet {H : CFGraph} {C : CFDiv H} {x y : H.V} {m t : ℤ} : t ∈ displacementSet C x y m ↔ IsDisplacement C x y m t

def Utilities.IsMaxDisplacement {H : CFGraph} (C : CFDiv H) (x y : H.V) (m t : ℤ) : Prop

t is the largest displacement of the m-twist (b_m of the note).

Equations

• Utilities.IsMaxDisplacement C x y m t = (Utilities.IsDisplacement C x y m t ∧ ∀ (s : ℤ), Utilities.IsDisplacement C x y m s → s ≤ t)

def Utilities.IsMinDisplacement {H : CFGraph} (C : CFDiv H) (x y : H.V) (m t : ℤ) : Prop

t is the smallest displacement of the m-twist (a_m of the note).

Equations

• Utilities.IsMinDisplacement C x y m t = (Utilities.IsDisplacement C x y m t ∧ ∀ (s : ℤ), Utilities.IsDisplacement C x y m s → t ≤ s)

def Utilities.junction {H : CFGraph} (C : CFDiv H) (x y : H.V) (m : ℤ) : CFDiv H

The junction class ξ_m = [C + m•α - (y)] of the pair m | m+1.

Equations

• Utilities.junction C x y m = Utilities.seamTwist C x y m - oneChip y

@[simp]

theorem Utilities.displacement_const {H : CFGraph} (x y : H.V) (c : ℤ) : (displacement x y fun (x : H.V) => c) = 0

A constant script has zero displacement.

theorem Utilities.seamTwist_succ {H : CFGraph} (C : CFDiv H) (x y : H.V) (m : ℤ) : seamTwist C x y (m + 1) = seamTwist C x y m + seamDivisor x y

theorem Utilities.junction_eq_succ_sub_x {H : CFGraph} (C : CFDiv H) (x y : H.V) (m : ℤ) : junction C x y m = seamTwist C x y (m + 1) - oneChip x

The junction class seen from the right: ξ_m = [C + (m+1)•α - (x)].

Displacement is well defined on representatives

theorem Utilities.linear_equiv_add_prin {H : CFGraph} (D : CFDiv H) (f : firingScript H) : linearEquiv H D (D + (prin H) f)

theorem Utilities.winnable_add_prin_iff {H : CFGraph} (D : CFDiv H) (f : firingScript H) : winnable H (D + (prin H) f) ↔ winnable H D

theorem Utilities.displacement_eq_of_prin_eq {H : CFGraph} (hconn : graphConnected H) (x y : H.V) {f f' : firingScript H} (h : (prin H) f = (prin H) f') : displacement x y f = displacement x y f'

t is well defined on representatives. On a connected graph two scripts with the same principal divisor differ by a constant, hence have the same displacement.

theorem Utilities.displacement_eq_of_div_eq {H : CFGraph} (hconn : graphConnected H) (C : CFDiv H) (x y : H.V) (m : ℤ) {f f' : firingScript H} (h : seamTwist C x y m + (prin H) f = seamTwist C x y m + (prin H) f') : displacement x y f = displacement x y f'

Hence the displacement attached to an effective representative of a twist depends only on the representative.

theorem Utilities.isDisplacement_zero_of_effective {H : CFGraph} (C : CFDiv H) (x y : H.V) (hC : effective C) : IsDisplacement C x y 0 0

Non-vacuity: an effective base divisor has displacement 0 at twist 0.

theorem Utilities.winnable_of_isDisplacement {H : CFGraph} {C : CFDiv H} {x y : H.V} {m t : ℤ} (h : IsDisplacement C x y m t) : winnable H (seamTwist C x y m)

theorem Utilities.exists_qReduced_script {H : CFGraph} (hconn : graphConnected H) (q : H.V) (A : CFDiv H) (hw : winnable H A) : ∃ (f : firingScript H), effective (A + (prin H) f) ∧ qReduced H q (A + (prin H) f)

Every winnable divisor has a q-reduced effective representative, presented as an explicit script.

The master lemma

Everything below rests on one statement: if a q-reduced divisor is reached from an effective divisor by adding a divisor that is nonnegative off q and then firing a script g, then g attains its minimum at q.

theorem Utilities.script_min_at_of_qReduced {H : CFGraph} (q : H.V) (D β : CFDiv H) (g : firingScript H) (hD : effective D) (hβ : ∀ (w : H.V), w ≠ q → 0 ≤ β w) (hred : qReduced H q (D + β + (prin H) g)) (w : H.V) : g q ≤ g w

Master lemma. Let D be effective, let β be nonnegative away from q, and suppose D + β + Δg is q-reduced. Then g is minimized at q.

Proposition 1 (extremal half): the reduced representatives are extremal

The y-reduced representative maximizes the displacement, the x-reduced one minimizes it. (The other half of Proposition 1 of the note — that every intermediate integer is attained, so that d(A_m) is an interval — requires the Dhar reduction path, which the library does not certify. It is not used anywhere below.)

theorem Utilities.isMaxDisplacement_of_qReduced_y {H : CFGraph} (C : CFDiv H) (x y : H.V) (m : ℤ) {f : firingScript H} (heff : effective (seamTwist C x y m + (prin H) f)) (hred : qReduced H y (seamTwist C x y m + (prin H) f)) : IsMaxDisplacement C x y m (displacement x y f)

The y-reduced effective representative attains the maximal displacement.

theorem Utilities.isMinDisplacement_of_qReduced_x {H : CFGraph} (C : CFDiv H) (x y : H.V) (m : ℤ) {f : firingScript H} (heff : effective (seamTwist C x y m + (prin H) f)) (hred : qReduced H x (seamTwist C x y m + (prin H) f)) : IsMinDisplacement C x y m (displacement x y f)

The x-reduced effective representative attains the minimal displacement.

theorem Utilities.exists_isMaxDisplacement {H : CFGraph} (hconn : graphConnected H) (C : CFDiv H) (x y : H.V) (m : ℤ) (hw : winnable H (seamTwist C x y m)) : ∃ (b : ℤ), IsMaxDisplacement C x y m b

A winnable twist has a maximal displacement.

theorem Utilities.exists_isMinDisplacement {H : CFGraph} (hconn : graphConnected H) (C : CFDiv H) (x y : H.V) (m : ℤ) (hw : winnable H (seamTwist C x y m)) : ∃ (a : ℤ), IsMinDisplacement C x y m a

A winnable twist has a minimal displacement.

theorem Utilities.IsMaxDisplacement.unique {H : CFGraph} {C : CFDiv H} {x y : H.V} {m b b' : ℤ} (h : IsMaxDisplacement C x y m b) (h' : IsMaxDisplacement C x y m b') : b = b'

theorem Utilities.IsMinDisplacement.unique {H : CFGraph} {C : CFDiv H} {x y : H.V} {m a a' : ℤ} (h : IsMinDisplacement C x y m a) (h' : IsMinDisplacement C x y m a') : a = a'

Theorem C: an effective junction class kills the gap

theorem Utilities.junction_winnable_iff_chip {H : CFGraph} (C : CFDiv H) (x y : H.V) (m : ℤ) {f : firingScript H} (hred : qReduced H y (seamTwist C x y m + (prin H) f)) : winnable H (junction C x y m) ↔ 1 ≤ (seamTwist C x y m + (prin H) f) y

The junction class ξ_m is effective iff the y-reduced representative of the m-twist carries a chip at y.

theorem Utilities.isDisplacement_succ_of_junction_winnable {H : CFGraph} (C : CFDiv H) (x y : H.V) (hxy : x ≠ y) (m : ℤ) {f : firingScript H} (heff : effective (seamTwist C x y m + (prin H) f)) (hred : qReduced H y (seamTwist C x y m + (prin H) f)) (hjun : winnable H (junction C x y m)) : IsDisplacement C x y (m + 1) (displacement x y f)

Theorem C (forward form). If the junction class ξ_m is effective then the y-reduced effective representative of the m-twist, translated by the seam, is an effective representative of the (m+1)-twist with the same script — hence with the same displacement.

theorem Utilities.isDisplacement_succ_of_isMaxDisplacement {H : CFGraph} (hconn : graphConnected H) (C : CFDiv H) (x y : H.V) (hxy : x ≠ y) (m b : ℤ) (hb : IsMaxDisplacement C x y m b) (hjun : winnable H (junction C x y m)) : IsDisplacement C x y (m + 1) b

Theorem C, packaged. If the junction class is effective then the maximal displacement of the m-twist is again a displacement of the (m+1)-twist; in particular b_{m+1} ≥ b_m, i.e. gap_m ≤ 0.

Lemma M: monotonicity of the displacement interval

theorem Utilities.le_displacement_of_qReduced_succ {H : CFGraph} (C : CFDiv H) (x y : H.V) (m : ℤ) {f f' : firingScript H} (heff : effective (seamTwist C x y m + (prin H) f)) (hred' : qReduced H y (seamTwist C x y (m + 1) + (prin H) f')) : displacement x y f ≤ displacement x y f'

Lemma M (b-side, non-strict). Every displacement of the m-twist is at most the displacement of the y-reduced representative of the (m+1)-twist. Equivalently b_m ≤ b_{m+1}.

theorem Utilities.exists_isDisplacement_succ_ge {H : CFGraph} (hconn : graphConnected H) (C : CFDiv H) (x y : H.V) (m s : ℤ) (hs : IsDisplacement C x y m s) (hw : winnable H (seamTwist C x y (m + 1))) : ∃ (t : ℤ), IsDisplacement C x y (m + 1) t ∧ s ≤ t

Lemma M, ∃-representative form. If the (m+1)-twist is winnable then every displacement of the m-twist is dominated by some displacement of the (m+1)-twist.

theorem Utilities.isMaxDisplacement_mono {H : CFGraph} (hconn : graphConnected H) (C : CFDiv H) (x y : H.V) (m b b' : ℤ) (hb : IsMaxDisplacement C x y m b) (hb' : IsMaxDisplacement C x y (m + 1) b') : b ≤ b'

Lemma M, maximal form: b_m ≤ b_{m+1}.

Theorem C′: a non-effective junction class forces a gap

This is §12 of the note. The argument there runs a terminating level-set firing iteration; the proof below shortcuts it. A single level set decides the matter: a y-reduced representative of the m-twist with no chip at y cannot tolerate y sitting at the top level of the transition script.

theorem Utilities.lt_script_of_qReduced_no_chip {H : CFGraph} (x y : H.V) (hxy : x ≠ y) {D : CFDiv H} {g : firingScript H} (hDred : qReduced H y D) (hDy : D y = 0) (heff : effective (D + seamDivisor x y + (prin H) g)) : g y < g x

The level-set core of Theorem C′. Let D be effective and y-reduced with no chip at y, and suppose D + α + Δg is effective. Then g is strictly larger at x than at y: the seam step strictly increases the displacement.

def Utilities.HasGap {H : CFGraph} (C : CFDiv H) (x y : H.V) (m : ℤ) : Prop

The junction m | m+1 has a gap: every displacement of the (m+1)-twist strictly exceeds every displacement of the m-twist. In the notation of the note this is gap_m = a_{m+1} - b_m ≥ 1.

Equations

• Utilities.HasGap C x y m = ∀ (s t : ℤ), Utilities.IsDisplacement C x y m s → Utilities.IsDisplacement C x y (m + 1) t → s < t

theorem Utilities.hasGap_of_junction_not_winnable {H : CFGraph} (hconn : graphConnected H) (C : CFDiv H) (x y : H.V) (hxy : x ≠ y) (m : ℤ) (hjun : ¬winnable H (junction C x y m)) : HasGap C x y m

Theorem C′. A non-effective junction class forces a gap.

theorem Utilities.not_hasGap_of_junction_winnable {H : CFGraph} (hconn : graphConnected H) (C : CFDiv H) (x y : H.V) (hxy : x ≠ y) (m : ℤ) (hw : winnable H (seamTwist C x y m)) (hjun : winnable H (junction C x y m)) : ¬HasGap C x y m

Theorem C, contrapositive form. An effective junction class rules out a gap (assuming the m-twist is winnable, so that there is something to rule out).

theorem Utilities.hasGap_iff {H : CFGraph} (hconn : graphConnected H) (C : CFDiv H) (x y : H.V) (hxy : x ≠ y) (m : ℤ) (hw : winnable H (seamTwist C x y m)) : HasGap C x y m ↔ ¬winnable H (junction C x y m)

Theorem C iff Theorem C′ (gap rigidity is an equivalence). For a winnable m-twist on a connected graph, the junction m | m+1 has a gap exactly when its junction class ξ_m = [C + m•α - (y)] = [C + (m+1)•α - (x)] fails to be effective.

theorem Utilities.not_hasGap_of_rank_pos {H : CFGraph} (hconn : graphConnected H) (C : CFDiv H) (x y : H.V) (hxy : x ≠ y) (m : ℤ) (hrank : 1 ≤ rank H (seamTwist C x y m)) : ¬HasGap C x y m

Corollary C1 (rank kills gaps). If the m-twist has positive rank then its junction class is effective, so the junction m | m+1 has no gap.

theorem Utilities.exists_isDisplacement_succ_gt {H : CFGraph} (hconn : graphConnected H) (C : CFDiv H) (x y : H.V) (hxy : x ≠ y) (m s : ℤ) (hs : IsDisplacement C x y m s) (hw : winnable H (seamTwist C x y (m + 1))) (hjun : ¬winnable H (junction C x y m)) : ∃ (t : ℤ), IsDisplacement C x y (m + 1) t ∧ s < t

Lemma M, strict form. When the junction class is not effective the displacement strictly increases: b_{m+1} ≥ b_m + 1.

The x ↔ y symmetry, and the a-side of Lemma M

Swapping the two marks negates the seam, the twist index and the displacement.

theorem Utilities.seamDivisor_swap {H : CFGraph} (x y : H.V) : seamDivisor y x = -seamDivisor x y

theorem Utilities.seamTwist_swap {H : CFGraph} (C : CFDiv H) (x y : H.V) (m : ℤ) : seamTwist C y x m = seamTwist C x y (-m)

theorem Utilities.displacement_swap {H : CFGraph} (x y : H.V) (f : firingScript H) : displacement y x f = -displacement x y f

theorem Utilities.isDisplacement_swap {H : CFGraph} (C : CFDiv H) (x y : H.V) (m t : ℤ) : IsDisplacement C y x m t ↔ IsDisplacement C x y (-m) (-t)

theorem Utilities.junction_swap {H : CFGraph} (C : CFDiv H) (x y : H.V) (m : ℤ) : junction C y x m = junction C x y (-m - 1)

theorem Utilities.isDisplacement_pred_of_junction_winnable {H : CFGraph} (C : CFDiv H) (x y : H.V) (hxy : x ≠ y) (m : ℤ) {f : firingScript H} (heff : effective (seamTwist C x y (m + 1) + (prin H) f)) (hred : qReduced H x (seamTwist C x y (m + 1) + (prin H) f)) (hjun : winnable H (junction C x y m)) : IsDisplacement C x y m (displacement x y f)

Theorem C, x-side form. The junction has a single obstruction class, seen from both sides (§5 of the note): the same hypothesis ξ_m = [C + (m+1)•α - (x)] effective shows that the x-reduced effective representative of the (m+1)-twist, translated back by the seam, is an effective representative of the m-twist with the same script.

theorem Utilities.isDisplacement_of_isMinDisplacement_succ {H : CFGraph} (hconn : graphConnected H) (C : CFDiv H) (x y : H.V) (hxy : x ≠ y) (m a : ℤ) (ha : IsMinDisplacement C x y (m + 1) a) (hjun : winnable H (junction C x y m)) : IsDisplacement C x y m a

Theorem C, x-side packaged. If the junction class is effective, the minimal displacement of the (m+1)-twist is again a displacement of the m-twist; in particular a_m ≤ a_{m+1} is not strict.

theorem Utilities.exists_isDisplacement_le {H : CFGraph} (hconn : graphConnected H) (C : CFDiv H) (x y : H.V) (m t : ℤ) (ht : IsDisplacement C x y (m + 1) t) (hw : winnable H (seamTwist C x y m)) : ∃ (s : ℤ), IsDisplacement C x y m s ∧ s ≤ t

Lemma M (a-side). If the m-twist is winnable then every displacement of the (m+1)-twist dominates some displacement of the m-twist: a_m ≤ a_{m+1}.

theorem Utilities.exists_isDisplacement_lt {H : CFGraph} (hconn : graphConnected H) (C : CFDiv H) (x y : H.V) (hxy : x ≠ y) (m t : ℤ) (ht : IsDisplacement C x y (m + 1) t) (hw : winnable H (seamTwist C x y m)) (hjun : ¬winnable H (junction C x y m)) : ∃ (s : ℤ), IsDisplacement C x y m s ∧ s < t

The a-side gap statement. A non-effective junction class also forces the strict inequality on the x-reduced side.