Affine row orbits and a characteristic-five lift
Abstract
Affine row orbits give exact lifted cycles and differences over finite fields of characteristic five.
All universe levels, field structures and finite fields in the displayed quantifiers are included. Operations use the bound field structure f. The map rowReturn(r,c) sends h to c+r(h-c), where r is a unit. SameCycle is the orbit relation of the actual permutation under integer powers.
Theorem 1.1 (Two affine row orbits).
Proof. Machine-checked in Lean as D5/S1/Words/Sequenceability/RowOrbitLift.row_same_cycle_iff (✓ std3). ∎
Source. Repository-derived.
Commentary.
When every unit is a natural power of r, the center c is fixed and every other row belongs to one orbit. For a and b different from c, choose a power of r equal to (b-c)/(a-c). The n-th return is c+r^n(a-c), so that power sends a to b. Conversely, a permutation orbit meeting a fixed point contains only that point.
The state space is Fin(4) times K. Its actual vertices are vertex(i,h)=(column(i),h), where column=(1,2,4,3) in ZMod(5). The successor lift(r,c) sends (0,h),(1,h),(2,h) to (1,-h),(2,-h),(3,-h), respectively, and sends (3,h) to (0,-rh+(1-r)c). The first row initialRow(i,h) is h at phases 0 and 2 and -h at phases 1 and 3. The edgeLabel is vertex(lift(r,c)(v))-vertex(v), with coefficient one.
Theorem 1.2 (Exact cycles and closing-edge inventory over every finite rowfield).
Proof. Machine-checked in Lean as D5/S1/Words/Sequenceability/RowOrbitLift.exists_characteristic_five_lift (✓ std3). ∎
Source. Repository-derived.
Commentary.
Choose a generator of the finite field’s unit group. It cannot be -1: powers of -1 are 1 or -1, whereas 2 is neither in characteristic five. Thus r+1 is nonzero. Four successor steps return to phase zero by rowReturn(r,c). The preceding orbit theorem and the first three successor steps prove the exact SameCycle criterion for arbitrary states, including the closing edge.
The first coordinates of the four edge labels are 1,2,4,3. Their row coordinates are -2h,-2h,-2h and -(r+1)h+(1-r)c. Each row map is bijective, so BijOn means that every vector with nonzero first coordinate occurs exactly once as a label. The separate vertex BijOn states the same exact inventory for vertices. This covers arbitrary finite extensions in characteristic five; no bound on their degree is imposed.
These are the row-lift ingredients for the dependent-hole construction. A relative detour still requires the three-cut reconnection. The prime seed, the different two-cut construction for primes at least seven, dimension induction and transport to the original vector-space coordinates are not asserted here.