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

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

The stabilizer of the row's fixed divisor inside the slot-level automorphism group of row06Core has order 96. 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.GenusFiveRow06Symmetry.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.GenusFiveRow06Symmetry.vfun data i = data.getD (↑i) 0

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

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

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

Equations

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

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

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

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

Equations

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

def AtanasovRanganathan.GenusFiveRow06Symmetry.blockSym1 : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row06Core

The row-06 block symmetry with vertex cycles (4 7) (5 6) and slot cycles (4 9) (5 10) (6 11) (7 8). It reverses precisely slots 7, 8.

Equations

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

def AtanasovRanganathan.GenusFiveRow06Symmetry.blockSym2 : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row06Core

The row-06 block symmetry with vertex cycles (0 1) (2 3) (4 5) (6 7) and slot cycles (2 3) (4 7) (8 9). It reverses precisely slots 0, 1, 2, 3, 4, 5, 6, 7, 10, 11.

Equations

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

def AtanasovRanganathan.GenusFiveRow06Symmetry.blockSym3 : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row06Core

The row-06 block symmetry with vertex cycles (0 1) (2 3) (4 6) (5 7) and slot cycles (2 3) (4 8) (5 10) (6 11) (7 9). It reverses precisely slots 0, 1, 2, 3, 5, 6, 7, 9, 10, 11.

Equations

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

def AtanasovRanganathan.GenusFiveRow06Symmetry.blockSym4 : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row06Core

The row-06 block symmetry with vertex cycles (0 4) (1 5) and slot cycles (0 10) (1 11) (2 9) (3 8). It reverses precisely slots 3, 8.

Equations

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

def AtanasovRanganathan.GenusFiveRow06Symmetry.blockSym5 : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row06Core

The row-06 block symmetry with vertex cycles (0 4 7) (1 5 6) and slot cycles (0 10 5) (1 11 6) (2 9 4) (3 8 7). It reverses precisely slots 3, 8.

Equations

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

def AtanasovRanganathan.GenusFiveRow06Symmetry.blockSym6 : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row06Core

The row-06 block symmetry with vertex cycles (0 5) (1 4) (2 3) (6 7) and slot cycles (0 10) (1 11) (2 8) (3 9) (4 7). It reverses precisely slots 0, 1, 3, 4, 5, 6, 7, 9, 10, 11.

Equations

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

def AtanasovRanganathan.GenusFiveRow06Symmetry.blockSym7 : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row06Core

The row-06 block symmetry with vertex cycles (0 5 7 1 4 6) (2 3) and slot cycles (0 10 5) (1 11 6) (2 8 4 3 9 7). It reverses precisely slots 0, 1, 3, 4, 5, 6, 7, 9, 10, 11.

Equations

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

def AtanasovRanganathan.GenusFiveRow06Symmetry.blockSym8 : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row06Core

The row-06 block symmetry with vertex cycles (0 6 4 1 7 5) (2 3) and slot cycles (0 5 10) (1 6 11) (2 7 9 3 4 8). It reverses precisely slots 0, 1, 2, 3, 5, 6, 7, 9, 10, 11.

Equations

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

def AtanasovRanganathan.GenusFiveRow06Symmetry.blockSym9 : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row06Core

The row-06 block symmetry with vertex cycles (0 6) (1 7) (2 3) (4 5) and slot cycles (0 5) (1 6) (2 7) (3 4) (8 9). It reverses precisely slots 0, 1, 2, 3, 4, 5, 6, 7, 10, 11.

Equations

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

def AtanasovRanganathan.GenusFiveRow06Symmetry.blockSym10 : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row06Core

The row-06 block symmetry with vertex cycles (0 7 4) (1 6 5) and slot cycles (0 5 10) (1 6 11) (2 4 9) (3 7 8). It reverses precisely slots 7, 8.

Equations

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

def AtanasovRanganathan.GenusFiveRow06Symmetry.blockSym11 : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row06Core

The row-06 block symmetry with vertex cycles (0 7) (1 6) and slot cycles (0 5) (1 6) (2 4) (3 7). It preserves every slot orientation.

