Rotation Map of the Fixed Powered Seed

Lax920634.SeedRotation · concepts/Lax920634/SeedRotation.lean · lax-920634

definition

Loading review…

Natural Language Statement

Definition

The selected thirty permutations supply sixty forward and inverse darts. Adding sixty stationary darts makes the walk lazy. Raising this fixed 120-regular graph to the power 5760000 gives a seed of degree $D=120^{5760000}$ on $D^4$ vertices. Labels of powered edges encode their sequences of original darts in base 120.

Concept map

2 concepts

100%

DefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

Lean source view on GitHub

Show types on hover

1	import Lax920634.SeedSearch
2	import Mathlib.Logic.Equiv.Fin.Basic
3
4	/-!
5	---
6	title: Rotation Map of the Fixed Powered Seed
7	type: definition
8	---
9	The selected thirty permutations supply sixty forward and inverse darts.
10	Adding sixty stationary darts makes the walk lazy. Raising this fixed
11	120-regular graph to the power 5760000 gives a seed of degree
12	$D=120^{5760000}$ on $D^4$ vertices. Labels of powered edges encode their
13	sequences of original darts in base 120.
14
15	# Formalization notes
16
17	Every definition is executable. Finite inverse queries are computed by the
18	scan in `SeedSearch`. Powered edges reverse the traversed dart labels in
19	reverse order. The long exponent and seed size are fixed constants.
20	-/
21
22	namespace Lax920634.SeedRotation
23
24	open SeedSearch
25
26	/-- Number forward and inverse permutation darts by integers below sixty. -/
27	def permutationLabels : (Fin 30 × Bool) ≃ Fin 60 :=
28	(Equiv.prodCongr (Equiv.refl _) finTwoEquiv.symm).trans finProdFinEquiv
29
30	/-- Number the permutation darts and the sixty stationary darts together. -/
31	def lazyLabels : ((Fin 30 × Bool) ⊕ Fin 60) ≃ Fin 120 :=
32	(Equiv.sumCongr permutationLabels (Equiv.refl _)).trans finSumFinEquiv
33
34	/-- The rotation of the selected lazy permutation graph, with numbered labels. -/
35	def lazyRotation (n : ℕ) (p : Fin n × Fin 120) : Fin n × Fin 120 :=
36	match lazyLabels.symm p.2 with
37	\| Sum.inl (i, false) =>
38	(selectedTable n i p.1, lazyLabels (Sum.inl (i, true)))
39	\| Sum.inl (i, true) =>
40	(inverse (selectedTable n i) p.1,
41	lazyLabels (Sum.inl (i, false)))
42	\| Sum.inr j => (p.1, lazyLabels (Sum.inr j))
43
44	/-- Follow a finite sequence of numbered darts to its endpoint. -/
45	def walkEnd {n d : ℕ} (R : Fin n × Fin d → Fin n × Fin d) :
46	(t : ℕ) → Fin n → (Fin t → Fin d) → Fin n
47	\| 0, v, _ => v
48	\| t + 1, v, s => walkEnd R t (R (v, s 0)).1 (fun j => s j.succ)
49
50	/-- The vertex reached after a prescribed number of steps of a finite dart sequence. -/
51	def walkAt {n d : ℕ} (R : Fin n × Fin d → Fin n × Fin d)
52	(t : ℕ) (v : Fin n) (s : Fin t → Fin d) : ℕ → Fin n
53	\| 0 => v
54	\| k + 1 => if h : k < t then
55	(R (walkAt R t v s k, s ⟨k, h⟩)).1 else walkAt R t v s k
56
57	/-- The edge rotation of a graph power, with dart sequences numbered in base `d`. -/
58	def powerRotation {n d : ℕ} (R : Fin n × Fin d → Fin n × Fin d)
59	(t : ℕ) (p : Fin n × Fin (d ^ t)) : Fin n × Fin (d ^ t) :=
60	let s := finFunctionFinEquiv.symm p.2
61	(walkEnd R t p.1 s, finFunctionFinEquiv (fun j =>
62	(R (walkAt R t p.1 s (Fin.rev j).val, s (Fin.rev j))).2))
63
64	/-- The fixed seed's rotation map, after lazy powering. -/
65	def rotation : Fin seedOrder × Fin seedDegree →
66	Fin seedOrder × Fin seedDegree :=
67	powerRotation (lazyRotation seedOrder) poweringExponent
68
69	end Lax920634.SeedRotation
70

Formalization notes

Every definition is executable. Finite inverse queries are computed by the scan in $SeedSearch$ . Powered edges reverse the traversed dart labels in reverse order. The long exponent and seed size are fixed constants.