Characteristic-seven complete relative path
Abstract
Marked returns, complete relative paths and exact prefix sums over characteristic-seven fields.
The affine lift, seam equations and vector-label conservation are supplied by CharacteristicSevenDetour. The marked-return construction proves that the particular overlapping surgery has one orbit on the entire carrier. Its bounded enumeration gives the complete relative path, with no claim of literature novelty.
Theorem 1.1 (Complete relative path over every finite characteristic-seven field).
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Sequenceability/CharacteristicSevenRelativePath.exists_characteristic_seven_relative_path (✓ std3). ∎
Source. Repository-derived.
Commentary.
The carrier is (Fin(6) times K) plus two endpoints. The inverse base permutation has four distinct marked cycles represented by headOne, headTwo, target and source. The original FiniteEndpointPairing.first_visit_reattach and same_cycle_of_first_visit interfaces identify the repaired marked return; FiniteBandSwitch.same_cycle_perm_congr transports its explicit four-cycle. Every base inverse edge connects points of the repaired orbit, proving whole-carrier connectivity rather than only the endpoint closing edge.
The label reindexing is swap(predecessorOne,source) times swap(predecessorTwo,source). It fixes target and permutes all other tails. Thus the two removed full vector labels are reassigned to predecessorTwo and source, while predecessorOne receives (0,u). Removing target deletes exactly (0,-u). The resulting label map is bijective onto the nonzero columns together with (0,u).
N=6 card(K)+1. Restrict(v,Fin(N+1)) and restrict(w,Fin(N)) are the bounded vertex and label lists. Interior(v,N-1) means i maps to v(i+1) on Fin(N-1), and boundedPrefixes(w,N+1) includes both the empty and full prefix. The one-cycle enumeration starts at source and ends at target because Q(target)=source. Telescoping identifies every prefix with its vertex and every interval with the difference of two distinct vertices, including the full interval.
No extension-degree or primitive-generator exception is assumed. The construction covers both primitive generators of F7. The arbitrary-subset, same-M and original-coordinate parent problem is outside this theorem.