Rank change under one marked chip

Adding one effective chip cannot lower rank. Conversely, subtracting one chip can lower a specified rank lower bound by at most one. The latter is proved directly from the universal effective-subtraction definition of rank.

These two inequalities are the rank-side input for propagating transmission conditions between adjacent lattice rows.

theorem Utilities.rank_add_one_chip_ge {G : CFGraph} (D : CFDiv G) (q : G.V) (k : ℤ) (hRank : rank G D ≥ k) : rank G (D + oneChip q) ≥ k

Adding one chip preserves every rank lower bound.

theorem Utilities.rank_sub_one_chip_ge_of_rank_ge_succ {G : CFGraph} (D : CFDiv G) (q : G.V) (k : ℤ) (hRank : rank G D ≥ k + 1) : rank G (D - oneChip q) ≥ k

If D has rank at least k+1, then removing one chip leaves rank at least k.

theorem Utilities.rank_sub_one_chip_ge_rank_sub_one {G : CFGraph} (D : CFDiv G) (q : G.V) : rank G (D - oneChip q) ≥ rank G D - 1

Numerical corollary: subtracting one chip lowers rank by at most one.