The leg-reversing symmetry of the AR row-08 core

Row 08 is AR's seventh family: a hub 3 carrying both bananas and the stem of a triangle 2 - 4 - 5, whose other two vertices carry the far banana legs.

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

Its vertex automorphism group has order two, generated by

 sigma = (0 6)(1 7)(4 5)

which exchanges the two bananas and the two triangle vertices carrying a leg, and therefore acts on the four leg lengths by (a,b,c,d) ↦ (d,c,b,a).

AR draw three of the four sign patterns of (|e4| - |e3|, |e7| - |e2|); the fourth is the sigma image of the third, so the row needs three chambers proved, not four. Chamber below is their disjunction, and chamber_covers carries every length vector into it.

Note that sigma does not reverse the stem e9 : 2 -> 3: both its ends are fixed. It reverses only the triangle edge e6 and the four slots it swaps in pairs; all six endpoint laws are decided.

def AtanasovRanganathan.GenusFiveRow08Symmetry.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.GenusFiveRow08Symmetry.vfun data i = data.getD (↑i) 0

def AtanasovRanganathan.GenusFiveRow08Symmetry.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.GenusFiveRow08Symmetry.sfun data i = data.getD (↑i) 0

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

Read orientation-reversal flags for the twelve slots, using false for a missing flag.

Equations

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

def AtanasovRanganathan.GenusFiveRow08Symmetry.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.row08Core.tail (smap e) = if rev e = true then vmap (GenusFiveCoreAtlas.row08Core.head e) else vmap (GenusFiveCoreAtlas.row08Core.tail e)) (hh : ∀ (e : Fin 12), GenusFiveCoreAtlas.row08Core.head (smap e) = if rev e = true then vmap (GenusFiveCoreAtlas.row08Core.tail e) else vmap (GenusFiveCoreAtlas.row08Core.head e)) : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row08Core

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.GenusFiveRow08Symmetry.idSym : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row08Core

The identity, spelled in the same shape as sigma.

Equations

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

def AtanasovRanganathan.GenusFiveRow08Symmetry.sigma : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row08Core

The leg reversal (0 6)(1 7)(4 5).

Equations

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

def AtanasovRanganathan.GenusFiveRow08Symmetry.ChamberOne (length : Fin 12 → ℕ) : Prop

AR's first scope: a ≤ b and d ≤ c.

Equations

• AtanasovRanganathan.GenusFiveRow08Symmetry.ChamberOne length = (length 4 ≤ length 3 ∧ length 7 ≤ length 2)

def AtanasovRanganathan.GenusFiveRow08Symmetry.ChamberTwo (length : Fin 12 → ℕ) : Prop

AR's second scope: b ≤ a and c ≤ d.

Equations

• AtanasovRanganathan.GenusFiveRow08Symmetry.ChamberTwo length = (length 3 ≤ length 4 ∧ length 2 ≤ length 7)

def AtanasovRanganathan.GenusFiveRow08Symmetry.ChamberThree (length : Fin 12 → ℕ) : Prop

AR's third scope: b ≤ a and d ≤ c. Its sigma image gives the remaining sign pattern.

Equations

• AtanasovRanganathan.GenusFiveRow08Symmetry.ChamberThree length = (length 3 ≤ length 4 ∧ length 7 ≤ length 2)

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

The union of the three scopes AR draw.

Equations

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

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

Coverage. The four sign patterns are covered by the three drawn scopes together with the sigma image of the third.