Equations

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

def AtanasovRanganathan.GenusFiveRow06Symmetry.pairSym0 : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row06Core

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

Equations

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

def AtanasovRanganathan.GenusFiveRow06Symmetry.pairSym1 : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row06Core

The parallel-slot symmetry of row 06 with slot cycles (10 11), fixing every vertex and preserving all orientations.

Equations

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

def AtanasovRanganathan.GenusFiveRow06Symmetry.pairSym2 : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row06Core

The parallel-slot symmetry of row 06 with slot cycles (5 6), fixing every vertex and preserving all orientations.

Equations

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

def AtanasovRanganathan.GenusFiveRow06Symmetry.pairSym3 : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row06Core

The parallel-slot symmetry of row 06 with slot cycles (5 6) (10 11), fixing every vertex and preserving all orientations.

Equations

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

def AtanasovRanganathan.GenusFiveRow06Symmetry.pairSym4 : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row06Core

The parallel-slot symmetry of row 06 with slot cycles (0 1), fixing every vertex and preserving all orientations.

Equations

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

def AtanasovRanganathan.GenusFiveRow06Symmetry.pairSym5 : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row06Core

The parallel-slot symmetry of row 06 with slot cycles (0 1) (10 11), fixing every vertex and preserving all orientations.

Equations

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

def AtanasovRanganathan.GenusFiveRow06Symmetry.pairSym6 : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row06Core

The parallel-slot symmetry of row 06 with slot cycles (0 1) (5 6), fixing every vertex and preserving all orientations.

Equations

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

def AtanasovRanganathan.GenusFiveRow06Symmetry.pairSym7 : Utilities.Certificate.CoreOrbitReduction.CoreSymmetry GenusFiveCoreAtlas.row06Core

The parallel-slot symmetry of row 06 with slot cycles (0 1) (5 6) (10 11), fixing every vertex and preserving all orientations.

Equations

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

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

The half of the chamber normalized by the transversal.

Equations

• AtanasovRanganathan.GenusFiveRow06Symmetry.BlockConds length = (length 2 ≤ length 4 ∧ length 4 ≤ length 9 ∧ length 2 ≤ length 3)

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

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

Equations

• AtanasovRanganathan.GenusFiveRow06Symmetry.PairConds length = (length 0 ≤ length 1 ∧ length 5 ≤ length 6 ∧ length 10 ≤ length 11)

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

The fundamental domain itself.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow06Symmetry.block_total (length : Fin 12 → ℕ) : length 2 ≤ length 4 ∧ length 4 ≤ length 9 ∧ length 2 ≤ length 3 ∨ length 2 ≤ length 9 ∧ length 9 ≤ length 4 ∧ length 2 ≤ length 3 ∨ length 3 ≤ length 7 ∧ length 7 ≤ length 8 ∧ length 3 ≤ length 2 ∨ length 3 ≤ length 8 ∧ length 8 ≤ length 7 ∧ length 3 ≤ length 2 ∨ length 9 ≤ length 4 ∧ length 4 ≤ length 2 ∧ length 9 ≤ length 8 ∨ length 4 ≤ length 9 ∧ length 9 ≤ length 2 ∧ length 4 ≤ length 7 ∨ length 8 ≤ length 7 ∧ length 7 ≤ length 3 ∧ length 8 ≤ length 9 ∨ length 7 ≤ length 8 ∧ length 8 ≤ length 3 ∧ length 7 ≤ length 4 ∨ length 8 ≤ length 3 ∧ length 3 ≤ length 7 ∧ length 8 ≤ length 9 ∨ length 7 ≤ length 3 ∧ length 3 ≤ length 8 ∧ length 7 ≤ length 4 ∨ length 9 ≤ length 2 ∧ length 2 ≤ length 4 ∧ length 9 ≤ length 8 ∨ length 4 ≤ length 2 ∧ length 2 ≤ length 9 ∧ length 4 ≤ length 7

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

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

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

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

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