CANONICAL DELETION OF THE BOUNDARY PAIR

Canonical deletion of coordinates {0, 1} from Fin (2n+2), producing Fin (2n) via the uniform shift x ↦ x + 2.

The construction avoids piecewise reindexing by restricting to the invariant subtype {x | 2 ≤ x.val} and conjugating through a single equivalence.

Architecture:

1. shiftTwoEquiv: the bijection Fin(2n) ≃ { x : Fin(2n+2) | 2 ≤ x }
2. mapsTo_remaining: π(0)=1 ∧ π(1)=0 → π maps {x≥2} to {x≥2}
3. contractZeroOne: restrict π to {x≥2}, conjugate through shiftTwoEquiv

The full deleteAdjacent is then: rotate to (0,1) → contractZeroOne → rotate back (if needed)

def SemicircleCore.shiftTwoEquiv (n : ℕ) : Fin (2 * n) ≃ { x : Fin (2 * n + 2) // 2 ≤ ↑x }

The uniform, piecewise-free embedding of the reduced universe into the expanded universe, bypassing coordinates 0 and 1.

Equations

• SemicircleCore.shiftTwoEquiv n = { toFun := fun (x : Fin (2 * n)) => ⟨⟨↑x + 2, ⋯⟩, ⋯⟩, invFun := fun (y : { x : Fin (2 * n + 2) // 2 ≤ ↑x }) => ⟨↑↑y - 2, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

def SemicircleCore.RemainingDomain (n : ℕ) : Set (Fin (2 * n + 2))

The invariant subspace after 0 and 1 are claimed by adjacency.

Equations

• SemicircleCore.RemainingDomain n = {x : Fin (2 * n + 2) | 2 ≤ ↑x}

theorem SemicircleCore.mapsTo_remaining {n : ℕ} {π : Equiv.Perm (Fin (2 * n + 2))} (h₀ : π ⟨0, ⋯⟩ = ⟨1, ⋯⟩) (h₁ : π ⟨1, ⋯⟩ = ⟨0, ⋯⟩) : Set.MapsTo (⇑π) (RemainingDomain n) (RemainingDomain n)

If π(0) = 1 and π(1) = 0, then π maps {x | x ≥ 2} into itself.

Proof: for x ≥ 2, π(x) ≠ 0 because π(1) = 0 and π is injective, so x = 1, contradicting x ≥ 2. Similarly π(x) ≠ 1 because π(0) = 1 and π is injective, so x = 0, contradicting x ≥ 2. Therefore π(x) ≥ 2.

def SemicircleCore.contractZeroOne {n : ℕ} (π : Equiv.Perm (Fin (2 * n + 2))) (h₀ : π ⟨0, ⋯⟩ = ⟨1, ⋯⟩) (h₁ : π ⟨1, ⋯⟩ = ⟨0, ⋯⟩) : Equiv.Perm (Fin (2 * n))

The sanitized deletion operator. Restrict π to the invariant subtype {x ≥ 2}, then pull back to Fin(2n) via shiftTwoEquiv.

Construction: build the restricted permutation on {x | 2 ≤ x.val}, then conjugate through shiftTwoEquiv.

Equations

• One or more equations did not get rendered due to their size.

theorem SemicircleCore.contractZeroOne_isPairing {n : ℕ} {π : Equiv.Perm (Fin (2 * n + 2))} (h₀ : π ⟨0, ⋯⟩ = ⟨1, ⋯⟩) (h₁ : π ⟨1, ⋯⟩ = ⟨0, ⋯⟩) (hinv : π ^ 2 = 1) (hfpf : ∀ (x : Fin (2 * n + 2)), π x ≠ x) : have π' := contractZeroOne π h₀ h₁; π' ^ 2 = 1 ∧ ∀ (x : Fin (2 * n)), π' x ≠ x

contractZeroOne preserves the pairing property. If π is a fixed-point-free involution on Fin(2n+2) with π(0)=1, then contractZeroOne π is a fixed-point-free involution on Fin(2n).