The normalization involution of Core 095

The Atanasov--Ranganathan first-family proof normalizes L₀ ≤ L₅. Core 095 has an involution

(0 5)(1 4)(2 3)

on core vertices. It exchanges slots 0,5 and 3,8, fixes the other slots, and reverses every slot orientation. This file packages that involution as an occurrence-preserving subdivision relabeling, so a proof in the normalized chamber transports to all positive length assignments.

def LowGenus.GenusFourRow095.slotSwapFun : Fin 9 → Fin 9

Slot permutation induced by the Core-095 involution.

Equations

• LowGenus.GenusFourRow095.slotSwapFun = ![5, 1, 2, 8, 4, 0, 6, 7, 3]

theorem LowGenus.GenusFourRow095.slotSwapFun_bijective : Function.Bijective slotSwapFun

def LowGenus.GenusFourRow095.slotSwap : Fin 9 ≃ Fin 9

The involutive permutation of the nine slots induced by the row-095 core symmetry, packaged as an equivalence for transporting lengths.

Equations

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

@[simp]

theorem LowGenus.GenusFourRow095.slotSwap_apply (edge : Fin 9) : slotSwap edge = slotSwapFun edge

def LowGenus.GenusFourRow095.swappedLength (length : Fin 9 → ℕ) (edge : Fin 9) : ℕ

Pull a length assignment across the slot involution.

Equations

• LowGenus.GenusFourRow095.swappedLength length edge = length (LowGenus.GenusFourRow095.slotSwap.symm edge)

theorem LowGenus.GenusFourRow095.swappedLength_pos (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (edge : Fin 9) : 0 < swappedLength length edge

theorem LowGenus.GenusFourRow095.swappedLength_slotSwap (length : Fin 9 → ℕ) (edge : Fin 9) : swappedLength length (slotSwap edge) = length edge

@[simp]

theorem LowGenus.GenusFourRow095.swappedLength_zero (length : Fin 9 → ℕ) : swappedLength length 0 = length 5

@[simp]

theorem LowGenus.GenusFourRow095.swappedLength_five (length : Fin 9 → ℕ) : swappedLength length 5 = length 0

@[simp]

theorem LowGenus.GenusFourRow095.swappedLength_three (length : Fin 9 → ℕ) : swappedLength length 3 = length 8

@[simp]

theorem LowGenus.GenusFourRow095.swappedLength_eight (length : Fin 9 → ℕ) : swappedLength length 8 = length 3

def LowGenus.GenusFourRow095.swapRelabeling (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) : (Spec length hLength).Relabeling (Spec (swappedLength length) ⋯)

The exact occurrence-sensitive relabeling from a Core-095 subdivision to the subdivision with swapped lengths.

Equations

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

def LowGenus.GenusFourRow095.swapGraphIso (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) : Utilities.CFGraphIso (Spec length hLength).graph (Spec (swappedLength length) ⋯).graph

Graph isomorphism implementing the normalization involution.

Equations

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

theorem LowGenus.GenusFourRow095.BNExists_swapped_iff (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (r d : ℤ) : Utilities.BNExists (Spec (swappedLength length) ⋯).graph r d ↔ Utilities.BNExists (Spec length hLength).graph r d

BNExists on the swapped normalization is exactly the original Core-095 existence problem.

theorem LowGenus.GenusFourRow095.BNExists_of_normalized (hNormalized : ∀ (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge), length 0 ≤ length 5 → Utilities.BNExists (Spec length hLength).graph 1 3) (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) : Utilities.BNExists (Spec length hLength).graph 1 3

If the normalized chamber has existence for every positive assignment, then Core 095 has existence for every positive assignment. The theorem is stated for arbitrary rank and degree so the same normalization can be reused at the transmission/essential-row level.