Degree-one equivalence is generated by separating edges

On a connected graph, a firing script whose principal divisor is (y)-(x) can be peeled one maximum level at a time. Each peel exposes a unique separating edge leaving the maximum set. This is the graph-theoretic input needed to show that a script normalized across every bridge is constant on the degree-one divisor classes.

theorem Utilities.target_not_mem_topSet_of_prin_eq_oneChip_sub {G : CFGraph} {sigma : firingScript G} {x y : G.V} (hxy : x ≠ y) (hPrincipal : (prin G) sigma = oneChip y - oneChip x) : y ∉ topSet sigma

The positive endpoint of a nontrivial principal one-chip difference is never in the maximum level set of its witnessing script.

theorem Utilities.source_mem_topSet_of_prin_eq_oneChip_sub {G : CFGraph} (hConnected : graphConnected G) {sigma : firingScript G} {x y : G.V} (hxy : x ≠ y) (hPrincipal : (prin G) sigma = oneChip y - oneChip x) : x ∈ topSet sigma

In a connected graph, the negative endpoint of a principal one-chip difference lies in the maximum level set of every witnessing script.

theorem Utilities.exists_separatingEdgeCut_of_prin_eq_oneChip_sub {G : CFGraph} (hConnected : graphConnected G) {sigma : firingScript G} {x y : G.V} (hxy : x ≠ y) (hPrincipal : (prin G) sigma = oneChip y - oneChip x) : ∃ (z : G.V) (cut : SeparatingEdgeCut G x z), cut.side = topSet sigma

The maximum-set peel of a one-chip equivalence exposes a separating edge at the negative endpoint.

theorem Utilities.eq_of_chipEquivalent_of_separating_normalized {G : CFGraph} (hConnected : graphConnected G) (rho : firingScript G) (hNormalized : ∀ {a b : G.V} (cut : SeparatingEdgeCut G a b), rho a = rho b) {x y : G.V} (hEquivalent : linearEquiv G (oneChip x) (oneChip y)) : rho x = rho y

A script which is normalized across every separating edge is constant on every degree-one divisor class of a connected graph. The proof peels the maximum set of a one-chip-equivalence witness and inducts on its endpoint height difference.