The order-two symmetry of the AR row-10 core

Row 10 is Atanasov--Ranganathan's ninth family: a triangle {0, 1, 2} with a spoke from each corner, an apex 3 joining the ends of two of the spokes, and a banana {6, 7} reached from the other two spoke ends.

 e0 : 0 -> 2   e1 : 2 -> 1   e2 : 1 -> 0            the triangle
 e10 : 0 -> 3   e4 : 1 -> 4   e3 : 2 -> 5           the three spokes  a, b, c
 e5 : 3 -> 4   e9 : 5 -> 3                          the apex
 e6 : 4 -> 6   e11 : 5 -> 7   e7, e8 : 6 == 7       the banana

The three spokes are not interchangeable -- e10 lands on the apex while e4 and e3 land on the banana side -- so the slot-level symmetry group has order four (two vertex permutations times the banana-slot swap) and the vertex group has order two, generated by

• sigma = (1 2)(4 5)(6 7), slots (e0 e2)(e3 e4)(e5 e9)(e6 e11) with e1, e7, e8, e10 fixed (e1, e7, e8 reversed).

It acts on the three spoke lengths by (a, b, c) ↦ (a, c, b).

The two displayed cases are "a = min(a,b,c)" and "b = min(a,b,c)". The remaining case, c = min, is the sigma image of the second. Thus the three chambers

chamber	inequalities
1 (their first scope)	|e10| ≤ |e4|, |e10| ≤ |e3|
2 (their second scope)	|e4| ≤ |e10|, |e4| ≤ |e3|
3 = sigma(2)	|e3| ≤ |e10|, |e3| ≤ |e4|

cover the closed orthant -- the minimum of three is attained -- and fall into the two orbits {1} (chamber 1 is sigma-stable as a region, since sigma fixes a and swaps b with c) and {2, 3}. Exactly the two scopes AR draw have to be proved. All inequalities are weak, so the three regions overlap on the walls and no strictness is ever needed.

Each permutation carries its own explicit inverse -- sigma is an involution -- which keeps CoreSymmetry.reindexLength definitionally transparent, the pattern of GenusFiveRow01Symmetry and GenusFiveRow05Symmetry.

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

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

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

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

Equations

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

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

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

The identity, spelled in the same shape as the involution.

Equations

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

def AtanasovRanganathan.GenusFiveRow10Symmetry.sigma : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row10Core

The reflection sigma = (1 2)(4 5)(6 7), which fixes the apex spoke e10 and swaps the two banana-side spokes e4 and e3.

Equations

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

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

Chamber 1: AR's first scope, the apex spoke a realizes the minimum.

Equations

• AtanasovRanganathan.GenusFiveRow10Symmetry.ChamberOne length = (length 10 ≤ length 4 ∧ length 10 ≤ length 3)

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

Chamber 2: AR's second scope, the spoke b realizes the minimum.

Equations

• AtanasovRanganathan.GenusFiveRow10Symmetry.ChamberTwo length = (length 4 ≤ length 10 ∧ length 4 ≤ length 3)

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

The union of the two scopes AR draw. The third case, c = min, is the sigma image of chamber 2 and needs no proof of its own.

Equations

• AtanasovRanganathan.GenusFiveRow10Symmetry.Chamber length = (AtanasovRanganathan.GenusFiveRow10Symmetry.ChamberOne length ∨ AtanasovRanganathan.GenusFiveRow10Symmetry.ChamberTwo length)

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

Coverage. The minimum of the three spoke lengths is attained; the two cases where it is a or b are the drawn scopes, and the third is carried onto chamber 2 by sigma, which swaps |e4| with |e3| and fixes |e10|.