Independent generated check. This module provides an additional generated proof of row 04 and is not imported by the main LowGenus root.

Generated symmetry data for the AR row-04 fundamental domain.

The stabilizer of the row's fixed divisor inside the slot-level automorphism group of row04Core has order 64. The chamber below is a fundamental domain for it, so a cover proved on the chamber closes the whole orthant through ClosedOrbit.closedConstruction_of_chamber.

Every permutation is supplied with an explicit inverse, which keeps reindexLength definitionally transparent; all endpoint laws are decided.

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

Read an eight-vertex reindexing from a list, with vertex zero as the default for missing entries.

Equations

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

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

Read a twelve-slot reindexing from a list, with slot zero as the default for missing entries.

Equations

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

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

Read the orientation-reversal flags of the twelve slots, treating missing flags as false.

Equations

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

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

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.GenusFiveRow04Symmetry.blockSym0 : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row04Core

The identity symmetry of the row-04 core, preserving every vertex, slot, and orientation.

Equations

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

def AtanasovRanganathan.GenusFiveRow04Symmetry.blockSym1 : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row04Core

The row-04 block symmetry swapping vertex pairs 0 and 2, 1 and 3, 4 and 7, 5 and 6 and slot pairs 0 and 9, 1 and 10, 2 and 8, 3 and 6, 4 and 7. It reverses every slot orientation.

Equations

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

def AtanasovRanganathan.GenusFiveRow04Symmetry.blockSym2 : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row04Core

The row-04 block symmetry swapping vertex pairs 0 and 5, 1 and 4, 2 and 6, 3 and 7 and slot pairs 0 and 3, 1 and 4, 5 and 11, 6 and 9, 7 and 10. It reverses every slot orientation.

Equations

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

def AtanasovRanganathan.GenusFiveRow04Symmetry.blockSym3 : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row04Core

The row-04 block symmetry swapping vertex pairs 0 and 6, 1 and 7, 2 and 5, 3 and 4 and slot pairs 0 and 6, 1 and 7, 2 and 8, 3 and 9, 4 and 10, 5 and 11. It preserves every slot orientation.

Equations

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

def AtanasovRanganathan.GenusFiveRow04Symmetry.pairSym0 : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row04Core

The row-04 core symmetry that fixes every slot while fixing every vertex and preserving all slot orientations.

Equations

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

def AtanasovRanganathan.GenusFiveRow04Symmetry.pairSym1 : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row04Core

The row-04 core symmetry that exchanges parallel-slot pairs 9 and 10 while fixing every vertex and preserving all slot orientations.

Equations

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

def AtanasovRanganathan.GenusFiveRow04Symmetry.pairSym2 : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row04Core

The row-04 core symmetry that exchanges parallel-slot pairs 6 and 7 while fixing every vertex and preserving all slot orientations.

Equations

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

def AtanasovRanganathan.GenusFiveRow04Symmetry.pairSym3 : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row04Core

The row-04 core symmetry that exchanges parallel-slot pairs 6 and 7, 9 and 10 while fixing every vertex and preserving all slot orientations.

Equations

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

def AtanasovRanganathan.GenusFiveRow04Symmetry.pairSym4 : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row04Core

The row-04 core symmetry that exchanges parallel-slot pairs 3 and 4 while fixing every vertex and preserving all slot orientations.

Equations

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

def AtanasovRanganathan.GenusFiveRow04Symmetry.pairSym5 : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row04Core

The row-04 core symmetry that exchanges parallel-slot pairs 3 and 4, 9 and 10 while fixing every vertex and preserving all slot orientations.

Equations

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

def AtanasovRanganathan.GenusFiveRow04Symmetry.pairSym6 : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row04Core

The row-04 core symmetry that exchanges parallel-slot pairs 3 and 4, 6 and 7 while fixing every vertex and preserving all slot orientations.

Equations

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

def AtanasovRanganathan.GenusFiveRow04Symmetry.pairSym7 : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row04Core

The row-04 core symmetry that exchanges parallel-slot pairs 3 and 4, 6 and 7, 9 and 10 while fixing every vertex and preserving all slot orientations.

Equations

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

def AtanasovRanganathan.GenusFiveRow04Symmetry.pairSym8 : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row04Core

