An old edge cut after a block splice
Abstract
Block surgery on a directed cycle with distinct vertices and labels.
Theorem 1.1 (Exact complementary labels and separated prefixes).
Proof. Machine-checked in Lean as D5/S1/Words/Sequenceability/BlockSpliceOrdering.block_splice_ordering (✓ std3). ∎
Source. Repository-derived.
Commentary.
Let G be any additive commutative group. Distinct cyclic vertices z(0),…,z(N-1) have distinct labels c(i)=z((i+1) mod N)-z(i). For 2 <= k <= t < N, assume the chord z(k)-z(0) equals c(t). The construction cuts the old edge indexed by t and retains the new chord. It orders exactly the labels c(k),…,c(N-1), each once. All bounded prefix sums, including empty and full prefixes, are distinct; every nonempty bounded interval has nonzero sum. The full sum is -c(t) and is nonzero.
The explicit path traverses z(t+1),…,z(N-1), then z(0), then z(k),…,z(t). Its label indices are t+1,…,N-1, then t for the new chord, then k,…,t-1. The three disjoint index blocks prove both inventories and distinctness. The initial block can be empty when t=N-1, and the last label block can be empty when t=k, including simultaneous emptiness. The label equality identifies values, not edge occurrences. No distinction between old and new label values, or restriction on characteristic, is assumed.
The result also returns a path P whose bounded vertices permute z(0),z(k),…,z(N-1), with no repetitions. The word consists of consecutive differences of P. Existing list telescoping gives every prefix as P(j)-P(0); prefix splitting then proves the interval assertion. In the displayed formula, rangeFrom(k,n) denotes List.range’ k n, map takes the function first, and take and drop take the count first. List operations otherwise have their usual meanings. The statement is a general cycle surgery result; finite-field primitive elements, independence and transport to a prescribed frame are separate premises needed to apply it to independent omitted vectors.