Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Finite Alternating Paths and Endpoint Pairing

Abstract

Finite alternating paths pair exposed endpoints and determine all reattached endpoint orbits.

The first-return witnesses give the same least positive first-visit length for the original cut path from J(x) and the reattached path from x, with terminal endpoint (P*J)(x). These lengths are the segment weights in the complete reattachment inventory.

Let X be finite and let s and r be involutive permutations of X. Put E = {x : r(x)=x} and q=s*r, with the right factor applied first. For x in E, take the least positive n with q^n(x) in E. Such n exists by finite permutation recurrence. P(s,r)(x) is this actual first-return endpoint. A first-return segment has no intermediate point in E. For a permutation J of E, extend(J) acts as J on E and fixes X outside E.

Theorem 1.1 (An Involutive Permutation Squares to the Identity).

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PerfectMatchings/FiniteEndpointPairing.square_of_involutive (✓ std3). ∎

Source. Repository-derived.

Commentary.

Applying an involutive permutation twice fixes every element, so its square is the identity permutation.

Theorem 1.2 (First Return Reverses the Same Path).

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PerfectMatchings/FiniteEndpointPairing.endpoint_pairing_involutive (✓ std3). ∎

Source. Repository-derived.

Commentary.

The identity q^nrq^n=r reverses any segment with endpoints fixed by r. If a reverse segment met E earlier, reversing that shorter segment would contradict minimality of the original return time. Thus the two return times agree and P squares to the identity.

Theorem 1.3 (A Free Corner Matching Gives Distinct Endpoints).

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PerfectMatchings/FiniteEndpointPairing.endpoint_pairing_fixed_point_free (✓ std3). ∎

Source. Repository-derived.

Commentary.

If a first return ended where it began, an even-length return would give an earlier r-fixed midpoint. An odd-length return would give an s-fixed midpoint. The first is excluded by minimality and the second by the absence of fixed points of s.

Theorem 1.4 (The Constructed Pairing Computes Reattached Orbits).

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PerfectMatchings/FiniteEndpointPairing.endpoint_pairing_reattach_same_cycle (✓ std3). ∎

Source. Repository-derived.

Commentary.

Changing the attachment acts only at E. Starting at x, the new walk first attaches to J(x), then follows the unchanged interior path to P(J(x)). Induction on a finite walk length decomposes every return into these actual segments. Conversely, each P*J step is a finite segment of the original permutation, so the two orbit relations agree.

References