The row-04 core symmetry that exchanges parallel-slot pairs 0 and 1 while fixing every vertex and preserving all slot orientations.

Equations

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

def AtanasovRanganathan.GenusFiveRow04Symmetry.pairSym9 : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row04Core

The row-04 core symmetry that exchanges parallel-slot pairs 0 and 1, 9 and 10 while fixing every vertex and preserving all slot orientations.

Equations

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

def AtanasovRanganathan.GenusFiveRow04Symmetry.pairSym10 : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row04Core

The row-04 core symmetry that exchanges parallel-slot pairs 0 and 1, 6 and 7 while fixing every vertex and preserving all slot orientations.

Equations

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

def AtanasovRanganathan.GenusFiveRow04Symmetry.pairSym11 : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row04Core

The row-04 core symmetry that exchanges parallel-slot pairs 0 and 1, 6 and 7, 9 and 10 while fixing every vertex and preserving all slot orientations.

Equations

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

def AtanasovRanganathan.GenusFiveRow04Symmetry.pairSym12 : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row04Core

The row-04 core symmetry that exchanges parallel-slot pairs 0 and 1, 3 and 4 while fixing every vertex and preserving all slot orientations.

Equations

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

def AtanasovRanganathan.GenusFiveRow04Symmetry.pairSym13 : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row04Core

The row-04 core symmetry that exchanges parallel-slot pairs 0 and 1, 3 and 4, 9 and 10 while fixing every vertex and preserving all slot orientations.

Equations

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

def AtanasovRanganathan.GenusFiveRow04Symmetry.pairSym14 : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row04Core

The row-04 core symmetry that exchanges parallel-slot pairs 0 and 1, 3 and 4, 6 and 7 while fixing every vertex and preserving all slot orientations.

Equations

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

def AtanasovRanganathan.GenusFiveRow04Symmetry.pairSym15 : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row04Core

The row-04 core symmetry that exchanges parallel-slot pairs 0 and 1, 3 and 4, 6 and 7, 9 and 10 while fixing every vertex and preserving all slot orientations.

Equations

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

def AtanasovRanganathan.GenusFiveRow04Symmetry.BlockConds (length : Fin 12 → ℕ) : Prop

The half of the chamber normalized by the transversal.

Equations

• AtanasovRanganathan.GenusFiveRow04Symmetry.BlockConds length = (length 2 ≤ length 8 ∧ length 11 ≤ length 5)

def AtanasovRanganathan.GenusFiveRow04Symmetry.PairConds (length : Fin 12 → ℕ) : Prop

The half of the chamber normalized by parallel-slot swaps.

Equations

• AtanasovRanganathan.GenusFiveRow04Symmetry.PairConds length = (length 0 ≤ length 1 ∧ length 3 ≤ length 4 ∧ length 6 ≤ length 7 ∧ length 9 ≤ length 10)

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

The fundamental domain itself.

Equations

• AtanasovRanganathan.GenusFiveRow04Symmetry.Chamber length = (AtanasovRanganathan.GenusFiveRow04Symmetry.PairConds length ∧ AtanasovRanganathan.GenusFiveRow04Symmetry.BlockConds length)

theorem AtanasovRanganathan.GenusFiveRow04Symmetry.block_total (length : Fin 12 → ℕ) : length 2 ≤ length 8 ∧ length 11 ≤ length 5 ∨ length 8 ≤ length 2 ∧ length 11 ≤ length 5 ∨ length 2 ≤ length 8 ∧ length 5 ≤ length 11 ∨ length 8 ≤ length 2 ∧ length 5 ≤ length 11

Some transversal element normalizes the non-parallel comparisons. The disjunction is exactly BlockConds read through each element's inverse slot map.

theorem AtanasovRanganathan.GenusFiveRow04Symmetry.block_normalize (length : Fin 12 → ℕ) : ∃ (g : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row04Core), BlockConds (g.reindexLength length)

theorem AtanasovRanganathan.GenusFiveRow04Symmetry.pair_normalize (length : Fin 12 → ℕ) (hblock : BlockConds length) : ∃ (g : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row04Core), Chamber (g.reindexLength length)

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

Coverage. Every length vector is carried into the chamber by some core symmetry.