The two leg swaps of the AR row-05 core

Row 05 is two bananas, each attached by one leg to each of the two opposite vertices of a four-cycle:

 e0, e1 : 0 == 1            e2 : 2 -> 0     e3 : 1 -> 3
 e4 : 2 -> 5   e5 : 3 -> 5   e9 : 4 -> 3   e7 : 2 -> 4     (the square)
 e6 : 5 -> 7   e8 : 4 -> 6   e10, e11 : 6 == 7

Atanasov--Ranganathan's sixth family draws two of the four sign patterns of (|e2| - |e3|, |e6| - |e8|); the other two are the images of the drawn ones under the two leg swaps

• tauL = (0 1)(2 3), slots (e2 e3)(e4 e5)(e7 e9) -- exchanges the two left legs, hence |e2| <-> |e3|;
• tauR = (4 5)(6 7), slots (e6 e8)(e4 e7)(e5 e9) -- exchanges the two right legs, hence |e6| <-> |e8|.

So the four chambers form a single orbit under ⟨tauL, tauR⟩ and only one has to be proved. Each permutation carries its own explicit inverse -- both are involutions -- which keeps CoreSymmetry.reindexLength definitionally transparent, the pattern of GenusFiveRow04Symmetry and GenusFiveRow06Symmetry.

def AtanasovRanganathan.GenusFiveRow05Symmetry.vfun (data : List (Fin 8)) : Fin 8 → Fin 8

Read an eight-vertex reindexing from a list, using vertex zero for a missing entry.

Equations

• AtanasovRanganathan.GenusFiveRow05Symmetry.vfun data i = data.getD (↑i) 0

def AtanasovRanganathan.GenusFiveRow05Symmetry.sfun (data : List (Fin 12)) : Fin 12 → Fin 12

Read a twelve-slot reindexing from a list, using slot zero for a missing entry.

Equations

• AtanasovRanganathan.GenusFiveRow05Symmetry.sfun data i = data.getD (↑i) 0

def AtanasovRanganathan.GenusFiveRow05Symmetry.bfun (data : List Bool) : Fin 12 → Bool

Read the orientation-reversal flags of the twelve slots, with false as the default.

Equations

• AtanasovRanganathan.GenusFiveRow05Symmetry.bfun data i = data.getD (↑i) false

def AtanasovRanganathan.GenusFiveRow05Symmetry.mkSym (vmap vinv : Fin 8 → Fin 8) (smap sinv : Fin 12 → Fin 12) (rev : Fin 12 → Bool) (hv1 : ∀ (x : Fin 8), vinv (vmap x) = x) (hv2 : ∀ (x : Fin 8), vmap (vinv x) = x) (hs1 : ∀ (x : Fin 12), sinv (smap x) = x) (hs2 : ∀ (x : Fin 12), smap (sinv x) = x) (ht : ∀ (e : Fin 12), GenusFiveCoreAtlas.row05Core.tail (smap e) = if rev e = true then vmap (GenusFiveCoreAtlas.row05Core.head e) else vmap (GenusFiveCoreAtlas.row05Core.tail e)) (hh : ∀ (e : Fin 12), GenusFiveCoreAtlas.row05Core.head (smap e) = if rev e = true then vmap (GenusFiveCoreAtlas.row05Core.tail e) else vmap (GenusFiveCoreAtlas.row05Core.head e)) : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row05Core

A CoreSymmetry literal carrying its own inverses, so that reindexLength reduces without Equiv.ofBijective.

Equations

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

def AtanasovRanganathan.GenusFiveRow05Symmetry.idSym : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row05Core

The identity, spelled in the same shape as the two swaps.

Equations

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

def AtanasovRanganathan.GenusFiveRow05Symmetry.tauL : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row05Core

The left leg swap (0 1)(2 3).

Equations

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

def AtanasovRanganathan.GenusFiveRow05Symmetry.tauR : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row05Core

The right leg swap (4 5)(6 7).

Equations

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

def AtanasovRanganathan.GenusFiveRow05Symmetry.LeftCond (length : Fin 12 → ℕ) : Prop

The left leg comparison of AR's figure.

Equations

• AtanasovRanganathan.GenusFiveRow05Symmetry.LeftCond length = (length 2 ≤ length 3)

def AtanasovRanganathan.GenusFiveRow05Symmetry.RightCond (length : Fin 12 → ℕ) : Prop

The right leg comparison of AR's figure.

Equations

• AtanasovRanganathan.GenusFiveRow05Symmetry.RightCond length = (length 6 ≤ length 8)

def AtanasovRanganathan.GenusFiveRow05Symmetry.Chamber (length : Fin 12 → ℕ) : Prop

Chamber A: the scope Atanasov--Ranganathan draw first.

Equations

• AtanasovRanganathan.GenusFiveRow05Symmetry.Chamber length = (AtanasovRanganathan.GenusFiveRow05Symmetry.LeftCond length ∧ AtanasovRanganathan.GenusFiveRow05Symmetry.RightCond length)

theorem AtanasovRanganathan.GenusFiveRow05Symmetry.left_normalize (length : Fin 12 → ℕ) : ∃ (g : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row05Core), LeftCond (g.reindexLength length)

theorem AtanasovRanganathan.GenusFiveRow05Symmetry.right_normalize (length : Fin 12 → ℕ) (hLeft : LeftCond length) : ∃ (g : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row05Core), Chamber (g.reindexLength length)

theorem AtanasovRanganathan.GenusFiveRow05Symmetry.chamber_covers (length : Fin 12 → ℕ) : ∃ (g : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row05Core), Chamber (g.reindexLength length)

Coverage. Every length vector is carried into chamber A by some core symmetry: the two leg swaps commute and each normalizes one comparison.